Minimal morphisms #
The standard right- and left-minimal predicates are useful both for almost-split morphisms and for minimal weak kernels and cokernels.
def
QuotientSubmoduleEquidistribution.IsRightMinimal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
A morphism is right minimal when every endomorphism of its source which fixes it is invertible.
Instances For
def
QuotientSubmoduleEquidistribution.IsLeftMinimal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
A morphism is left minimal when every endomorphism of its target which fixes it is invertible.
Instances For
theorem
QuotientSubmoduleEquidistribution.isIso_of_isIso_comp_both
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
(a : X ⟶ Y)
(b : Y ⟶ X)
[CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp a b)]
[CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp b a)]
:
CategoryTheory.IsIso a
A morphism whose composites with one reverse morphism are invertible in both orders is itself invertible.
theorem
QuotientSubmoduleEquidistribution.isRightMinimal_of_localEnd_of_ne_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
[IsLocalRing (CategoryTheory.End X)]
(f : X ⟶ Y)
(hf : f ≠ 0)
:
Every nonzero morphism out of an object with local endomorphism ring is right minimal.
theorem
QuotientSubmoduleEquidistribution.IsRightMinimal.postcomp_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y Z : C}
{g : X ⟶ Y}
(e : Y ≅ Z)
(hg : IsRightMinimal g)
:
IsRightMinimal (CategoryTheory.CategoryStruct.comp g e.hom)
Postcomposing by an isomorphism preserves right minimality.
theorem
QuotientSubmoduleEquidistribution.IsRightMinimal.precomp_splitMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{Z X Y : C}
{g : X ⟶ Y}
(hg : IsRightMinimal g)
(j : Z ⟶ X)
[CategoryTheory.IsSplitMono j]
:
IsRightMinimal (CategoryTheory.CategoryStruct.comp j g)
Precomposing a right-minimal morphism by a split monomorphism preserves right minimality.