The projective boundary almost-split morphism

For an indecomposable projective finitely generated module P, the inclusion rad P ⟶ P is minimal right almost split. The proof is a bounded adaptation of the relevant arguments in the donor's ProjectiveSimpleTop.lean, ProjectiveSimpleRank.lean, and ProjectiveBoundaryAlmostSplit.lean at commit d5ba0c48e7a851afd51247ff9cd81fc629e00ed2. Their unrelated simple-ranking and standard-semantics layers are not imported.

theorem MagnitudeConjecture.moduleProjective_of_fgProjective {R : Type u} [Ring R] [IsNoetherianRing R] (X : FGModuleCat R) (hX : CategoryTheory.Projective X) : Module.Projective R ↑X

A categorical projective in FGModuleCat is projective as an unbundled module.

theorem MagnitudeConjecture.surjective_of_quotient_comp_surjective {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] [IsLocalRing (Module.End R P)] {N : Submodule R P} (hN : N ≠ ⊤) {Z : Type w} [AddCommGroup Z] [Module R Z] (g : Z →ₗ[R] P) (hg : Function.Surjective ⇑(N.mkQ ∘ₗ g)) : Function.Surjective ⇑g

If a composite with a proper module quotient is surjective and the intermediate target is projective with local endomorphism ring, then the original map is surjective.

theorem MagnitudeConjecture.jacobson_isCoatom_of_projective_local_end {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Nontrivial P] [Module.Finite R P] [Module.Projective R P] [IsLocalRing (Module.End R P)] : IsCoatom (Module.jacobson R P)

A finite projective module with local endomorphism ring has a unique maximal submodule, namely its module Jacobson radical.

def MagnitudeConjecture.fgModuleRadical {R : Type u} [Ring R] [IsNoetherianRing R] (P : FGModuleCat R) : FGModuleCat R

The module Jacobson radical of an arbitrary finitely generated module, retained in the finitely generated module category.

def MagnitudeConjecture.fgModuleRadicalInclusion {R : Type u} [Ring R] [IsNoetherianRing R] (P : FGModuleCat R) : fgModuleRadical P ⟶ P

The canonical inclusion of the module Jacobson radical into a finitely generated module.

theorem MagnitudeConjecture.fgModuleRadicalInclusion_isRightAlmostSplit {R : Type u} [Ring R] [IsNoetherianRing R] (P : FGModuleCat R) (hP : CategoryTheory.Projective P) [Nontrivial ↑P] [IsLocalRing (Module.End R ↑P)] : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (fgModuleRadicalInclusion P)

For a nonzero projective with local module endomorphism ring, the radical inclusion is right almost split.

theorem MagnitudeConjecture.fgModuleRadicalInclusion_isRightMinimal {R : Type u} [Ring R] [IsNoetherianRing R] (P : FGModuleCat R) : QuotientSubmoduleEquidistribution.IsRightMinimal (fgModuleRadicalInclusion P)

The radical inclusion of any finitely generated module is right minimal.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveBoundaryRadical {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) : FinitelyGeneratedCategory A

The module Jacobson radical of a chosen right-module representative.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveBoundaryRadicalInclusion {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) : S.projectiveBoundaryRadical p ⟶ S.fgObj p

The canonical inclusion rad P ⟶ P.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveBoundary_jacobson_isCoatom {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : IsCoatom (Module.jacobson Aᵐᵒᵖ ↑(S.fgObj p))

The Jacobson radical of a selected indecomposable projective is its unique maximal submodule.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveBoundaryRadicalInclusion_isRightAlmostSplit {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.projectiveBoundaryRadicalInclusion p)

The radical inclusion of an indecomposable projective is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveBoundaryRadicalInclusion_isRightMinimal {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.projectiveBoundaryRadicalInclusion p)

The projective-boundary radical inclusion is right minimal.