mathlib3 documentation

category_theory.epi_mono

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]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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) :
@[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'

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) :
self.section_ f = 𝟙 Y
@[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') :
self.section_ f f' = 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_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') :

The retraction of a split monomorphism has an obvious section.

Equations
@[protected, instance]

The retraction of a split monomorphism is itself a split epimorphism.

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.)

Equations
Instances for category_theory.section_
@[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') :

The section of a split epimorphism has an obvious retraction.

Equations
@[protected, instance]

The section of a split epimorphism is itself a split monomorphism.

A split epi which is mono is an iso.

@[protected, instance]

Every iso is a split mono.

@[protected, instance]

Every iso is a split epi.

@[protected, instance]

Every split mono is a mono.

@[protected, instance]

Every split epi is an epi.

Every split mono whose retraction is mono is an iso.

Every split mono whose retraction is mono is an iso.

Every split epi whose section is epi is an iso.

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]

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]

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

In a category in which every monomorphism is split, every monomorphism splits. This is not an instance because it would create an instance loop.

In a category in which every epimorphism is split, every epimorphism splits. This is not an instance because it would create an instance loop.

Split monomorphisms are also absolute monomorphisms.

Equations
@[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) :
@[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) :
(se.map F).section_ = F.map se.section_

Split epimorphisms are also absolute epimorphisms.

Equations
@[protected, instance]
@[protected, instance]