Fullness of an incidence representable functor

A morphism of represented poset spaces is a linear map on Hom(P,-) that preserves the images of all Hom(P_t,-). When precomposition along P ⟶ P_t is injective, it therefore lifts uniquely to every projective coordinate. If the chosen root maps span all maps from P to the boundary projectives, these coordinate lifts commute with every boundary morphism and assemble into a module map on the representable of the boundary biproduct.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.biproduct_lift_eq_sum {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] {F : J → C} [CategoryTheory.Limits.HasBiproduct F] {X : C} (g : (j : J) → X ⟶ F j) : CategoryTheory.Limits.biproduct.lift g = ∑ j : J, CategoryTheory.CategoryStruct.comp (g j) (CategoryTheory.Limits.biproduct.ι F j)

The usual finite-biproduct formula, with an index type in an arbitrary universe. Mathlib's existing statement currently fixes the index in Type 0.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.biproduct_lift_desc {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] {F : J → C} [CategoryTheory.Limits.HasBiproduct F] {X Y : C} (g : (j : J) → X ⟶ F j) (h : (j : J) → F j ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g) (CategoryTheory.Limits.biproduct.desc h) = ∑ j : J, CategoryTheory.CategoryStruct.comp (g j) (h j)

Composition through a finite biproduct is the sum of the coordinate composites, without a universe restriction on the index type.

noncomputable def MagnitudeConjecture.PosetSpace.RepresentableData.biproductReindex {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {I : Type w} {J : Type z} [Finite I] (e : I ≃ J) (F : J → C) [CategoryTheory.Limits.HasBiproduct F] [CategoryTheory.Limits.HasBiproduct fun (i : I) => F (e i)] : (⨁ fun (i : I) => F (e i)) ≅ ⨁ F

Reindex a finite biproduct across index types in arbitrary universes.

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.RepresentableData.boundaryFamily {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) : Option T → C

The root projective followed by the projectives indexed by the poset.

def MagnitudeConjecture.PosetSpace.RepresentableData.boundaryUnit {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (q : Option T) : D.source ⟶ D.boundaryFamily q

The root identity and the chosen maps P ⟶ P_t, uniformly indexed.

def MagnitudeConjecture.PosetSpace.RepresentableData.boundaryPrecomposition {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (q : Option T) (X : C) : (D.boundaryFamily q ⟶ X) →ₗ[k] D.source ⟶ X

Precomposition with a root-to-boundary map.

@[simp]

theorem MagnitudeConjecture.PosetSpace.RepresentableData.boundaryPrecomposition_apply {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (q : Option T) (X : C) (h : D.boundaryFamily q ⟶ X) : (D.boundaryPrecomposition q X) h = CategoryTheory.CategoryStruct.comp (D.boundaryUnit q) h

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.RepresentableData.boundaryGenerator {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) : C

The biproduct of the root and all non-root boundary projectives.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.boundaryPrecomposition_injective {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (X : C), Function.Injective ⇑(D.precomposition t X)) (q : Option T) (X : C) : Function.Injective ⇑(D.boundaryPrecomposition q X)

theorem MagnitudeConjecture.PosetSpace.RepresentableData.map_boundaryPrecomposition_mem_range {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) {X Y : C} (f : D.obj X ⟶ D.obj Y) (q : Option T) (h : D.boundaryFamily q ⟶ X) : f.linear ((D.boundaryPrecomposition q X) h) ∈ (D.boundaryPrecomposition q Y).range

A poset-space morphism sends the image of every boundary precomposition map into the corresponding target image.

def MagnitudeConjecture.PosetSpace.RepresentableData.boundaryRangeMap {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) {X Y : C} (f : D.obj X ⟶ D.obj Y) (q : Option T) : ↥(D.boundaryPrecomposition q X).range →ₗ[k] ↥(D.boundaryPrecomposition q Y).range

The map induced by a poset-space morphism on the ranges of the boundary precomposition maps.

noncomputable def MagnitudeConjecture.PosetSpace.RepresentableData.boundaryComponentMap {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) {X Y : C} (f : D.obj X ⟶ D.obj Y) (q : Option T) : (D.boundaryFamily q ⟶ X) →ₗ[k] D.boundaryFamily q ⟶ Y

The unique lift of a poset-space morphism to one boundary-projective Hom coordinate.

@[simp]

theorem MagnitudeConjecture.PosetSpace.RepresentableData.boundaryPrecomposition_componentMap {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) {X Y : C} (f : D.obj X ⟶ D.obj Y) (q : Option T) (h : D.boundaryFamily q ⟶ X) : (D.boundaryPrecomposition q Y) ((D.boundaryComponentMap hinj f q) h) = f.linear ((D.boundaryPrecomposition q X) h)

theorem MagnitudeConjecture.PosetSpace.RepresentableData.boundaryComponentMap_natural {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) (hspan : ∀ (q : Option T) (a : D.source ⟶ D.boundaryFamily q), ∃ (c : k), c • D.boundaryUnit q = a) {X Y : C} (f : D.obj X ⟶ D.obj Y) (q r : Option T) (a : D.boundaryFamily q ⟶ D.boundaryFamily r) (h : D.boundaryFamily r ⟶ X) : (D.boundaryComponentMap hinj f q) (CategoryTheory.CategoryStruct.comp a h) = CategoryTheory.CategoryStruct.comp a ((D.boundaryComponentMap hinj f r) h)

Coordinate lifts commute with every morphism among boundary projectives. The proof only uses that root-to-boundary maps span the corresponding Hom spaces.

noncomputable def MagnitudeConjecture.PosetSpace.RepresentableData.boundaryTotalLinearMap {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) {X Y : C} (f : D.obj X ⟶ D.obj Y) : (D.boundaryGenerator ⟶ X) →ₗ[k] D.boundaryGenerator ⟶ Y

The coordinate lifts assembled on the boundary biproduct.

@[simp]

theorem MagnitudeConjecture.PosetSpace.RepresentableData.boundary_ι_totalLinearMap {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) {X Y : C} (f : D.obj X ⟶ D.obj Y) (q : Option T) (h : D.boundaryGenerator ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι D.boundaryFamily q) ((D.boundaryTotalLinearMap hinj f) h) = (D.boundaryComponentMap hinj f q) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι D.boundaryFamily q) h)

theorem MagnitudeConjecture.PosetSpace.RepresentableData.boundaryTotalLinearMap_natural {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) (hspan : ∀ (q : Option T) (a : D.source ⟶ D.boundaryFamily q), ∃ (c : k), c • D.boundaryUnit q = a) {X Y : C} (f : D.obj X ⟶ D.obj Y) (a : D.boundaryGenerator ⟶ D.boundaryGenerator) (h : D.boundaryGenerator ⟶ X) : (D.boundaryTotalLinearMap hinj f) (CategoryTheory.CategoryStruct.comp a h) = CategoryTheory.CategoryStruct.comp a ((D.boundaryTotalLinearMap hinj f) h)

The assembled map is natural for precomposition by every endomorphism of the boundary generator.

noncomputable def MagnitudeConjecture.PosetSpace.RepresentableData.boundaryModuleMap {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) (hspan : ∀ (q : Option T) (a : D.source ⟶ D.boundaryFamily q), ∃ (c : k), c • D.boundaryUnit q = a) {X Y : C} (f : D.obj X ⟶ D.obj Y) : (CategoryTheory.preadditiveCoyonedaObj D.boundaryGenerator).obj X ⟶ (CategoryTheory.preadditiveCoyonedaObj D.boundaryGenerator).obj Y

A poset-space morphism determines a module morphism between the representables of the boundary generator.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.map_surjective_of_boundaryCoyoneda_full {k T : Type u} {C : Type v} [Field k] [Fintype T] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (D : RepresentableData k T C) (hinj : ∀ (t : T) (Z : C), Function.Injective ⇑(D.precomposition t Z)) (hspan : ∀ (q : Option T) (a : D.source ⟶ D.boundaryFamily q), ∃ (c : k), c • D.boundaryUnit q = a) (hfull : (CategoryTheory.preadditiveCoyonedaObj D.boundaryGenerator).Full) {X Y : C} (f : D.obj X ⟶ D.obj Y) : ∃ (g : X ⟶ Y), D.map g = f

Fullness of restricted Yoneda on the boundary generator implies fullness of the concrete represented poset-space functor.