Representing the strict boundary-generator cover

The explicit strict cover of a finite poset space is represented by a finite biproduct of the distinguished source and the non-root tau-projectives. This supplies the degree-zero object in a boundary-projective presentation for Iyama's minimal realization. Applying the same construction to its kernel will supply the relation object; the remaining step is to lift that relation map and construct its categorical weak cokernel/minimal realization.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverIndex {k : Type u} [Field k] {T : Type u} [PartialOrder T] (Y : PosetSpace.Obj k T) : Type u

Coordinates used for the root and point summands of the strict cover.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverFamily {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) : boundaryCoverIndex Y → S.FactorCategory K

The categorical family whose root summands are copies of P and whose point summands over t are copies of P_t.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) : S.FactorCategory K

The object representing the explicit boundary-generator cover.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverRootProjection {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) (i : Fin (Module.finrank k Y.carrier)) : R.boundaryCoverObject Y ⟶ R.representableData.source

Projection from the categorical cover to one root copy.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverPointProjection {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) (t : T) (i : Fin (Module.finrank k ↥(Y.subspace t))) : R.boundaryCoverObject Y ⟶ R.projective t

Projection from the categorical cover to one point copy.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) : ((j : boundaryCoverIndex Y) → R.representableData.source ⟶ R.boundaryCoverFamily Y j) ≃ₗ[k] PosetSpace.boundaryCoverCarrier Y

Boundary Hom coordinates converted into the carrier coordinates of the explicit root-plus-point cover.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) : (R.representableData.obj (R.boundaryCoverObject Y)).carrier ≃ₗ[k] PosetSpace.boundaryCoverCarrier Y

The represented carrier of the categorical cover has the explicit root-plus-point coordinates.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverLinearEquiv_apply_root {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) (f : (R.representableData.obj (R.boundaryCoverObject Y)).carrier) (i : Fin (Module.finrank k Y.carrier)) : (Module.finBasis k Y.carrier).equivFun ((R.representedBoundaryCoverLinearEquiv Y) f).1 i = R.sourceCoordinateEquiv (CategoryTheory.CategoryStruct.comp f (R.boundaryCoverRootProjection Y i))

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverLinearEquiv_apply_point {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) (f : (R.representableData.obj (R.boundaryCoverObject Y)).carrier) (t : T) (i : Fin (Module.finrank k ↥(Y.subspace t))) : (Module.finBasis k ↥(Y.subspace t)).equivFun (((R.representedBoundaryCoverLinearEquiv Y) f).2 t) i = (R.unitCoordinateEquiv t) (CategoryTheory.CategoryStruct.comp f (R.boundaryCoverPointProjection Y t i))

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryCoverObjectIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) : R.representableData.obj (R.boundaryCoverObject Y) ≅ PosetSpace.boundaryCover Y

Restricted Yoneda sends the categorical boundary-cover object to the explicit strict boundary cover.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) : R.representableData.obj (R.boundaryCoverObject Y) ⟶ Y

The explicit represented cover map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverMap_boundarySurjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) : PosetSpace.BoundarySurjective (R.representedBoundaryCoverMap H Y)

Every finite poset space admits a represented boundary-surjective cover assembled only from the distinguished source and non-root tau-projectives.