The tau-projective boundary generator

The manuscript realizes the primitive factor through the biproduct U of all indecomposable tau-projective boundary objects. This file constructs that literal object, exhibits it as a coordinate retract of the full surviving additive generator, and proves directly that its representable functor is faithful in the primitive situation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveGenerator {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)) : S.FactorCategory K

The biproduct of all surviving indecomposable tau-projectives. This is the manuscript's object U.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveGeneratorRetract {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)) : CategoryTheory.Retract (S.factorProjectiveGenerator K) (S.factorAdditiveGenerator K)

The boundary generator is the coordinate retract of the full surviving additive generator selected by the tau-projective predicate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveGenerator_finiteAddPresentation {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)) : CategoryTheory.FiniteAddPresentation (S.factorAdditiveGenerator K) (S.factorProjectiveGenerator K)

In particular, the tau-projective boundary generator belongs to the additive closure of the full surviving generator.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRestrictedYoneda {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)) : CategoryTheory.Functor (S.FactorCategory K) (ModuleCat (CategoryTheory.End (S.factorProjectiveGenerator K))ᵐᵒᵖ)

Restricted Yoneda on the actual tau-projective boundary generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRestrictedYoneda_faithful {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) : (S.factorProjectiveRestrictedYoneda K).Faithful

In a primitive factor, restricted Yoneda on all tau-projectives is faithful. The distinguished source is one of the summands of U, and its representable functor was already proved faithful by the trace quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRestrictedYoneda_full_of_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) (hpresent : ∀ (X : S.FactorCategory K), Nonempty (CategoryTheory.FiniteAddGeneratorPresentation (S.factorProjectiveGenerator K) X)) : (S.factorProjectiveRestrictedYoneda K).Full

Once finite presentations by the tau-projective boundary generator are constructed, the restricted Yoneda functor is full. This is the exact routine lifting part of Iyama's minimal-realization argument.