Uniserial essential extensions

A simple essential subobject is contained in every nonzero subobject. Hence, if the quotient by that subobject is uniserial, the whole object is uniserial. This is the categorical induction step for an ascending socle series.

noncomputable def MagnitudeConjecture.cokernelInclusionOfComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] : CategoryTheory.Limits.cokernel r ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp r l)

The inclusion of the first quotient in the quotient by a composite monomorphism.

instance MagnitudeConjecture.cokernelInclusionOfComp_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] : CategoryTheory.Mono (cokernelInclusionOfComp r l)

theorem MagnitudeConjecture.cokernel_π_comp_cokernelInclusionOfComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π r) (cokernelInclusionOfComp r l) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp r l))

theorem MagnitudeConjecture.cokernel_π_comp_cokernelInclusionOfComp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] {Z : C} (h : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp r l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π r) (CategoryTheory.CategoryStruct.comp (cokernelInclusionOfComp r l) h) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp r l)) h)

noncomputable def MagnitudeConjecture.cokernelTowerDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] : CategoryTheory.Limits.cokernel (cokernelInclusionOfComp r l) ⟶ CategoryTheory.Limits.cokernel l

Collapsing the two successive quotients by R ⊆ H gives the direct quotient by H.

theorem MagnitudeConjecture.cokernel_π_comp_cokernel_π_comp_cokernelTowerDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp r l)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (cokernelInclusionOfComp r l)) (cokernelTowerDesc r l)) = CategoryTheory.Limits.cokernel.π l

theorem MagnitudeConjecture.cokernel_π_comp_cokernel_π_comp_cokernelTowerDesc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] {Z : C} (h : CategoryTheory.Limits.cokernel l ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp r l)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (cokernelInclusionOfComp r l)) (CategoryTheory.CategoryStruct.comp (cokernelTowerDesc r l) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π l) h

theorem MagnitudeConjecture.comp_cokernel_π_eq_of_comp_cokernelTower_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H G P : C} (r : R ⟶ H) [CategoryTheory.Mono r] (l : H ⟶ G) [CategoryTheory.Mono l] (f g : P ⟶ G) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp r l))) (CategoryTheory.Limits.cokernel.π (cokernelInclusionOfComp r l)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp r l))) (CategoryTheory.Limits.cokernel.π (cokernelInclusionOfComp r l))) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π l) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π l)

Equality after the two successive quotients by R ⊆ H descends to equality after the direct quotient by H.

theorem MagnitudeConjecture.cokernel_π_comp_eqToIso_of_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f g : X ⟶ Y} (h : f = g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.eqToIso ⋯).hom = CategoryTheory.Limits.cokernel.π g

The quotient map commutes with the canonical transport between cokernels of equal morphisms.

theorem MagnitudeConjecture.cokernel_π_comp_eqToIso_of_eq_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f g : X ⟶ Y} (h : f = g) {Z : C} (h✝ : CategoryTheory.Limits.cokernel g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToIso ⋯).hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) h✝

The quotient map commutes with the canonical transport between cokernels of equal morphisms.

def MagnitudeConjecture.IsUniserialObject.IsWaistSubobject {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : CategoryTheory.Subobject X) : Prop

A subobject is a waist when it is comparable with every subobject of the ambient object. Successive terms of an ascending uniserial socle series have this stronger ambient property.

theorem MagnitudeConjecture.IsUniserialObject.isEssentialMono_of_comp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (e : Y ≅ Z) (h : IsEssentialMono (CategoryTheory.CategoryStruct.comp f e.hom)) : IsEssentialMono f

Essentiality is unchanged by composing the target with an isomorphism.

theorem MagnitudeConjecture.IsUniserialObject.of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.Simple X] : IsUniserialObject X

A simple object is uniserial.

theorem MagnitudeConjecture.IsUniserialObject.simple_le_nonzero_subobject_of_essential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} [CategoryTheory.Simple L] (l : L ⟶ X) [CategoryTheory.Mono l] (hl : IsEssentialMono l) (P : CategoryTheory.Subobject X) (hP : P ≠ ⊥) : CategoryTheory.Subobject.mk l ≤ P

A nonzero subobject of an essential extension of a simple object contains that simple subobject.

theorem MagnitudeConjecture.IsUniserialObject.isWaistSubobject_of_simple_essential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} [CategoryTheory.Simple L] (l : L ⟶ X) [CategoryTheory.Mono l] (hl : IsEssentialMono l) : IsWaistSubobject (CategoryTheory.Subobject.mk l)

A simple essential subobject is a waist in its ambient object.

theorem MagnitudeConjecture.IsUniserialObject.isWaistSubobject_of_essentialSimpleTop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R H X : C} (r : R ⟶ H) [CategoryTheory.Mono r] (m : H ⟶ X) [CategoryTheory.Mono m] (hR : IsWaistSubobject (CategoryTheory.Subobject.mk (CategoryTheory.CategoryStruct.comp r m))) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel r)] (ht : IsEssentialMono (cokernelInclusionOfComp r m)) : IsWaistSubobject (CategoryTheory.Subobject.mk m)

A waist remains a waist after adjoining a simple layer which is essential in the quotient by the old waist. This is the abstract propagation step for an ascending uniserial socle series.

theorem MagnitudeConjecture.IsUniserialObject.isWaistSubobject_restrict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L H X : C} (a : L ⟶ H) [CategoryTheory.Mono a] (m : H ⟶ X) [CategoryTheory.Mono m] (hL : IsWaistSubobject (CategoryTheory.Subobject.mk (CategoryTheory.CategoryStruct.comp a m))) : IsWaistSubobject (CategoryTheory.Subobject.mk a)

Restricting an ambient waist to an intermediate subobject preserves the waist property.

theorem MagnitudeConjecture.IsUniserialObject.essential_restrict_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L H X : C} [CategoryTheory.Simple L] (l : L ⟶ X) [CategoryTheory.Mono l] (hl : IsEssentialMono l) (a : L ⟶ H) [CategoryTheory.Mono a] (m : H ⟶ X) [CategoryTheory.Mono m] (ham : CategoryTheory.CategoryStruct.comp a m = l) : IsEssentialMono a

A simple essential subobject remains essential in every intermediate subobject through which its inclusion factors.

theorem MagnitudeConjecture.IsUniserialObject.of_essential_simple_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} [CategoryTheory.Simple L] (l : L ⟶ X) (hl : IsEssentialMono l) (hQ : IsUniserialObject (CategoryTheory.Limits.cokernel l)) : IsUniserialObject X

A simple essential subobject with uniserial cokernel has uniserial ambient object.

theorem MagnitudeConjecture.IsUniserialObject.isRadicalSubobject_of_waist_simple_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} (l : L ⟶ X) [CategoryTheory.Mono l] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] (hl : IsWaistSubobject (CategoryTheory.Subobject.mk l)) : IsRadicalSubobject (CategoryTheory.Subobject.mk l)

A waist subobject with simple cokernel is the unique maximal subobject and hence contains every proper subobject.

theorem MagnitudeConjecture.IsUniserialObject.isRadicalSubobject_of_uniserial_simple_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} (hX : IsUniserialObject X) (l : L ⟶ X) [CategoryTheory.Mono l] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] : IsRadicalSubobject (CategoryTheory.Subobject.mk l)

In a uniserial object, a subobject with simple cokernel is the unique maximal subobject and hence contains every proper subobject.

theorem MagnitudeConjecture.IsUniserialObject.of_waist_simple_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} (hL : IsUniserialObject L) (l : L ⟶ X) [CategoryTheory.Mono l] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] (hl : IsWaistSubobject (CategoryTheory.Subobject.mk l)) : IsUniserialObject X

Extending a uniserial object across a waist inclusion with simple cokernel again gives a uniserial object.

theorem MagnitudeConjecture.IsUniserialObject.isRadicalSubobject_of_essential_simple_cokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L X : C} [CategoryTheory.Simple L] (l : L ⟶ X) [CategoryTheory.Mono l] (hl : IsEssentialMono l) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] : IsRadicalSubobject (CategoryTheory.Subobject.mk l)

A simple essential subobject with simple quotient contains every proper subobject of its ambient object.

theorem MagnitudeConjecture.CoveringHom.moduleTotalDimension_lt_of_epi_not_isIso {k : Type uK} [Field k] {D : Type uC} [CategoryTheory.Category.{uK, uC} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (M N : FiniteDimensionalModuleCategory k) (p : M ⟶ N) [CategoryTheory.Epi p] (hp : ¬CategoryTheory.IsIso p) : moduleTotalDimension N < moduleTotalDimension M

A proper quotient of a finite module has strictly smaller total pointwise dimension.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_isUniserial_of_essentialSimpleCokernelSuccessors {k : Type uK} [Field k] {D : Type uC} [CategoryTheory.Category.{uK, uC} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (Good : FiniteDimensionalModuleCategory k → Prop) (hsuccessor : ∀ (F : FiniteDimensionalModuleCategory k), Good F → ¬CategoryTheory.Limits.IsZero F → ∃ (L : FiniteDimensionalModuleCategory k) (l : L ⟶ F), CategoryTheory.Simple L ∧ CategoryTheory.Mono l ∧ IsEssentialMono l ∧ Good (CategoryTheory.Limits.cokernel l)) (F : FiniteDimensionalModuleCategory k) (hF : Good F) : IsUniserialObject F

Finite ascending-socle induction. If every nonzero object in a class has a simple essential subobject whose cokernel remains in the class, then every object in the class is uniserial.