Functors controlled by finite additive coordinates

If every source object is a finite biproduct of a fixed family of coordinate objects, fullness or faithfulness on pairs of coordinates extends to the whole functor. These lemmas isolate the finite matrix argument used in the standard-mesh restriction comparison.

theorem MagnitudeConjecture.CategoryTheory.functor_faithful_of_finite_coordinates {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : Type} (H : P → C) (F : CategoryTheory.Functor C D) (hcoord : ∀ (X : C), ∃ (n : ℕ) (p : Fin n → P), Nonempty ((⨁ fun (i : Fin n) => H (p i)) ≅ X)) (hfaithful : ∀ (p q : P), Function.Injective fun (f : H p ⟶ H q) => F.map f) : F.Faithful

A functor is faithful if its map is injective between every pair of coordinate objects and every source object is a finite biproduct of coordinates.

theorem MagnitudeConjecture.CategoryTheory.functor_full_of_finite_coordinates {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : Type} (H : P → C) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (hcoord : ∀ (X : C), ∃ (n : ℕ) (p : Fin n → P), Nonempty ((⨁ fun (i : Fin n) => H (p i)) ≅ X)) (hfull : ∀ (p q : P), Function.Surjective fun (f : H p ⟶ H q) => F.map f) : F.Full

An additive functor is full if its map is surjective between every pair of coordinate objects and every source object is a finite biproduct of coordinates.