Presentations from directed factor meshes

This file constructs the finite add(U) presentations required by the minimal-realization argument. The induction is over the ambient directed order. Tau-projective labels are coordinates of U; at every other label, the compatible right mesh is a weak-cokernel pair whose middle summands and left boundary strictly precede the endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveObject_finiteAddClosure {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)} (p : S.FactorProjectiveLabel K) : CategoryTheory.finiteAddClosure (S.factorProjectiveGenerator K) (S.factorObject K ↑p)

Every tau-projective selected object is a coordinate retract of the boundary generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightMesh_isWeakCokernel_of_nonprojective {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)} (x : S.SurvivingLabel K) (hx : ¬(S.factorFiniteTauCategoryData K).IsProjective x) : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakCokernel ((S.factorFiniteTauCategoryData K).rightMesh ((S.factorFiniteTauCategoryData K).obj x))

A nonprojective factor right mesh is a weak-cokernel pair, by transport from its compatible left mesh.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorTauPlus_strictly_precedes {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)} (H : S.HasAcyclicNonzeroNonisomorphisms) (x : S.SurvivingLabel K) (hx : ¬(S.factorFiniteTauCategoryData K).IsProjective x) : ↑((S.factorFiniteTauCategoryData K).tauPlus ⟨x, hx⟩) < ↑x

Restricted positive translation strictly precedes its nonprojective factor endpoint in the ambient directed order.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightMiddle_label_strictly_precedes {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)} (H : S.HasAcyclicNonzeroNonisomorphisms) (x : S.SurvivingLabel K) (hx : ¬(S.factorFiniteTauCategoryData K).IsProjective x) {n : ℕ} (label : Fin n → S.SurvivingLabel K) (e : (S.factorFiniteTauCategoryData K).thetaPlus x ≅ ⨁ fun (i : Fin n) => (S.factorFiniteTauCategoryData K).obj (label i)) (t : Fin n) : ↑(label t) < ↑x

Every indecomposable summand in a chosen decomposition of the middle of a nonprojective factor right mesh strictly precedes its endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveGenerator_map_rightEndpoint_isRadical {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)} (H : S.HasAcyclicNonzeroNonisomorphisms) (x : S.SurvivingLabel K) (hx : ¬(S.factorFiniteTauCategoryData K).IsProjective x) (a : S.factorProjectiveGenerator K ⟶ ((S.factorFiniteTauCategoryData K).rightMesh ((S.factorFiniteTauCategoryData K).obj x)).X₃) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism a

Every map from the tau-projective boundary generator into the right endpoint at a nonprojective label is radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject_finiteAddGeneratorPresentation {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (x : S.SurvivingLabel K) : Nonempty (CategoryTheory.FiniteAddGeneratorPresentation (S.factorProjectiveGenerator K) (S.factorObject K x))

Every surviving indecomposable factor object has a finite presentation by the tau-projective boundary generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveGenerator_presentations {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (X : S.FactorCategory K) : Nonempty (CategoryTheory.FiniteAddGeneratorPresentation (S.factorProjectiveGenerator K) X)

Every object of the primitive factor has a finite presentation by the tau-projective boundary generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRestrictedYoneda_full {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) (H : S.HasAcyclicNonzeroNonisomorphisms) : (S.factorProjectiveRestrictedYoneda K).Full

Restricted Yoneda on all tau-projective boundary objects is full in the primitive directed factor.