Almost-split morphisms in short exact sequences

This file records three intrinsic facts used to rotate the density-free push-down theorem. A right almost-split morphism has indecomposable target; a radical kernel map in a short exact sequence makes the quotient map right minimal; and a right-minimal right almost-split quotient makes the displayed kernel map left almost split.

theorem MagnitudeConjecture.CategoryTheory.IsRightAlmostSplit.target_indecomposable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E Z : C} (f : E ⟶ Z) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : CategoryTheory.Indecomposable Z

The target of a right almost-split morphism is indecomposable in any preadditive category with binary biproducts.

theorem MagnitudeConjecture.CategoryTheory.isWeakKernel_map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hS : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel S) (E : C ≌ D) : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel (S.map E.functor)

An equivalence transports a weak-kernel diagram.

noncomputable def MagnitudeConjecture.CategoryTheory.isLimit_kernelFork_of_isWeakKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hS : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel S) [CategoryTheory.Mono S.f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)

A monic weak kernel is an actual kernel.

theorem MagnitudeConjecture.CategoryTheory.IsLeftAlmostSplit.comp_factorThruImage_of_comp_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {M E : C} (f : M ⟶ E) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (e : E ⟶ E) (he : CategoryTheory.CategoryStruct.comp f e = f) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.factorThruImage e))

If a target endomorphism fixes a left almost-split morphism, then factoring that morphism through the endomorphism's image remains left almost split.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.isRightMinimal_g_of_isRadicalMorphism_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism S.f) : QuotientSubmoduleEquidistribution.IsRightMinimal S.g

In a short exact sequence, a radical kernel map makes the quotient map right minimal.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.isRightMinimal_g_of_local_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [IsLocalRing (CategoryTheory.End S.X₁)] (hg : ¬CategoryTheory.IsSplitEpi S.g) : QuotientSubmoduleEquidistribution.IsRightMinimal S.g

A nonsplit epimorphism in a short exact sequence whose kernel has local endomorphism ring is right minimal.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.isLeftAlmostSplit_f_of_rightAlmostSplit_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g) (hmin : QuotientSubmoduleEquidistribution.IsRightMinimal S.g) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit S.f

A right-minimal right almost-split quotient in a short exact sequence makes its displayed kernel map left almost split.