Uniserial sources of irreducible maps into projectives

This file combines the stable-representable conclusion at a projective boundary with coherent defect duality. Under the two-arm bound, every nonprojective indecomposable source of an irreducible morphism into an indecomposable projective is uniserial.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedProjectivePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : MinimalProjectivePresentation (S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp))

The selected quotient of an irreducible inclusion into a projective, with the original projective as its minimal projective cover.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_sourceIsoSelectedSyzygy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : S.fgObj u ≅ CategoryTheory.Limits.kernel (S.irreducibleIntoProjective_selectedProjectivePresentation u p g hg hp).f

The source of the irreducible inclusion is the syzygy of the selected quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_source_isUniserialModule {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt (FinitelyGeneratedCategory A)] (harity : ∀ (j : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj j) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData j ≤ 2) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (hu : ¬CategoryTheory.Projective (S.fgObj u)) : IsUniserialModule Aᵐᵒᵖ ↑(S.fgObj u).obj

The source-shaped conclusion of Auslander--Reiten Proposition 1.3(a)(iii) at a projective boundary.