Radical subobjects from projective covers

A monic right almost-split morphism represents the unique maximal subobject of its target. If such a subobject is mapped through a minimal projective cover, its image contains every proper subobject of the cover target and is itself proper. This is the intrinsic projective-cover description of the module radical used in the covering argument.

theorem MagnitudeConjecture.isRadicalSubobject_mk_of_mono_rightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] {R P : C} (r : R ⟶ P) [CategoryTheory.Mono r] (hr : QuotientSubmoduleEquidistribution.IsRightAlmostSplit r) : IsUniserialObject.IsRadicalSubobject (CategoryTheory.Subobject.mk r)

A monic right almost-split morphism represents a subobject containing every proper subobject of its target.

theorem MagnitudeConjecture.mk_ne_top_of_mono_rightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] {R P : C} (r : R ⟶ P) [CategoryTheory.Mono r] (hr : QuotientSubmoduleEquidistribution.IsRightAlmostSplit r) : CategoryTheory.Subobject.mk r ≠ ⊤

The subobject represented by a monic right almost-split morphism is proper.

theorem MagnitudeConjecture.isCoatom_mk_of_mono_rightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] {R P : C} (r : R ⟶ P) [CategoryTheory.Mono r] (hr : QuotientSubmoduleEquidistribution.IsRightAlmostSplit r) : IsCoatom (CategoryTheory.Subobject.mk r)

A monic right almost-split morphism represents a maximal proper subobject.

theorem MagnitudeConjecture.simple_cokernel_of_isRadicalSubobject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R X : C} (r : R ⟶ X) [CategoryTheory.Mono r] (hr : IsUniserialObject.IsRadicalSubobject (CategoryTheory.Subobject.mk r)) (hproper : CategoryTheory.Subobject.mk r ≠ ⊤) : CategoryTheory.Simple (CategoryTheory.Limits.cokernel r)

A proper radical subobject has simple quotient. Indeed, it is a coatom in the subobject lattice, hence its quotient is an atom under the abelian subobject--quotient order duality.

theorem MagnitudeConjecture.imageSubobject_pullback_arrow_comp_eq_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P M : C} (p : P ⟶ M) [CategoryTheory.Epi p] (S : CategoryTheory.Subobject M) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Subobject.pullback p).obj S).arrow p) = S

The image of the inverse image of a subobject along an epimorphism is the original subobject.

theorem MagnitudeConjecture.isRadicalSubobject_imageSubobject_comp_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R P M : C} (r : R ⟶ P) [CategoryTheory.Mono r] (p : P ⟶ M) [CategoryTheory.Epi p] (hr : IsUniserialObject.IsRadicalSubobject (CategoryTheory.Subobject.mk r)) : IsUniserialObject.IsRadicalSubobject (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp r p))

If a subobject contains every proper subobject of the source of an epimorphism, then its image contains every proper subobject of the target.

theorem MagnitudeConjecture.imageSubobject_comp_ne_top_of_isEssentialEpi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R P M : C} (r : R ⟶ P) [CategoryTheory.Mono r] (p : P ⟶ M) [CategoryTheory.Epi p] (hp : IsEssentialEpi p) (hr : CategoryTheory.Subobject.mk r ≠ ⊤) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp r p) ≠ ⊤

Under an essential epimorphism, the image of a proper subobject remains proper.

theorem MagnitudeConjecture.MinimalProjectivePresentation.source_indecomposable_of_uniserial {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {M : C} (P : MinimalProjectivePresentation M) (hM : IsUniserialObject M) (hMzero : ¬CategoryTheory.Limits.IsZero M) : CategoryTheory.Indecomposable P.p

A minimal projective cover of a nonzero uniserial object has indecomposable source.