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 : Cᵒᵖ}
{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 : Cᵒᵖ}
{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 : C}
{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 : C}
{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 : 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
fcomposed withretractionis 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},
x.retraction = y.retraction → x = y
@[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
@[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
class
CategoryTheory.IsSplitMono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
IsSplitMono f is the assertion that f admits a retraction
- exists_splitMono : Nonempty (CategoryTheory.SplitMono f)
There is a splitting
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
def
CategoryTheory.SplitMono.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(smf : CategoryTheory.SplitMono f)
(smg : CategoryTheory.SplitMono 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 : C}
{Y : C}
{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 : C}
{Y : C}
{f : X ⟶ Y}
(sm : CategoryTheory.SplitMono 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 : 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 withfis 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},
x.section_ = y.section_ → x = y
@[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
@[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
class
CategoryTheory.IsSplitEpi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
IsSplitEpi f is the assertion that f admits a section
- exists_splitEpi : Nonempty (CategoryTheory.SplitEpi f)
There is a splitting
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
def
CategoryTheory.SplitEpi.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(sef : CategoryTheory.SplitEpi f)
(seg : CategoryTheory.SplitEpi 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 : C}
{Y : C}
{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 : C}
{Y : C}
{f : X ⟶ Y}
(se : CategoryTheory.SplitEpi 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 : 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
Instances For
@[simp]
theorem
CategoryTheory.IsSplitMono.id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[hf : CategoryTheory.IsSplitMono f]
:
@[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)
:
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 := ⋯ }
instance
CategoryTheory.retraction_isSplitEpi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono 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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono f]
[CategoryTheory.Epi f]
:
A split mono which is epi is an iso.
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_
Instances For
@[simp]
theorem
CategoryTheory.IsSplitEpi.id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[hf : CategoryTheory.IsSplitEpi f]
:
@[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)
:
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 := ⋯ }
instance
CategoryTheory.section_isSplitMono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitEpi 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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
[CategoryTheory.IsSplitEpi 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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
Every iso is a split mono.
Equations
- ⋯ = ⋯
@[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]
:
Every iso is a split epi.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.SplitMono.mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(sm : CategoryTheory.SplitMono f)
:
@[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]
:
Every split mono is a mono.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.SplitEpi.epi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(se : CategoryTheory.SplitEpi f)
:
@[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]
:
Every split epi is an epi.
Equations
- ⋯ = ⋯
instance
CategoryTheory.instIsSplitMonoComp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[hf : CategoryTheory.IsSplitMono f]
[hg : CategoryTheory.IsSplitMono g]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.instIsSplitEpiComp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[hf : CategoryTheory.IsSplitEpi f]
[hg : CategoryTheory.IsSplitEpi g]
:
Equations
- ⋯ = ⋯
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]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[hf : CategoryTheory.IsSplitMono f]
[hf' : CategoryTheory.Mono (CategoryTheory.retraction 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 : C}
{Y : C}
{f : X ⟶ Y}
(hf : CategoryTheory.SplitEpi f)
[CategoryTheory.Epi hf.section_]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[hf : CategoryTheory.IsSplitEpi f]
[hf' : CategoryTheory.Epi (CategoryTheory.section_ 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))
:
A category where every morphism has a Trunc retraction is computably a groupoid.
Equations
- CategoryTheory.Groupoid.ofTruncSplitMono all_split_mono = CategoryTheory.Groupoid.ofIsIso ⋯
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
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
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.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
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]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi 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 : 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 := ⋯ }
@[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
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 := ⋯ }
@[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_
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
- ⋯ = ⋯
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
- ⋯ = ⋯