Boundary-generator covers of finite poset spaces

Every finite poset space is a strict quotient of an explicit object assembled from an empty-support ambient summand and principal-filter boundary summands. The construction records the elementary projective presentation on the target side of Iyama's realization. The remaining algebraic issue is to lift this strict quotient through the finite strict tau-category.

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.boundaryCoverCarrier {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) : Type u

The carrier of the boundary-generator cover. The first coordinate is an empty-support copy of the ambient space. The second coordinate contains one copy of Y_t for every boundary point t.

def MagnitudeConjecture.PosetSpace.boundaryCoverSubspace {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) (r : T) : Submodule k (boundaryCoverCarrier Y)

At r, the boundary cover retains exactly the coordinates indexed by t ≤ r; the empty-support ambient coordinate is zero.

def MagnitudeConjecture.PosetSpace.boundaryCover {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : Obj k T

The explicit finite poset space built from the root and non-root boundary coordinates.

def MagnitudeConjecture.PosetSpace.boundaryCoverLinear {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : boundaryCoverCarrier Y →ₗ[k] Y.carrier

Sum the ambient coordinate and all non-root boundary coordinates.

def MagnitudeConjecture.PosetSpace.boundaryCoverMap {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : boundaryCover Y ⟶ Y

The canonical boundary-generator cover of Y.

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryCoverMap_linear {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : (boundaryCoverMap Y).linear = boundaryCoverLinear Y

theorem MagnitudeConjecture.PosetSpace.boundaryCoverMap_surjective {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : Function.Surjective ⇑(boundaryCoverMap Y).linear

The boundary cover is surjective on its ambient vector space.

theorem MagnitudeConjecture.PosetSpace.boundaryCoverMap_epi {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : CategoryTheory.Epi (boundaryCoverMap Y)

The canonical boundary cover is an epimorphism.

theorem MagnitudeConjecture.PosetSpace.boundaryCoverMap_subspace_surjective {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) (r : T) : Function.Surjective ⇑(LinearMap.codRestrict (Y.subspace r) ((boundaryCoverMap Y).linear.domRestrict ((boundaryCover Y).subspace r)) ⋯)

The boundary cover is also surjective on every distinguished subspace. Thus it is the strict/deflation-type cover used by the hereditary torsionfree realization, not merely a categorical epimorphism.

theorem MagnitudeConjecture.PosetSpace.map_boundaryCoverSubspace {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) (r : T) : Submodule.map (boundaryCoverMap Y).linear ((boundaryCover Y).subspace r) = Y.subspace r

Equivalently, the image of the r-subspace under the cover map is exactly Y_r.

def MagnitudeConjecture.PosetSpace.BoundarySurjective {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) : Prop

A morphism of poset spaces is boundary-surjective when it is surjective on the ambient space and on each distinguished subspace.

theorem MagnitudeConjecture.PosetSpace.BoundarySurjective.comp {k T : Type u} [Field k] [PartialOrder T] {X Y Z : Obj k T} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : BoundarySurjective f) (hg : BoundarySurjective g) : BoundarySurjective (CategoryTheory.CategoryStruct.comp f g)

Boundary-surjective morphisms are closed under composition.

theorem MagnitudeConjecture.PosetSpace.boundarySurjective_iso_hom {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (e : X ≅ Y) : BoundarySurjective e.hom

Either direction of an isomorphism is boundary-surjective.

theorem MagnitudeConjecture.PosetSpace.boundaryCoverMap_boundarySurjective {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) : BoundarySurjective (boundaryCoverMap Y)

The canonical boundary cover is boundary-surjective.

def MagnitudeConjecture.PosetSpace.boundaryCoverRootVector {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) (y : Y.carrier) : boundaryCoverCarrier Y

The empty-support contribution of one ambient vector.

noncomputable def MagnitudeConjecture.PosetSpace.boundaryCoverPointVector {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) (t : T) (y : ↥(Y.subspace t)) : boundaryCoverCarrier Y

The principal-filter contribution of one vector in Y_t.

theorem MagnitudeConjecture.PosetSpace.boundaryCover_eq_root_add_sum_points {k T : Type u} [Field k] [Fintype T] [PartialOrder T] (Y : Obj k T) (x : boundaryCoverCarrier Y) : x = boundaryCoverRootVector Y x.1 + ∑ t : T, boundaryCoverPointVector Y t (x.2 t)

The explicit cover is generated by its empty-support coordinate and its principal-filter coordinates.

Relative projectivity of the boundary lines

def MagnitudeConjecture.PosetSpace.BoundaryProjective {k T : Type u} [Field k] [PartialOrder T] (P : Obj k T) : Prop

A poset-space object is projective for boundary-surjective morphisms if maps from it lift across every such morphism.

def MagnitudeConjecture.PosetSpace.lineMapOfVector {k T : Type u} [Field k] [PartialOrder T] (U : Set T) (hU : IsUpperSet U) (X : Obj k T) (x : X.carrier) (hx : ∀ r ∈ U, x ∈ X.subspace r) : line k T U hU ⟶ X

A vector lying in all subspaces on U defines a map from the line with support U.

@[simp]

theorem MagnitudeConjecture.PosetSpace.lineMapOfVector_apply {k T : Type u} [Field k] [PartialOrder T] (U : Set T) (hU : IsUpperSet U) (X : Obj k T) (x : X.carrier) (hx : ∀ r ∈ U, x ∈ X.subspace r) (a : k) : (lineMapOfVector U hU X x hx).linear a = a • x

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.emptySupport {T : Type u} : Set T

The empty upper support carried by the root boundary line.

theorem MagnitudeConjecture.PosetSpace.emptySupport_isUpperSet {T : Type u} [PartialOrder T] : IsUpperSet emptySupport

def MagnitudeConjecture.PosetSpace.principalSupport {T : Type u} [PartialOrder T] (t : T) : Set T

The principal upper support carried by the boundary line at t.

theorem MagnitudeConjecture.PosetSpace.principalSupport_isUpperSet {T : Type u} [PartialOrder T] (t : T) : IsUpperSet (principalSupport t)

theorem MagnitudeConjecture.PosetSpace.emptyLine_boundaryProjective {k T : Type u} [Field k] [PartialOrder T] : BoundaryProjective (line k T emptySupport ⋯)

The empty-support root line lifts across every boundary-surjective map.

theorem MagnitudeConjecture.PosetSpace.principalLine_boundaryProjective {k T : Type u} [Field k] [PartialOrder T] (t : T) : BoundaryProjective (line k T (principalSupport t) ⋯)

Every principal-filter boundary line lifts across boundary-surjective maps. These are the non-root projectives of the exact boundary structure.