Uniqueness and transport of minimal almost-split morphisms

Minimal right almost-split morphisms with a common target have isomorphic sources, and minimal left almost-split morphisms with a common source have isomorphic targets. This file also records the isomorphism-transport and kernel/cokernel consequences used to identify Auslander--Reiten translates inside a chosen indecomposable skeleton.

theorem QuotientSubmoduleEquidistribution.exists_rightAlmostSplit_middleIso {C : Type u} [CategoryTheory.Category.{v, u} C] {E E' Z : C} {f : E ⟶ Z} {g : E' ⟶ Z} (hf : IsRightAlmostSplit f) (hfmin : IsRightMinimal f) (hg : IsRightAlmostSplit g) (hgmin : IsRightMinimal g) : ∃ (e : E ≅ E'), CategoryTheory.CategoryStruct.comp e.hom g = f

Minimal right almost-split morphisms with the same target have isomorphic sources, compatibly with their structure maps.

theorem QuotientSubmoduleEquidistribution.exists_leftAlmostSplit_middleIso {C : Type u} [CategoryTheory.Category.{v, u} C] {Z E E' : C} {f : Z ⟶ E} {g : Z ⟶ E'} (hf : IsLeftAlmostSplit f) (hfmin : IsLeftMinimal f) (hg : IsLeftAlmostSplit g) (hgmin : IsLeftMinimal g) : ∃ (e : E ≅ E'), CategoryTheory.CategoryStruct.comp f e.hom = g

Minimal left almost-split morphisms with the same source have isomorphic targets, compatibly with their structure maps.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.precomp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X' X E : C} (i : X' ≅ X) {f : X ⟶ E} (hf : IsLeftAlmostSplit f) : IsLeftAlmostSplit (CategoryTheory.CategoryStruct.comp i.hom f)

Precomposition by an isomorphism preserves left almost-splitness.

theorem QuotientSubmoduleEquidistribution.IsLeftMinimal.precomp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X' X E : C} (i : X' ≅ X) {f : X ⟶ E} (hf : IsLeftMinimal f) : IsLeftMinimal (CategoryTheory.CategoryStruct.comp i.hom f)

Precomposition by an isomorphism preserves left minimality.

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

Postcomposition by an isomorphism preserves right almost-splitness.

theorem QuotientSubmoduleEquidistribution.nonempty_kernelIso_of_rightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] {E E' Z : C} {f : E ⟶ Z} {g : E' ⟶ Z} (hf : IsRightAlmostSplit f) (hfmin : IsRightMinimal f) (hg : IsRightAlmostSplit g) (hgmin : IsRightMinimal g) : Nonempty (CategoryTheory.Limits.kernel f ≅ CategoryTheory.Limits.kernel g)

Uniqueness of a minimal right almost-split map identifies its kernels.

theorem QuotientSubmoduleEquidistribution.nonempty_cokernelIso_of_leftAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasCokernels C] {Z E E' : C} {f : Z ⟶ E} {g : Z ⟶ E'} (hf : IsLeftAlmostSplit f) (hfmin : IsLeftMinimal f) (hg : IsLeftAlmostSplit g) (hgmin : IsLeftMinimal g) : Nonempty (CategoryTheory.Limits.cokernel f ≅ CategoryTheory.Limits.cokernel g)

Uniqueness of a minimal left almost-split map identifies its cokernels.

noncomputable def QuotientSubmoduleEquidistribution.cokernelKernelIsoTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.ι f) ≅ Y

The canonical cokernel of the kernel inclusion of an epimorphism is isomorphic to its target.

noncomputable def QuotientSubmoduleEquidistribution.kernelCokernelIsoSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.π f) ≅ X

Dually, the canonical kernel of the cokernel projection of a monomorphism is isomorphic to its source.