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
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
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
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
structure
CategoryTheory.SplitMono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Type v₁
- retraction : Y ⟶ X
The map splitting
f - id : CategoryTheory.CategoryStruct.comp f s.retraction = CategoryTheory.CategoryStruct.id X
fcomposed withretractionis the identity
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.
Instances For
@[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)
:
- exists_splitMono : Nonempty (CategoryTheory.SplitMono f)
There is a splitting
IsSplitMono f is the assertion that f admits a retraction
Instances
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₁
- section_ : Y ⟶ X
The map splitting
f - id : CategoryTheory.CategoryStruct.comp s.section_ f = CategoryTheory.CategoryStruct.id Y
section_composed withfis the identity
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.
Instances For
@[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)
:
- exists_splitEpi : Nonempty (CategoryTheory.SplitEpi f)
There is a splitting
IsSplitEpi f is the assertion that f admits a section
Instances
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 = (Nonempty.some (_ : Nonempty (CategoryTheory.SplitMono f))).retraction
Instances For
@[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)
:
@[simp]
theorem
CategoryTheory.IsSplitMono.id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[hf : CategoryTheory.IsSplitMono f]
:
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
Instances For
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.
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 = (Nonempty.some (_ : Nonempty (CategoryTheory.SplitEpi f))).section_
Instances For
@[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)
:
@[simp]
theorem
CategoryTheory.IsSplitEpi.id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[hf : CategoryTheory.IsSplitEpi f]
:
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
Instances For
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.
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
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.
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.
theorem
CategoryTheory.SplitMono.mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(sm : CategoryTheory.SplitMono f)
:
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.
theorem
CategoryTheory.SplitEpi.epi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(se : CategoryTheory.SplitEpi f)
:
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.
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 (_ : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f)
Instances For
- isSplitMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.IsSplitMono f
All monos are split
A split mono category is a category in which every monomorphism is split.
Instances
- isSplitEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f
All epis are split
A split epi category is a category in which every epimorphism is split.
Instances
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.
@[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)
:
(CategoryTheory.SplitMono.map sm F).retraction = F.map sm.retraction
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
- CategoryTheory.SplitMono.map sm F = CategoryTheory.SplitMono.mk (F.map sm.retraction)
Instances For
@[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)
:
(CategoryTheory.SplitEpi.map se F).section_ = F.map se.section_
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
- CategoryTheory.SplitEpi.map se F = CategoryTheory.SplitEpi.mk (F.map se.section_)
Instances For
instance
CategoryTheory.instIsSplitMonoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap
{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
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.instIsSplitEpiObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap
{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
- One or more equations did not get rendered due to their size.