Facts about epimorphisms and monomorphisms. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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] :
@[nolint, ext]
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 with a given retraction retraction f : Y ⟶ X
such that f ≫ retraction f = 𝟙 X.
Every split monomorphism is a monomorphism.
Instances for category_theory.split_mono
- category_theory.split_mono.has_sizeof_inst
theorem
category_theory.split_mono.ext
{C : Type u₁}
{_inst_1 : category_theory.category C}
{X Y : C}
{f : X ⟶ Y}
(x y : category_theory.split_mono f)
(h : x.retraction = y.retraction) :
x = y
theorem
category_theory.split_mono.ext_iff
{C : Type u₁}
{_inst_1 : category_theory.category C}
{X Y : C}
{f : X ⟶ Y}
(x y : category_theory.split_mono f) :
x = y ↔ x.retraction = y.retraction
@[simp]
theorem
category_theory.split_mono.id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(self : category_theory.split_mono f) :
f ≫ self.retraction = 𝟙 X
@[simp]
theorem
category_theory.split_mono.id_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(self : category_theory.split_mono f)
{X' : C}
(f' : X ⟶ X') :
f ≫ self.retraction ≫ f' = f'
@[class]
structure
category_theory.is_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
Prop
- exists_split_mono : nonempty (category_theory.split_mono f)
is_split_mono f is the assertion that f admits a retraction
Instances of this typeclass
- category_theory.is_split_mono.of_iso
- category_theory.section_is_split_mono
- category_theory.functor.map.is_split_mono
- category_theory.limits.terminal.is_split_mono_from
- category_theory.limits.diag.category_theory.is_split_mono
- category_theory.limits.is_split_mono_sigma_ι
- category_theory.limits.is_split_mono_coprod_inl
- category_theory.limits.is_split_mono_coprod_inr
- category_theory.limits.biproduct.ι_mono
- category_theory.limits.binary_bicone.inl.category_theory.is_split_mono
- category_theory.limits.binary_bicone.inr.category_theory.is_split_mono
- category_theory.limits.biprod.inl_mono
- category_theory.limits.biprod.inr_mono
- category_theory.functor.biproduct_comparison'.category_theory.is_split_mono
- category_theory.functor.biprod_comparison'.category_theory.is_split_mono
- category_theory.limits.pullback.diagonal.category_theory.is_split_mono
theorem
category_theory.is_split_mono.mk'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(sm : category_theory.split_mono f) :
A constructor for is_split_mono f taking a split_mono f as an argument
theorem
category_theory.split_epi.ext_iff
{C : Type u₁}
{_inst_1 : category_theory.category C}
{X Y : C}
{f : X ⟶ Y}
(x y : category_theory.split_epi f) :
theorem
category_theory.split_epi.ext
{C : Type u₁}
{_inst_1 : category_theory.category C}
{X Y : C}
{f : X ⟶ Y}
(x y : category_theory.split_epi f)
(h : x.section_ = y.section_) :
x = y
@[nolint, ext]
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 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 category_theory.split_epi
- category_theory.split_epi.has_sizeof_inst
@[simp]
theorem
category_theory.split_epi.id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(self : category_theory.split_epi f) :
@[simp]
theorem
category_theory.split_epi.id_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(self : category_theory.split_epi f)
{X' : C}
(f' : Y ⟶ X') :
@[class]
structure
category_theory.is_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
Prop
- exists_split_epi : nonempty (category_theory.split_epi f)
is_split_epi f is the assertion that f admits a section
Instances of this typeclass
- category_theory.is_split_epi.of_iso
- category_theory.retraction_is_split_epi
- category_theory.functor.map.is_split_epi
- category_theory.limits.initial.is_split_epi_to
- category_theory.limits.is_split_epi_pi_π
- category_theory.limits.is_split_epi_prod_fst
- category_theory.limits.is_split_epi_prod_snd
- category_theory.limits.biproduct.π_epi
- category_theory.limits.binary_bicone.fst.category_theory.is_split_epi
- category_theory.limits.binary_bicone.snd.category_theory.is_split_epi
- category_theory.limits.biprod.fst_epi
- category_theory.limits.biprod.snd_epi
- category_theory.functor.biproduct_comparison.category_theory.is_split_epi
- category_theory.functor.biprod_comparison.category_theory.is_split_epi
- category_theory.limits.pullback.fst.category_theory.is_split_epi
- category_theory.limits.pullback.snd.category_theory.is_split_epi
theorem
category_theory.is_split_epi.mk'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(se : category_theory.split_epi f) :
A constructor for is_split_epi f taking a split_epi f as an argument
noncomputable
def
category_theory.retraction
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f] :
Y ⟶ X
The chosen retraction of a split monomorphism.
Equations
Instances for category_theory.retraction
@[simp]
theorem
category_theory.is_split_mono.id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f] :
f ≫ category_theory.retraction f = 𝟙 X
@[simp]
theorem
category_theory.is_split_mono.id_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f]
{X' : C}
(f' : X ⟶ X') :
f ≫ category_theory.retraction f ≫ f' = f'
def
category_theory.split_mono.split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(sm : category_theory.split_mono f) :
The retraction of a split monomorphism has an obvious section.
@[protected, instance]
def
category_theory.retraction_is_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f] :
The retraction of a split monomorphism is itself a split epimorphism.
theorem
category_theory.is_iso_of_epi_of_is_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_split_mono f]
[category_theory.epi f] :
A split mono which is epi is an iso.
noncomputable
def
category_theory.section_
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_epi f] :
Y ⟶ X
The chosen section of a split epimorphism.
(Note that section is a reserved keyword, so we append an underscore.)
Instances for category_theory.section_
@[simp]
theorem
category_theory.is_split_epi.id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_epi f] :
category_theory.section_ f ≫ f = 𝟙 Y
@[simp]
theorem
category_theory.is_split_epi.id_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_epi f]
{X' : C}
(f' : Y ⟶ X') :
category_theory.section_ f ≫ f ≫ f' = f'
def
category_theory.split_epi.split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(se : category_theory.split_epi f) :
The section of a split epimorphism has an obvious retraction.
Equations
- se.split_mono = {retraction := f, id' := _}
@[protected, instance]
def
category_theory.section_is_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_epi f] :
The section of a split epimorphism is itself a split monomorphism.
theorem
category_theory.is_iso_of_mono_of_is_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
[category_theory.is_split_epi f] :
A split epi which is mono is an iso.
@[protected, instance]
def
category_theory.is_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.
@[protected, instance]
def
category_theory.is_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.
theorem
category_theory.split_mono.mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(sm : category_theory.split_mono f) :
@[protected, instance]
def
category_theory.is_split_mono.mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f] :
Every split mono is a mono.
theorem
category_theory.split_epi.epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
(se : category_theory.split_epi f) :
@[protected, instance]
def
category_theory.is_split_epi.epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_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}
(hf : category_theory.split_mono f)
[category_theory.mono hf.retraction] :
Every split mono whose retraction is mono is an iso.
theorem
category_theory.is_iso.of_mono_retraction
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f]
[hf' : 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}
(hf : category_theory.split_epi f)
[category_theory.epi hf.section_] :
Every split epi whose section is epi is an iso.
theorem
category_theory.is_iso.of_epi_section
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_epi f]
[hf' : 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.is_split_mono f)) :
A category where every morphism has a trunc retraction is computably a groupoid.
Equations
@[class]
- is_split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f], category_theory.is_split_mono f
A split mono category is a category in which every monomorphism is split.
Instances for category_theory.split_mono_category
- category_theory.split_mono_category.has_sizeof_inst
@[class]
- is_split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.epi f], category_theory.is_split_epi f
A split epi category is a category in which every epimorphism is split.
Instances of this typeclass
Instances of other typeclasses for category_theory.split_epi_category
- category_theory.split_epi_category.has_sizeof_inst
theorem
category_theory.is_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.
theorem
category_theory.is_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.
def
category_theory.split_mono.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
{f : X ⟶ Y}
(sm : category_theory.split_mono f)
(F : C ⥤ D) :
Split monomorphisms are also absolute monomorphisms.
Equations
- sm.map F = {retraction := F.map sm.retraction, id' := _}
@[simp]
theorem
category_theory.split_mono.map_retraction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
{f : X ⟶ Y}
(sm : category_theory.split_mono f)
(F : C ⥤ D) :
(sm.map F).retraction = F.map sm.retraction
@[simp]
theorem
category_theory.split_epi.map_section_
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
{f : X ⟶ Y}
(se : category_theory.split_epi f)
(F : C ⥤ D) :
def
category_theory.split_epi.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
{f : X ⟶ Y}
(se : category_theory.split_epi f)
(F : C ⥤ D) :
category_theory.split_epi (F.map f)
Split epimorphisms are also absolute epimorphisms.
@[protected, instance]
def
category_theory.functor.map.is_split_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_mono f]
(F : C ⥤ D) :
@[protected, instance]
def
category_theory.functor.map.is_split_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_split_epi f]
(F : C ⥤ D) :