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₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : Cᵒᵖ} (f : A ⟶ B) [CategoryTheory.Epi f] : CategoryTheory.Mono f.unop

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

structure CategoryTheory.SplitMono {C : Type u₁} [CategoryTheory.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 : CategoryTheory.CategoryStruct.comp f self.retraction = CategoryTheory.CategoryStruct.id X

  f composed with retraction is the identity

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

@[simp]

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

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

IsSplitMono f is the assertion that f admits a retraction

• exists_splitMono : Nonempty (CategoryTheory.SplitMono f)

  There is a splitting

def CategoryTheory.SplitMono.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (smf : CategoryTheory.SplitMono f) (smg : CategoryTheory.SplitMono g) : CategoryTheory.SplitMono (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (smf : CategoryTheory.SplitMono f) (smg : CategoryTheory.SplitMono g) : (smf.comp smg).retraction = CategoryTheory.CategoryStruct.comp smg.retraction smf.retraction

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

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

structure CategoryTheory.SplitEpi {C : Type u₁} [CategoryTheory.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 : CategoryTheory.CategoryStruct.comp self.section_ f = CategoryTheory.CategoryStruct.id Y

  section_ composed with f is the identity

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

@[simp]

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

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

IsSplitEpi f is the assertion that f admits a section

• exists_splitEpi : Nonempty (CategoryTheory.SplitEpi f)

  There is a splitting

def CategoryTheory.SplitEpi.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (sef : CategoryTheory.SplitEpi f) (seg : CategoryTheory.SplitEpi g) : CategoryTheory.SplitEpi (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (sef : CategoryTheory.SplitEpi f) (seg : CategoryTheory.SplitEpi g) : (sef.comp seg).section_ = CategoryTheory.CategoryStruct.comp seg.section_ sef.section_

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

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

noncomputable def CategoryTheory.retraction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitMono f] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.retraction f) = CategoryTheory.CategoryStruct.id X

@[simp]

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

def CategoryTheory.SplitMono.splitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (sm : CategoryTheory.SplitMono f) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsSplitEpi (CategoryTheory.retraction f)

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

Equations

• ⋯ = ⋯

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

A split mono which is epi is an iso.

noncomputable def CategoryTheory.section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) f = CategoryTheory.CategoryStruct.id Y

@[simp]

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

def CategoryTheory.SplitEpi.splitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitEpi f] : CategoryTheory.IsSplitMono (CategoryTheory.section_ f)

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

Equations

• ⋯ = ⋯

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

A split epi which is mono is an iso.

@[instance 100]

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

Every iso is a split mono.

Equations

• ⋯ = ⋯

@[instance 100]

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

Every iso is a split epi.

Equations

• ⋯ = ⋯

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

@[instance 100]

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

Every split mono is a mono.

Equations

• ⋯ = ⋯

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

@[instance 100]

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

Every split epi is an epi.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Every split mono whose retraction is mono is an iso.

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

Every split mono whose retraction is mono is an iso.

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

Every split epi whose section is epi is an iso.

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

Every split epi whose section is epi is an iso.

noncomputable def CategoryTheory.Groupoid.ofTruncSplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (CategoryTheory.IsSplitMono f)) : CategoryTheory.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₁) [CategoryTheory.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) [inst : CategoryTheory.Mono f], CategoryTheory.IsSplitMono f

  All monos are split

class CategoryTheory.SplitEpiCategory (C : Type u₁) [CategoryTheory.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) [inst : CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f

  All epis are split

theorem CategoryTheory.isSplitMono_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (sm : CategoryTheory.SplitMono f) (F : CategoryTheory.Functor C D) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (sm : CategoryTheory.SplitMono f) (F : CategoryTheory.Functor C D) : (sm.map F).retraction = F.map sm.retraction

def CategoryTheory.SplitEpi.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f) (F : CategoryTheory.Functor C D) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f) (F : CategoryTheory.Functor C D) : (se.map F).section_ = F.map se.section_

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯