Lemma 4.12: exhaustion by sources and sinks

lem:cover-exhaustion (scalar-normalization.tex): "There is an increasing sequence of finite convex full subcategories of L with union L, each obtained from the previous one by adding a source or a sink. […] Consequently L has a multiplicative basis."

This file proves the abstract form for a thin directed category with a height function, finitely many outgoing lines at each object and countably many objects. Sinks are sources of the opposite category (extend_sink).

The opposite category

def MultiplicativeBasisDeformations.Thin.opLinear {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] : CategoryTheory.Linear k Oᵒᵖ

The opposite of a k-linear category is k-linear.

theorem MultiplicativeBasisDeformations.Thin.unop_smul {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {X Y : Oᵒᵖ} (c : k) (f : X ⟶ Y) : (c • f).unop = c • f.unop

def MultiplicativeBasisDeformations.Thin.unopLinearEquiv {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (X Y : Oᵒᵖ) : (X ⟶ Y) ≃ₗ[k] Opposite.unop Y ⟶ Opposite.unop X

unop as a linear equivalence.

theorem MultiplicativeBasisDeformations.Thin.isThin_op {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) : IsThin k Oᵒᵖ

def MultiplicativeBasisDeformations.Thin.opβ {O : Type v} [CategoryTheory.Category.{w, v} O] (β : (o o' : O) → o ⟶ o') (X Y : Oᵒᵖ) : X ⟶ Y

The opposite of a family of basis vectors.

theorem MultiplicativeBasisDeformations.Thin.multBasis_op {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {β : (o o' : O) → o ⟶ o'} (hβ : MultBasis S β) : MultBasis (Opposite.unop ⁻¹' S) (opβ β)

theorem MultiplicativeBasisDeformations.Thin.multBasis_unop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {β : (X Y : Oᵒᵖ) → X ⟶ Y} (hβ : MultBasis (Opposite.unop ⁻¹' S) β) : MultBasis S fun (o o' : O) => (β (Opposite.op o') (Opposite.op o)).unop

def MultiplicativeBasisDeformations.Thin.opEmb {O : Type v} : O ↪ Oᵒᵖ

op as an embedding.

theorem MultiplicativeBasisDeformations.Thin.coe_map_op {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Finset O) : ↑(Finset.map opEmb S) = Opposite.unop ⁻¹' ↑S

theorem MultiplicativeBasisDeformations.Thin.extend_sink {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) [Infinite k] (t : O) (S : Finset O) (htS : t ∉ S) (hsnk : ∀ o ∈ S, ∀ (f : t ⟶ o), f = 0) (β : (o o' : O) → o ⟶ o') (hβ : MultBasis (↑S) β) (hrep : SupRepFinite ⋯ ⋯) : ∃ (β' : (o o' : O) → o ⟶ o'), MultBasis (insert t ↑S) β' ∧ ∀ o ∈ S, ∀ o' ∈ S, β' o o' = β o o'

Lemma 4.11(1) for a sink: a source of the opposite category.

Chains and convex sets

def MultiplicativeBasisDeformations.Thin.Rl {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (o o' : O) : Prop

A nonzero line between distinct objects.

def MultiplicativeBasisDeformations.Thin.Le {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (o o' : O) : Prop

The chain order.

theorem MultiplicativeBasisDeformations.Thin.le_hgt {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') {a b : O} (h : Le a b) : hgt a ≤ hgt b

theorem MultiplicativeBasisDeformations.Thin.lt_hgt {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') {a b : O} (h : Le a b) (hne : a ≠ b) : hgt a < hgt b

theorem MultiplicativeBasisDeformations.Thin.le_antisymm' {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') {a b : O} (h₁ : Le a b) (h₂ : Le b a) : a = b

def MultiplicativeBasisDeformations.Thin.Convex {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (T : Set O) : Prop

A convex set.

theorem MultiplicativeBasisDeformations.Thin.interval_finite {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (b : O) (n : ℕ) (a : O) : hgt b - hgt a < ↑n → {c : O | Le a c ∧ Le c b}.Finite

Intervals are finite.

def MultiplicativeBasisDeformations.Thin.hull {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (F : Finset O) : Set O

The convex hull of a finite set.

theorem MultiplicativeBasisDeformations.Thin.hull_finite {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (F : Finset O) : (hull F).Finite

theorem MultiplicativeBasisDeformations.Thin.hull_convex {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (F : Finset O) : Convex (hull F)

theorem MultiplicativeBasisDeformations.Thin.subset_hull {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (F : Finset O) : ↑F ⊆ hull F

theorem MultiplicativeBasisDeformations.Thin.hull_mono {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {F F' : Finset O} (h : F ⊆ F') : hull F ⊆ hull F'

Choosing the next object

theorem MultiplicativeBasisDeformations.Thin.step_obj {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (T T' : Finset O) (hTT' : T ⊆ T') (hne : T ≠ T') (hT1 : Convex ↑T) (hT2 : Convex ↑T') : ∃ c ∈ T', c ∉ T ∧ Convex (insert c ↑T) ∧ ((∀ o ∈ T, ∀ (f : o ⟶ c), f = 0) ∨ ∀ o ∈ T, ∀ (f : c ⟶ o), f = 0)

One step, objects only: a missing object which is a source or a sink for T, keeping convexity.

Adding one object at a time

theorem MultiplicativeBasisDeformations.Thin.step {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (T T' : Finset O) (hTT' : T ⊆ T') (hne : T ≠ T') (hT1 : Convex ↑T) (hT2 : Convex ↑T') (β : (o o' : O) → o ⟶ o') (hβ : MultBasis (↑T) β) : ∃ c ∈ T', c ∉ T ∧ Convex (insert c ↑T) ∧ ∃ (β' : (o o' : O) → o ⟶ o'), MultBasis (insert c ↑T) β' ∧ ∀ o ∈ T, ∀ o' ∈ T, β' o o' = β o o'

One step: add a source, a sink, or an isolated object, keeping convexity (scalar-normalization.tex).

theorem MultiplicativeBasisDeformations.Thin.fill {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) [DecidableEq O] (n : ℕ) (T T' : Finset O) : (T' \ T).card = n → T ⊆ T' → Convex ↑T → Convex ↑T' → ∀ (β : (o o' : O) → o ⟶ o'), MultBasis (↑T) β → ∃ (β' : (o o' : O) → o ⟶ o'), MultBasis (↑T') β' ∧ ∀ o ∈ T, ∀ o' ∈ T, β' o o' = β o o'

Filling a finite convex set from a smaller one.

noncomputable def MultiplicativeBasisDeformations.Thin.exT {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) : Finset O

The finite convex sets of the exhaustion.

theorem MultiplicativeBasisDeformations.Thin.coe_exT {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) : ↑(exT hgt hR hsucc e n) = hull (Finset.image e (Finset.range (n + 1)))

theorem MultiplicativeBasisDeformations.Thin.exT_mono {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) : exT hgt hR hsucc e n ⊆ exT hgt hR hsucc e (n + 1)

theorem MultiplicativeBasisDeformations.Thin.exT_convex {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) : Convex ↑(exT hgt hR hsucc e n)

theorem MultiplicativeBasisDeformations.Thin.mem_exT {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) : e n ∈ exT hgt hR hsucc e n

theorem MultiplicativeBasisDeformations.Thin.exists_next {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) (β : (o o' : O) → o ⟶ o') (hβ : MultBasis (↑(exT hgt hR hsucc e n)) β) : ∃ (β' : (o o' : O) → o ⟶ o'), MultBasis (↑(exT hgt hR hsucc e (n + 1))) β' ∧ ∀ o ∈ exT hgt hR hsucc e n, ∀ o' ∈ exT hgt hR hsucc e n, β' o o' = β o o'

theorem MultiplicativeBasisDeformations.Thin.exists_first {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) : ∃ (β' : (o o' : O) → o ⟶ o'), MultBasis (↑(exT hgt hR hsucc e 0)) β'

def MultiplicativeBasisDeformations.Thin.basSeq {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) : { β : (o o' : O) → o ⟶ o' // MultBasis (↑(exT hgt hR hsucc e n)) β }

The sequence of bases.

theorem MultiplicativeBasisDeformations.Thin.basSeq_succ {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) (n : ℕ) (o : O) : o ∈ exT hgt hR hsucc e n → ∀ o' ∈ exT hgt hR hsucc e n, ↑(basSeq hT hgt hR hsrcRep hsnkRep hsucc e (n + 1)) o o' = ↑(basSeq hT hgt hR hsrcRep hsnkRep hsucc e n) o o'

theorem MultiplicativeBasisDeformations.Thin.exT_mono' {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) {n m : ℕ} (h : n ≤ m) : exT hgt hR hsucc e n ⊆ exT hgt hR hsucc e m

theorem MultiplicativeBasisDeformations.Thin.basSeq_agree {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) [DecidableEq O] (e : ℕ → O) {n m : ℕ} (h : n ≤ m) (o : O) : o ∈ exT hgt hR hsucc e n → ∀ o' ∈ exT hgt hR hsucc e n, ↑(basSeq hT hgt hR hsrcRep hsnkRep hsucc e m) o o' = ↑(basSeq hT hgt hR hsrcRep hsnkRep hsucc e n) o o'

theorem MultiplicativeBasisDeformations.Thin.exists_multBasis {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) (he : Function.Surjective e) : ∃ (β : (o o' : O) → o ⟶ o'), MultBasis Set.univ β

Lemma 4.12 (lem:cover-exhaustion): a thin directed category with a height, finitely many outgoing lines at each object and countably many objects has a multiplicative basis.