Poset-space realization by generated relations

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_realization_of_generated_relations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) {T : Type u} [Fintype T] [PartialOrder T] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (R : S.PrimitiveProjectivePosetData (S.primitiveMultiplicityInput D) T) (X : S.FactorCategory (S.primitiveKilledLabels D)) (Y : PosetSpace.Obj k T) (c : R.representableData.obj X ⟶ Y) (hc : PosetSpace.BoundarySurjective c) : ∃ (M : S.FactorCategory (S.primitiveKilledLabels D)), Nonempty (R.representableData.obj M ≅ Y)

A represented boundary cover realizes its target after quotienting its underlying module by the relations generated at e.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelations_essentiallySurjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) {T : Type u} [Fintype T] [PartialOrder T] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (R : S.PrimitiveProjectivePosetData (S.primitiveMultiplicityInput D) T) (Y : PosetSpace.Obj k T) : ∃ (M : S.FactorCategory (S.primitiveKilledLabels D)), Nonempty (R.representableData.obj M ≅ Y)

Every finite poset space is realized by the generated-relations quotient of the explicit source-and-projective presentation.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsEquivalenceData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) {T : Type u} [Fintype T] [PartialOrder T] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (R : S.PrimitiveProjectivePosetData (S.primitiveMultiplicityInput D) T) : R.representableData.EquivalenceData

The primitive realization equivalence uses generated relations for essential surjectivity and the existing directed-mesh fullness proof.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) {T : Type u} [Fintype T] [PartialOrder T] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (R : S.PrimitiveProjectivePosetData (S.primitiveMultiplicityInput D) T) : S.FactorCategory (S.primitiveKilledLabels D) ≌ PosetSpace.Obj k T

The generated-relations equivalence on the literal primitive factor.