Projective factorizations from indecomposable nonprojectives

This file isolates the second elementary module-theoretic ingredient in Auslander--Reiten, Proposition 1.1(a). A map from an indecomposable nonprojective finite module into a finite projective has radical image.

theorem MagnitudeConjecture.range_le_jacobson_of_map_to_fgProjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X P : RightModule.FinitelyGeneratedCategory A} (hX : CategoryTheory.Indecomposable X) (hXnonprojective : ¬CategoryTheory.Projective X) (hP : CategoryTheory.Projective P) (f : X ⟶ P) : (ModuleCat.Hom.hom f.hom).range ≤ Module.jacobson Aᵐᵒᵖ ↑P

A map from an indecomposable nonprojective finitely generated module to a finite projective module has image in the target radical.

theorem MagnitudeConjecture.range_le_jacobson_of_factorsThroughProjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : RightModule.FinitelyGeneratedCategory A} (hX : CategoryTheory.Indecomposable X) (hXnonprojective : ¬CategoryTheory.Projective X) {f : X ⟶ Y} (hfactor : ProjectiveStable.FactorsThroughProjective f.hom) : (ModuleCat.Hom.hom f.hom).range ≤ Module.jacobson Aᵐᵒᵖ ↑Y

A map from an indecomposable nonprojective finitely generated module which factors through an arbitrary projective in the ambient module category has radical image. The ambient factorization is first lifted through a finite free epimorphism onto the target.