Facts about epimorphisms and monomorphisms.

The definitions of Epi and Mono are in CategoryTheory.Category, since they are used by some lemmas for Iso, which is used everywhere.

instance CategoryTheory.unop_mono_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {A B : Cᵒᵖ} (f : A ⟶ B) [Epi f] : Mono f.unop

instance CategoryTheory.unop_epi_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {A B : Cᵒᵖ} (f : A ⟶ B) [Mono f] : Epi f.unop

instance CategoryTheory.op_mono_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) [Epi f] : Mono f.op

instance CategoryTheory.op_epi_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) [Mono f] : Epi f.op

structure CategoryTheory.SplitMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Type v₁

A split monomorphism is a morphism f : X ⟶ Y with a given retraction retraction f : Y ⟶ X such that f ≫ retraction f = 𝟙 X.

Every split monomorphism is a monomorphism.

• retraction : Y ⟶ X

  The map splitting f

• id : CategoryStruct.comp f self.retraction = CategoryStruct.id X

  f composed with retraction is the identity

theorem CategoryTheory.SplitMono.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : SplitMono f} (retraction : x.retraction = y.retraction) : x = y

@[simp]

theorem CategoryTheory.SplitMono.id_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : SplitMono f) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp self.retraction h) = h

class CategoryTheory.IsSplitMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop

IsSplitMono f is the assertion that f admits a retraction

• exists_splitMono : Nonempty (SplitMono f)

  There is a splitting

def CategoryTheory.SplitMono.comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (smf : SplitMono f) (smg : SplitMono g) : SplitMono (CategoryStruct.comp f g)

A composition of SplitMono is a SplitMono. -

Equations

• smf.comp smg = { retraction := CategoryTheory.CategoryStruct.comp smg.retraction smf.retraction, id := ⋯ }

@[simp]

theorem CategoryTheory.SplitMono.comp_retraction {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (smf : SplitMono f) (smg : SplitMono g) : (smf.comp smg).retraction = CategoryStruct.comp smg.retraction smf.retraction

theorem CategoryTheory.IsSplitMono.mk' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : IsSplitMono f

A constructor for IsSplitMono f taking a SplitMono f as an argument

structure CategoryTheory.SplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Type v₁

A split epimorphism is a morphism f : X ⟶ Y with a given section section_ f : Y ⟶ X such that section_ f ≫ f = 𝟙 Y. (Note that section is a reserved keyword, so we append an underscore.)

Every split epimorphism is an epimorphism.

• section_ : Y ⟶ X

  The map splitting f

• id : CategoryStruct.comp self.section_ f = CategoryStruct.id Y

  section_ composed with f is the identity

theorem CategoryTheory.SplitEpi.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : SplitEpi f} (section_ : x.section_ = y.section_) : x = y

@[simp]

theorem CategoryTheory.SplitEpi.id_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : SplitEpi f) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp self.section_ (CategoryStruct.comp f h) = h

class CategoryTheory.IsSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop

IsSplitEpi f is the assertion that f admits a section

• exists_splitEpi : Nonempty (SplitEpi f)

  There is a splitting

def CategoryTheory.SplitEpi.comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (sef : SplitEpi f) (seg : SplitEpi g) : SplitEpi (CategoryStruct.comp f g)

A composition of SplitEpi is a split SplitEpi. -

Equations

• sef.comp seg = { section_ := CategoryTheory.CategoryStruct.comp seg.section_ sef.section_, id := ⋯ }

@[simp]

theorem CategoryTheory.SplitEpi.comp_section_ {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (sef : SplitEpi f) (seg : SplitEpi g) : (sef.comp seg).section_ = CategoryStruct.comp seg.section_ sef.section_

theorem CategoryTheory.IsSplitEpi.mk' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : IsSplitEpi f

A constructor for IsSplitEpi f taking a SplitEpi f as an argument

noncomputable def CategoryTheory.retraction {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Y ⟶ X

The chosen retraction of a split monomorphism.

Equations

• CategoryTheory.retraction f = ⋯.some.retraction

@[simp]

theorem CategoryTheory.IsSplitMono.id {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : CategoryStruct.comp f (retraction f) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.IsSplitMono.id_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (retraction f) h) = h

def CategoryTheory.SplitMono.splitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : SplitEpi sm.retraction

The retraction of a split monomorphism has an obvious section.

Equations

• sm.splitEpi = { section_ := f, id := ⋯ }

instance CategoryTheory.retraction_isSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsSplitEpi (retraction f)

The retraction of a split monomorphism is itself a split epimorphism.

theorem CategoryTheory.isIso_of_epi_of_isSplitMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] [Epi f] : IsIso f

A split mono which is epi is an iso.

noncomputable def CategoryTheory.section_ {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Y ⟶ X

The chosen section of a split epimorphism. (Note that section is a reserved keyword, so we append an underscore.)

Equations

• CategoryTheory.section_ f = ⋯.some.section_

@[simp]

theorem CategoryTheory.IsSplitEpi.id {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : CategoryStruct.comp (section_ f) f = CategoryStruct.id Y

@[simp]

theorem CategoryTheory.IsSplitEpi.id_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (section_ f) (CategoryStruct.comp f h) = h

def CategoryTheory.SplitEpi.splitMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : SplitMono se.section_

The section of a split epimorphism has an obvious retraction.

Equations

• se.splitMono = { retraction := f, id := ⋯ }

instance CategoryTheory.section_isSplitMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsSplitMono (section_ f)

The section of a split epimorphism is itself a split monomorphism.

theorem CategoryTheory.isIso_of_mono_of_isSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] [IsSplitEpi f] : IsIso f

A split epi which is mono is an iso.

@[instance 100]

instance CategoryTheory.IsSplitMono.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitMono f

Every iso is a split mono.

@[instance 100]

instance CategoryTheory.IsSplitEpi.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitEpi f

Every iso is a split epi.

theorem CategoryTheory.SplitMono.mono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : Mono f

@[instance 100]

instance CategoryTheory.IsSplitMono.mono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Mono f

Every split mono is a mono.

theorem CategoryTheory.SplitEpi.epi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : Epi f

@[instance 100]

instance CategoryTheory.IsSplitEpi.epi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Epi f

Every split epi is an epi.

instance CategoryTheory.instIsSplitMonoComp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitMono f] [hg : IsSplitMono g] : IsSplitMono (CategoryStruct.comp f g)

instance CategoryTheory.instIsSplitEpiComp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitEpi f] [hg : IsSplitEpi g] : IsSplitEpi (CategoryStruct.comp f g)

theorem CategoryTheory.IsIso.of_mono_retraction' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : SplitMono f) [Mono hf.retraction] : IsIso f

Every split mono whose retraction is mono is an iso.

theorem CategoryTheory.IsIso.of_mono_retraction {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] [hf' : Mono (retraction f)] : IsIso f

Every split mono whose retraction is mono is an iso.

theorem CategoryTheory.IsIso.of_epi_section' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : SplitEpi f) [Epi hf.section_] : IsIso f

Every split epi whose section is epi is an iso.

theorem CategoryTheory.IsIso.of_epi_section {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] [hf' : Epi (section_ f)] : IsIso f

Every split epi whose section is epi is an iso.

noncomputable def CategoryTheory.Groupoid.ofTruncSplitMono {C : Type u₁} [Category.{v₁, u₁} C] (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)) : Groupoid C

A category where every morphism has a Trunc retraction is computably a groupoid.

Equations

• CategoryTheory.Groupoid.ofTruncSplitMono all_split_mono = CategoryTheory.Groupoid.ofIsIso ⋯

class CategoryTheory.SplitMonoCategory (C : Type u₁) [Category.{v₁, u₁} C] : Prop

A split mono category is a category in which every monomorphism is split.

• isSplitMono_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f

  All monos are split

class CategoryTheory.SplitEpiCategory (C : Type u₁) [Category.{v₁, u₁} C] : Prop

A split epi category is a category in which every epimorphism is split.

• isSplitEpi_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f

  All epis are split

theorem CategoryTheory.isSplitMono_of_mono {C : Type u₁} [Category.{v₁, u₁} C] [SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f

In a category in which every monomorphism is split, every monomorphism splits. This is not an instance because it would create an instance loop.

theorem CategoryTheory.isSplitEpi_of_epi {C : Type u₁} [Category.{v₁, u₁} C] [SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f

In a category in which every epimorphism is split, every epimorphism splits. This is not an instance because it would create an instance loop.

def CategoryTheory.SplitMono.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) (F : Functor C D) : SplitMono (F.map f)

Split monomorphisms are also absolute monomorphisms.

Equations

• sm.map F = { retraction := F.map sm.retraction, id := ⋯ }

@[simp]

theorem CategoryTheory.SplitMono.map_retraction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) (F : Functor C D) : (sm.map F).retraction = F.map sm.retraction

def CategoryTheory.SplitEpi.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) (F : Functor C D) : SplitEpi (F.map f)

Split epimorphisms are also absolute epimorphisms.

Equations

• se.map F = { section_ := F.map se.section_, id := ⋯ }

@[simp]

theorem CategoryTheory.SplitEpi.map_section_ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) (F : Functor C D) : (se.map F).section_ = F.map se.section_

instance CategoryTheory.instIsSplitMonoMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] (F : Functor C D) : IsSplitMono (F.map f)

instance CategoryTheory.instIsSplitEpiMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] (F : Functor C D) : IsSplitEpi (F.map f)