Fullness of a representable functor from finite additive presentations

This file isolates the elementary categorical core of a minimal-realization argument. If every object has a two-term presentation by objects in add(G), the displayed map is surjective on maps out of G, and the second arrow has the weak-cokernel factorization property, then a faithful Hom(G,-) is full.

The theorem separates the routine Yoneda lifting from the genuinely homological task of constructing these presentations in a strict tau-category.

structure MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G X : C) : Type (max u v)

A two-term presentation of X by objects in add(G), with exactly the two exactness properties detected by Hom(G,-).

• P₁ : C
• P₀ : C
• P₀_mem : finiteAddClosure G self.P₀
• d : self.P₁ ⟶ self.P₀
• p : self.P₀ ⟶ X
• zero : CategoryTheory.CategoryStruct.comp self.d self.p = 0
• lifts_from_generator (h : G ⟶ X) : ∃ (l : G ⟶ self.P₀), CategoryTheory.CategoryStruct.comp l self.p = h
• weakCokernel {Y : C} (q : self.P₀ ⟶ Y) : CategoryTheory.CategoryStruct.comp self.d q = 0 → ∃ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp self.p f = q

def MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.ofFiniteAddClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G X : C} (hX : finiteAddClosure G X) : FiniteAddGeneratorPresentation G X

An object already in add(G) has the tautological presentation.

def MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G X Y : C} (P : FiniteAddGeneratorPresentation G X) (e : X ≅ Y) : FiniteAddGeneratorPresentation G Y

Transport a finite additive presentation across an isomorphism of target objects.

def MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.replaceGenerator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G H X : C} (P : FiniteAddGeneratorPresentation G X) (e : G ≅ H) : FiniteAddGeneratorPresentation H X

Replace the generator of a finite additive presentation by an isomorphic one.

theorem MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.lifts_from_finiteAddClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G X A : C} (P : FiniteAddGeneratorPresentation G X) (hA : finiteAddClosure G A) (h : A ⟶ X) : ∃ (l : A ⟶ P.P₀), CategoryTheory.CategoryStruct.comp l P.p = h

Generator lifting extends from G to every object of add(G).

theorem MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.epi_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G X : C} (P : FiniteAddGeneratorPresentation G X) (hfaithful : (CategoryTheory.preadditiveCoyonedaObj G).Faithful) : CategoryTheory.Epi P.p

Under faithfulness of Hom(G,-), the displayed cover in any finite additive generator presentation is an epimorphism.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G X Y : C} (P : FiniteAddGeneratorPresentation G X) (Q : FiniteAddGeneratorPresentation G Y) : FiniteAddGeneratorPresentation G (X ⊞ Y)

Binary biproducts of finite additive generator presentations.

theorem MagnitudeConjecture.CategoryTheory.finiteAddGeneratorPresentation_finBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : C} {n : ℕ} (F : Fin n → C) (P : (i : Fin n) → FiniteAddGeneratorPresentation G (F i)) : Nonempty (FiniteAddGeneratorPresentation G (⨁ F))

A finite biproduct of objects carrying finite additive generator presentations again carries such a presentation.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteAddGeneratorPresentation.splice {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G L M X : C} (PL : FiniteAddGeneratorPresentation G L) (PM : FiniteAddGeneratorPresentation G M) (f : L ⟶ M) (g : M ⟶ X) (hzero : CategoryTheory.CategoryStruct.comp f g = 0) (hlift : ∀ (h : G ⟶ X), ∃ (k : G ⟶ M), CategoryTheory.CategoryStruct.comp k g = h) (hweak : ∀ {Y : C} (q : M ⟶ Y), CategoryTheory.CategoryStruct.comp f q = 0 → ∃ (s : X ⟶ Y), CategoryTheory.CategoryStruct.comp g s = q) (hfaithful : (CategoryTheory.preadditiveCoyonedaObj G).Faithful) : FiniteAddGeneratorPresentation G X

Splice presentations through a weak-cokernel pair. This is the formal horseshoe step used by the right-tau-mesh induction.

theorem MagnitudeConjecture.CategoryTheory.preadditiveCoyonedaObj_full_of_finiteAddGeneratorPresentations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hfaithful : (CategoryTheory.preadditiveCoyonedaObj G).Faithful) (hpresent : ∀ (X : C), Nonempty (FiniteAddGeneratorPresentation G X)) : (CategoryTheory.preadditiveCoyonedaObj G).Full

A faithful representable functor is full once every object has a finite add(G) presentation of the displayed exact form.