Quotients by irreducible submodules of indecomposable projectives

This file packages the categorical initialization of Auslander--Reiten Corollary 3.8. An irreducible morphism into a projective cannot be epic, so it is monic. Its cokernel is a nonzero quotient of an indecomposable projective and hence is indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_mono {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {U P : FinitelyGeneratedCategory A} (g : U ⟶ P) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hP : CategoryTheory.Projective P) : CategoryTheory.Mono g

An irreducible morphism into a projective object is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernel_factorization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U X : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (h : X ⟶ CategoryTheory.Limits.cokernel g) (hnot : ¬∃ (l : X ⟶ S.fgObj p), CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.cokernel.π g) = h) : ∃ (r : S.fgObj p ⟶ X), CategoryTheory.CategoryStruct.comp r h = CategoryTheory.Limits.cokernel.π g

A map into the cokernel of an irreducible inclusion into a projective which does not lift to that projective contains the cokernel projection as a factor. This is the projective-cokernel form of the pullback argument in Auslander--Reiten IV, Proposition 2.7.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernel_not_isZero {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {U P : FinitelyGeneratedCategory A} (g : U ⟶ P) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hP : CategoryTheory.Projective P) : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel g)

The cokernel of an irreducible morphism into a projective is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernel_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Indecomposable (CategoryTheory.Limits.cokernel g)

If the target is a selected indecomposable projective, the cokernel of an irreducible morphism into it is indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernelπ_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.Limits.cokernel.π g)

The canonical projective quotient is right minimal.

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

The cokernel projection, bundled as the minimal projective presentation of the quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernel_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : ¬CategoryTheory.Projective (CategoryTheory.Limits.cokernel g)

The quotient cannot itself be projective, since otherwise its defining short exact sequence would split and the irreducible inclusion would be a section.

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

The selected label of the indecomposable quotient.

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

The quotient in the coordinates of the chosen finite skeleton.

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

The canonical projective quotient map in the chosen skeleton coordinates.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_quotientMap_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Epi (S.irreducibleIntoProjective_quotientMap p g hg hp)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_comp_quotientMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.CategoryStruct.comp g (S.irreducibleIntoProjective_quotientMap p g hg hp) = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_comp_quotientMap_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) {Z : FinitelyGeneratedCategory A} (h : S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp) ⟶ Z) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_quotientMap p g hg hp) h) = CategoryTheory.CategoryStruct.comp 0 h

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

The selected quotient label is nonprojective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_quotientMap_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.irreducibleIntoProjective_quotientMap p g hg hp)

The selected projective quotient remains right minimal.