Cokernels of minimal left almost-split monomorphisms

This file derives the cokernel half of the abstract Auslander--Reiten sequence theorem from the already-vendored kernel half by passage to the opposite category. Keeping the transport explicit avoids duplicating the pushout argument used for kernels.

theorem MagnitudeConjecture.CategoryTheory.leftAlmostSplit_op {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f.op

A left almost-split morphism becomes right almost split after taking its opposite.

theorem MagnitudeConjecture.CategoryTheory.leftAlmostSplit_unop {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f.unop

A left almost-split morphism in an opposite category becomes right almost split after taking its underlying morphism.

theorem MagnitudeConjecture.CategoryTheory.leftMinimal_op {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsLeftMinimal f) : QuotientSubmoduleEquidistribution.IsRightMinimal f.op

Left minimality becomes right minimality on the opposite morphism.

theorem MagnitudeConjecture.CategoryTheory.rightAlmostSplit_precomp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {E' E Z : C} (i : E' ≅ E) {f : E ⟶ Z} (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.CategoryStruct.comp i.hom f)

Precomposition by an isomorphism preserves right almost-splitness.

theorem MagnitudeConjecture.CategoryTheory.leftAlmostSplit_epi_of_injective_source {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Injective X] (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (hmin : QuotientSubmoduleEquidistribution.IsLeftMinimal f) : CategoryTheory.Epi f

A left-minimal left almost-split morphism with injective source is epic.

theorem MagnitudeConjecture.CategoryTheory.rightAlmostSplit_mono_of_projective_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Projective Y] (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) : CategoryTheory.Mono f

A right-minimal right almost-split morphism with projective target is monic.

theorem MagnitudeConjecture.CategoryTheory.simple_cokernel_of_mono_rightAlmostSplit_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R P : C} (r : R ⟶ P) [CategoryTheory.Mono r] [CategoryTheory.Projective P] (hr : QuotientSubmoduleEquidistribution.IsRightAlmostSplit r) : CategoryTheory.Simple (CategoryTheory.Limits.cokernel r)

The cokernel of a monic right almost-split morphism into a projective object is simple. This is the abstract projective-boundary case of an almost-split sequence.

theorem MagnitudeConjecture.CategoryTheory.simple_unop_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : Cᵒᵖ} [CategoryTheory.Simple X] : CategoryTheory.Simple (Opposite.unop X)

Simplicity descends from an object of an opposite abelian category to its underlying object.

theorem MagnitudeConjecture.CategoryTheory.simple_kernel_of_epi_leftAlmostSplit_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {I R : C} (r : I ⟶ R) [CategoryTheory.Epi r] [CategoryTheory.Injective I] (hr : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit r) : CategoryTheory.Simple (CategoryTheory.Limits.kernel r)

The kernel of an epic left almost-split morphism out of an injective object is simple. This is the injective-boundary dual of simple_cokernel_of_mono_rightAlmostSplit_projective.

noncomputable def MagnitudeConjecture.CategoryTheory.cokernelIsoSimpleTarget_of_mono_rightAlmostSplit_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R P S : C} (r : R ⟶ P) [CategoryTheory.Mono r] [CategoryTheory.Projective P] [IsLocalRing (CategoryTheory.End P)] (hr : QuotientSubmoduleEquidistribution.IsRightAlmostSplit r) [CategoryTheory.Simple S] (p : P ⟶ S) (hp : p ≠ 0) : CategoryTheory.Limits.cokernel r ≅ S

If the projective target of a monic right almost-split morphism has local endomorphism ring, every nonzero morphism from it to a simple object exhibits that simple as the cokernel.

theorem MagnitudeConjecture.CategoryTheory.projective_of_mono_rightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : CategoryTheory.Projective Y

In an abelian category with enough projectives, a monic right almost-split morphism has projective target.

theorem MagnitudeConjecture.CategoryTheory.IsRightAlmostSplit.epi_of_not_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] {X Y : C} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hY : ¬CategoryTheory.Projective Y) : CategoryTheory.Epi f

In a category with enough projectives, a right almost-split map ending at a nonprojective object is epic.

theorem MagnitudeConjecture.CategoryTheory.leftAlmostSplit_cokernel_π_isRightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (hmin : QuotientSubmoduleEquidistribution.IsLeftMinimal f) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.Limits.cokernel.π f)

The cokernel projection of a left-minimal left almost-split monomorphism is right almost split.