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.

source

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

CategoryTheory.Mono f.unop

Equations

⋯ = ⋯

source

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

CategoryTheory.Epi f.unop

Equations

⋯ = ⋯

source

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

CategoryTheory.Mono f.op

Equations

⋯ = ⋯

source

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

CategoryTheory.Epi f.op

Equations

⋯ = ⋯

source

theorem CategoryTheory.SplitMono.ext {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitMono f}, x.retraction = y.retraction → x = y

source

theorem CategoryTheory.SplitMono.ext_iff {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitMono f}, x = y ↔ x.retraction = y.retraction

source

structure CategoryTheory.SplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp f self.retraction = CategoryTheory.CategoryStruct.id X

f composed with retraction is the identity

source

@[simp]

theorem CategoryTheory.SplitMono.id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

source

class CategoryTheory.IsSplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

Instances

source

theorem CategoryTheory.IsSplitMono.exists_splitMono {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsSplitMono f], Nonempty (CategoryTheory.SplitMono f)

There is a splitting

source

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

CategoryTheory.IsSplitMono f

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

source

theorem CategoryTheory.SplitEpi.ext {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitEpi f}, x.section_ = y.section_ → x = y

source

theorem CategoryTheory.SplitEpi.ext_iff {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitEpi f}, x = y ↔ x.section_ = y.section_

source

structure CategoryTheory.SplitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp self.section_ f = CategoryTheory.CategoryStruct.id Y

section_ composed with f is the identity

source

@[simp]

theorem CategoryTheory.SplitEpi.id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

source

class CategoryTheory.IsSplitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

Instances

source

theorem CategoryTheory.IsSplitEpi.exists_splitEpi {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsSplitEpi f], Nonempty (CategoryTheory.SplitEpi f)

There is a splitting

source

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

CategoryTheory.IsSplitEpi f

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

source

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

Y ⟶ X

The chosen retraction of a split monomorphism.

Equations

CategoryTheory.retraction f = ⋯.some.retraction

source

@[simp]

theorem CategoryTheory.IsSplitMono.id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp f (CategoryTheory.retraction f) = CategoryTheory.CategoryStruct.id X

source

def CategoryTheory.SplitMono.splitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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 := ⋯ }

source

instance CategoryTheory.retraction_isSplitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

⋯ = ⋯

source

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

CategoryTheory.IsIso f

A split mono which is epi is an iso.

source

noncomputable def CategoryTheory.section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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_

source

@[simp]

theorem CategoryTheory.IsSplitEpi.id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) f = CategoryTheory.CategoryStruct.id Y

source

def CategoryTheory.SplitEpi.splitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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 := ⋯ }

source

instance CategoryTheory.section_isSplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

⋯ = ⋯

source

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

CategoryTheory.IsIso f

A split epi which is mono is an iso.

source

@[instance 100]

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

CategoryTheory.IsSplitMono f

Every iso is a split mono.

Equations

⋯ = ⋯

source

@[instance 100]

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

CategoryTheory.IsSplitEpi f

Every iso is a split epi.

Equations

⋯ = ⋯

source

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

CategoryTheory.Mono f

source

@[instance 100]

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

CategoryTheory.Mono f

Every split mono is a mono.

Equations

⋯ = ⋯

source

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

CategoryTheory.Epi f

source

@[instance 100]

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

CategoryTheory.Epi f

Every split epi is an epi.

Equations

⋯ = ⋯

source

theorem CategoryTheory.IsIso.of_mono_retraction' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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.

source

theorem CategoryTheory.IsIso.of_mono_retraction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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.

source

theorem CategoryTheory.IsIso.of_epi_section' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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.

source

theorem CategoryTheory.IsIso.of_epi_section {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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.

source

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 ⋯

source

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

Instances

source

theorem CategoryTheory.SplitMonoCategory.isSplitMono_of_mono {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f], CategoryTheory.IsSplitMono f

All monos are split

source

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

Instances

source

theorem CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f

All epis are split

source

theorem CategoryTheory.isSplitMono_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitMonoCategory C] {X : C} {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.

source

theorem CategoryTheory.isSplitEpi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitEpiCategory C] {X : C} {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.

source

@[simp]

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

(sm.map F).retraction = F.map sm.retraction

source

def CategoryTheory.SplitMono.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {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 := ⋯ }

source

@[simp]

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

(se.map F).section_ = F.map se.section_

source

def CategoryTheory.SplitEpi.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {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 := ⋯ }

source

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

CategoryTheory.IsSplitMono (F.map f)

Equations

⋯ = ⋯

source

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

CategoryTheory.IsSplitEpi (F.map f)

Equations

⋯ = ⋯

Documentation

Mathlib.CategoryTheory.EpiMono

Facts about epimorphisms and monomorphisms. #