Facts about epimorphisms and monomorphisms. #
The definitions of epi and mono are in category_theory.category,
since they are used by some lemmas for iso, which is used everywhere.
@[protected, instance]
def
category_theory.unop_mono_of_epi
{C : Type u₁}
[category_theory.category C]
{A B : Cᵒᵖ}
(f : A ⟶ B)
[category_theory.epi f] :
@[protected, instance]
def
category_theory.unop_epi_of_mono
{C : Type u₁}
[category_theory.category C]
{A B : Cᵒᵖ}
(f : A ⟶ B)
[category_theory.mono f] :
@[protected, instance]
def
category_theory.op_mono_of_epi
{C : Type u₁}
[category_theory.category C]
{A B : C}
(f : A ⟶ B)
[category_theory.epi f] :
@[protected, instance]
def
category_theory.op_epi_of_mono
{C : Type u₁}
[category_theory.category C]
{A B : C}
(f : A ⟶ B)
[category_theory.mono f] :
theorem
category_theory.left_adjoint_preserves_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X Y : C}
{f : X ⟶ Y}
(hf : category_theory.epi f) :
category_theory.epi (F.map f)
theorem
category_theory.right_adjoint_preserves_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X Y : D}
{f : X ⟶ Y}
(hf : category_theory.mono f) :
category_theory.mono (G.map f)
@[protected, instance]
def
category_theory.is_equivalence.epi_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[category_theory.is_left_adjoint F]
{X Y : C}
{f : X ⟶ Y}
[h : category_theory.epi f] :
category_theory.epi (F.map f)
@[protected, instance]
def
category_theory.is_equivalence.mono_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[category_theory.is_right_adjoint F]
{X Y : C}
{f : X ⟶ Y}
[h : category_theory.mono f] :
category_theory.mono (F.map f)
theorem
category_theory.faithful_reflects_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.faithful F]
{X Y : C}
{f : X ⟶ Y}
(hf : category_theory.epi (F.map f)) :
theorem
category_theory.faithful_reflects_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.faithful F]
{X Y : C}
{f : X ⟶ Y}
(hf : category_theory.mono (F.map f)) :
@[class]
structure
category_theory.split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
Type v₁
A split monomorphism is a morphism f : X ⟶ Y admitting a retraction retraction f : Y ⟶ X
such that f ≫ retraction f = 𝟙 X.
Every split monomorphism is a monomorphism.
@[class]
structure
category_theory.split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
Type v₁
A split epimorphism is a morphism f : X ⟶ Y admitting a 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.
def
category_theory.retraction
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f] :
Y ⟶ X
The chosen retraction of a split monomorphism.
Equations
@[simp]
theorem
category_theory.split_mono.id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f] :
f ≫ category_theory.retraction f = 𝟙 X
@[simp]
theorem
category_theory.split_mono.id_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f]
{X' : C}
(f' : X ⟶ X') :
f ≫ category_theory.retraction f ≫ f' = f'
@[protected, instance]
def
category_theory.retraction_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f] :
The retraction of a split monomorphism is itself a split epimorphism.
Equations
- category_theory.retraction_split_epi f = {section_ := f, id' := _}
theorem
category_theory.is_iso_of_epi_of_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f]
[category_theory.epi f] :
A split mono which is epi is an iso.
def
category_theory.section_
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_epi f] :
Y ⟶ X
The chosen section of a split epimorphism.
(Note that section is a reserved keyword, so we append an underscore.)
Equations
@[simp]
theorem
category_theory.split_epi.id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_epi f] :
category_theory.section_ f ≫ f = 𝟙 Y
@[simp]
theorem
category_theory.split_epi.id_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_epi f]
{X' : C}
(f' : Y ⟶ X') :
category_theory.section_ f ≫ f ≫ f' = f'
@[protected, instance]
def
category_theory.section_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_epi f] :
The section of a split epimorphism is itself a split monomorphism.
Equations
- category_theory.section_split_mono f = {retraction := f, id' := _}
theorem
category_theory.is_iso_of_mono_of_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
[category_theory.split_epi f] :
A split epi which is mono is an iso.
@[protected, instance]
noncomputable
def
category_theory.split_mono.of_iso
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
Every iso is a split mono.
Equations
- category_theory.split_mono.of_iso f = {retraction := category_theory.inv f _inst_2, id' := _}
@[protected, instance]
noncomputable
def
category_theory.split_epi.of_iso
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
Every iso is a split epi.
Equations
- category_theory.split_epi.of_iso f = {section_ := category_theory.inv f _inst_2, id' := _}
@[protected, instance]
def
category_theory.split_mono.mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f] :
Every split mono is a mono.
@[protected, instance]
def
category_theory.split_epi.epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_epi f] :
Every split epi is an epi.
theorem
category_theory.is_iso.of_mono_retraction
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.split_mono f]
[category_theory.mono (category_theory.retraction f)] :
Every split mono whose retraction is mono is an iso.
theorem
category_theory.is_iso.of_epi_section
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.split_epi f]
[category_theory.epi (category_theory.section_ f)] :
Every split epi whose section is epi is an iso.
noncomputable
def
category_theory.groupoid.of_trunc_split_mono
{C : Type u₁}
[category_theory.category C]
(all_split_mono : Π {X Y : C} (f : X ⟶ Y), trunc (category_theory.split_mono f)) :
A category where every morphism has a trunc retraction is computably a groupoid.
Equations
@[class]
structure
category_theory.split_mono_category
(C : Type u₁)
[category_theory.category C] :
Type (max u₁ v₁)
- split_mono_of_mono : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f], category_theory.split_mono f
A split mono category is a category in which every monomorphism is split.
@[class]
structure
category_theory.split_epi_category
(C : Type u₁)
[category_theory.category C] :
Type (max u₁ v₁)
- split_epi_of_epi : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.epi f], category_theory.split_epi f
A split epi category is a category in which every epimorphism is split.
Instances
def
category_theory.split_mono_of_mono
{C : Type u₁}
[category_theory.category C]
[category_theory.split_mono_category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.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.
def
category_theory.split_epi_of_epi
{C : Type u₁}
[category_theory.category C]
[category_theory.split_epi_category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.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.
@[protected, instance]
def
category_theory.functor.map.split_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f]
(F : C ⥤ D) :
Split monomorphisms are also absolute monomorphisms.
Equations
- category_theory.functor.map.split_mono f F = {retraction := F.map (category_theory.retraction f), id' := _}
@[protected, instance]
def
category_theory.functor.map.split_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_epi f]
(F : C ⥤ D) :
category_theory.split_epi (F.map f)
Split epimorphisms are also absolute epimorphisms.
Equations
- category_theory.functor.map.split_epi f F = {section_ := F.map (category_theory.section_ f), id' := _}