Definitions and basic properties of regular monomorphisms and epimorphisms. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A regular monomorphism is a morphism that is the equalizer of some parallel pair.
We give the constructions
is_split_mono → regular_monoandregular_mono → monoas well as the dual constructions for regular epimorphisms. Additionally, we give the constructionregular_epi ⟶ strong_epi.
We also define classes regular_mono_category and regular_epi_category for categories in which
every monomorphism or epimorphism is regular, and deduce that these categories are
strong_mono_categorys resp. strong_epi_categorys.
@[class]
structure
category_theory.regular_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
Type (max u₁ v₁)
- Z : C
- left : Y ⟶ category_theory.regular_mono.Z f
- right : Y ⟶ category_theory.regular_mono.Z f
- w : f ≫ category_theory.regular_mono.left = f ≫ category_theory.regular_mono.right
- is_limit : category_theory.limits.is_limit (category_theory.limits.fork.of_ι f category_theory.regular_mono.w)
A regular monomorphism is a morphism which is the equalizer of some parallel pair.
Instances of this typeclass
Instances of other typeclasses for category_theory.regular_mono
- category_theory.regular_mono.has_sizeof_inst
theorem
category_theory.regular_mono.w_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
[self : category_theory.regular_mono f]
{X' : C}
(f' : category_theory.regular_mono.Z f ⟶ X') :
@[protected, instance]
def
category_theory.regular_mono.mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.regular_mono f] :
Every regular monomorphism is a monomorphism.
@[protected, instance]
noncomputable
def
category_theory.equalizer_regular
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(g h : X ⟶ Y)
[category_theory.limits.has_limit (category_theory.limits.parallel_pair g h)] :
Equations
- category_theory.equalizer_regular g h = {Z := Y, left := g, right := h, w := _, is_limit := category_theory.limits.fork.is_limit.mk (category_theory.limits.fork.of_ι (category_theory.limits.equalizer.ι g h) _) (λ (s : category_theory.limits.fork g h), category_theory.limits.limit.lift (category_theory.limits.parallel_pair g h) s) _ _}
@[protected, instance]
noncomputable
def
category_theory.regular_mono.of_is_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_split_mono f] :
Every split monomorphism is a regular monomorphism.
Equations
- category_theory.regular_mono.of_is_split_mono f = {Z := Y, left := 𝟙 Y, right := category_theory.retraction f ≫ f, w := _, is_limit := category_theory.limits.is_split_mono_equalizes f _inst_2}
def
category_theory.regular_mono.lift'
{C : Type u₁}
[category_theory.category C]
{X Y W : C}
(f : X ⟶ Y)
[category_theory.regular_mono f]
(k : W ⟶ Y)
(h : k ≫ category_theory.regular_mono.left = k ≫ category_theory.regular_mono.right) :
If f is a regular mono, then any map k : W ⟶ Y equalizing regular_mono.left and
regular_mono.right induces a morphism l : W ⟶ X such that l ≫ f = k.
def
category_theory.regular_of_is_pullback_snd_of_regular
{C : Type u₁}
[category_theory.category C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[hr : category_theory.regular_mono h]
(comm : f ≫ h = g ≫ k)
(t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm)) :
The second leg of a pullback cone is a regular monomorphism if the right component is too.
See also pullback.snd_of_mono for the basic monomorphism version, and
regular_of_is_pullback_fst_of_regular for the flipped version.
Equations
- category_theory.regular_of_is_pullback_snd_of_regular comm t = {Z := category_theory.regular_mono.Z h hr, left := k ≫ category_theory.regular_mono.left, right := k ≫ category_theory.regular_mono.right, w := _, is_limit := category_theory.limits.fork.is_limit.mk' (category_theory.limits.fork.of_ι g _) (λ (s : category_theory.limits.fork (k ≫ category_theory.regular_mono.left) (k ≫ category_theory.regular_mono.right)), (category_theory.limits.fork.is_limit.lift' category_theory.regular_mono.is_limit (s.ι ≫ k) _).cases_on (λ (l : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero ⟶ (category_theory.limits.fork.of_ι h category_theory.regular_mono.w).X) (hl : l ≫ (category_theory.limits.fork.of_ι h category_theory.regular_mono.w).ι = s.ι ≫ k), (category_theory.limits.pullback_cone.is_limit.lift' t l s.ι hl).cases_on (λ (p : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero ⟶ (category_theory.limits.pullback_cone.mk f g comm).X) (property : p ≫ (category_theory.limits.pullback_cone.mk f g comm).fst = l ∧ p ≫ (category_theory.limits.pullback_cone.mk f g comm).snd = s.ι), property.dcases_on (λ (hp₁ : p ≫ (category_theory.limits.pullback_cone.mk f g comm).fst = l) (hp₂ : p ≫ (category_theory.limits.pullback_cone.mk f g comm).snd = s.ι), ⟨p, _⟩))))}
def
category_theory.regular_of_is_pullback_fst_of_regular
{C : Type u₁}
[category_theory.category C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[hr : category_theory.regular_mono k]
(comm : f ≫ h = g ≫ k)
(t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm)) :
The first leg of a pullback cone is a regular monomorphism if the left component is too.
See also pullback.fst_of_mono for the basic monomorphism version, and
regular_of_is_pullback_snd_of_regular for the flipped version.
@[protected, instance]
def
category_theory.strong_mono_of_regular_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.regular_mono f] :
theorem
category_theory.is_iso_of_regular_mono_of_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.regular_mono f]
[e : category_theory.epi f] :
A regular monomorphism is an isomorphism if it is an epimorphism.
@[class]
structure
category_theory.regular_mono_category
(C : Type u₁)
[category_theory.category C] :
Type (max u₁ v₁)
- regular_mono_of_mono : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f], category_theory.regular_mono f
A regular mono category is a category in which every monomorphism is regular.
Instances of this typeclass
Instances of other typeclasses for category_theory.regular_mono_category
- category_theory.regular_mono_category.has_sizeof_inst
def
category_theory.regular_mono_of_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.regular_mono_category C]
(f : X ⟶ Y)
[category_theory.mono f] :
In a category in which every monomorphism is regular, we can express every monomorphism as an equalizer. This is not an instance because it would create an instance loop.
@[protected, instance]
noncomputable
def
category_theory.regular_mono_category_of_split_mono_category
{C : Type u₁}
[category_theory.category C]
[category_theory.split_mono_category C] :
Equations
- category_theory.regular_mono_category_of_split_mono_category = {regular_mono_of_mono := λ (_x _x_1 : C) (f : _x ⟶ _x_1) (_x_2 : category_theory.mono f), category_theory.regular_mono.of_is_split_mono f}
@[protected, instance]
@[class]
structure
category_theory.regular_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
Type (max u₁ v₁)
- W : C
- left : category_theory.regular_epi.W f ⟶ X
- right : category_theory.regular_epi.W f ⟶ X
- w : category_theory.regular_epi.left ≫ f = category_theory.regular_epi.right ≫ f
- is_colimit : category_theory.limits.is_colimit (category_theory.limits.cofork.of_π f category_theory.regular_epi.w)
A regular epimorphism is a morphism which is the coequalizer of some parallel pair.
Instances of this typeclass
Instances of other typeclasses for category_theory.regular_epi
- category_theory.regular_epi.has_sizeof_inst
theorem
category_theory.regular_epi.w_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
[self : category_theory.regular_epi f]
{X' : C}
(f' : Y ⟶ X') :
@[protected, instance]
def
category_theory.regular_epi.epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.regular_epi f] :
Every regular epimorphism is an epimorphism.
@[protected, instance]
noncomputable
def
category_theory.coequalizer_regular
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(g h : X ⟶ Y)
[category_theory.limits.has_colimit (category_theory.limits.parallel_pair g h)] :
Equations
- category_theory.coequalizer_regular g h = {W := X, left := g, right := h, w := _, is_colimit := category_theory.limits.cofork.is_colimit.mk (category_theory.limits.cofork.of_π (category_theory.limits.coequalizer.π g h) _) (λ (s : category_theory.limits.cofork g h), category_theory.limits.colimit.desc (category_theory.limits.parallel_pair g h) s) _ _}
@[protected, instance]
noncomputable
def
category_theory.regular_epi.of_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_split_epi f] :
Every split epimorphism is a regular epimorphism.
Equations
- category_theory.regular_epi.of_split_epi f = {W := X, left := 𝟙 X, right := f ≫ category_theory.section_ f, w := _, is_colimit := category_theory.limits.is_split_epi_coequalizes f _inst_2}
def
category_theory.regular_epi.desc'
{C : Type u₁}
[category_theory.category C]
{X Y W : C}
(f : X ⟶ Y)
[category_theory.regular_epi f]
(k : X ⟶ W)
(h : category_theory.regular_epi.left ≫ k = category_theory.regular_epi.right ≫ k) :
If f is a regular epi, then every morphism k : X ⟶ W coequalizing regular_epi.left and
regular_epi.right induces l : Y ⟶ W such that f ≫ l = k.
def
category_theory.regular_of_is_pushout_snd_of_regular
{C : Type u₁}
[category_theory.category C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[gr : category_theory.regular_epi g]
(comm : f ≫ h = g ≫ k)
(t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h k comm)) :
The second leg of a pushout cocone is a regular epimorphism if the right component is too.
See also pushout.snd_of_epi for the basic epimorphism version, and
regular_of_is_pushout_fst_of_regular for the flipped version.
Equations
- category_theory.regular_of_is_pushout_snd_of_regular comm t = {W := category_theory.regular_epi.W g gr, left := category_theory.regular_epi.left ≫ f, right := category_theory.regular_epi.right ≫ f, w := _, is_colimit := category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cofork.of_π h _) (λ (s : category_theory.limits.cofork (category_theory.regular_epi.left ≫ f) (category_theory.regular_epi.right ≫ f)), (category_theory.limits.cofork.is_colimit.desc' category_theory.regular_epi.is_colimit (f ≫ s.π) _).cases_on (λ (l : (category_theory.limits.cofork.of_π g category_theory.regular_epi.w).X ⟶ ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.one) (hl : (category_theory.limits.cofork.of_π g category_theory.regular_epi.w).π ≫ l = f ≫ s.π), (category_theory.limits.pushout_cocone.is_colimit.desc' t s.π l _).cases_on (λ (p : (category_theory.limits.pushout_cocone.mk h k comm).X ⟶ ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.one) (property : (category_theory.limits.pushout_cocone.mk h k comm).inl ≫ p = s.π ∧ (category_theory.limits.pushout_cocone.mk h k comm).inr ≫ p = l), property.dcases_on (λ (hp₁ : (category_theory.limits.pushout_cocone.mk h k comm).inl ≫ p = s.π) (hp₂ : (category_theory.limits.pushout_cocone.mk h k comm).inr ≫ p = l), ⟨p, _⟩))))}
def
category_theory.regular_of_is_pushout_fst_of_regular
{C : Type u₁}
[category_theory.category C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[fr : category_theory.regular_epi f]
(comm : f ≫ h = g ≫ k)
(t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h k comm)) :
The first leg of a pushout cocone is a regular epimorphism if the left component is too.
See also pushout.fst_of_epi for the basic epimorphism version, and
regular_of_is_pushout_snd_of_regular for the flipped version.
@[protected, instance]
def
category_theory.strong_epi_of_regular_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.regular_epi f] :
theorem
category_theory.is_iso_of_regular_epi_of_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.regular_epi f]
[m : category_theory.mono f] :
A regular epimorphism is an isomorphism if it is a monomorphism.
@[class]
structure
category_theory.regular_epi_category
(C : Type u₁)
[category_theory.category C] :
Type (max u₁ v₁)
- regular_epi_of_epi : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.epi f], category_theory.regular_epi f
A regular epi category is a category in which every epimorphism is regular.
Instances of this typeclass
Instances of other typeclasses for category_theory.regular_epi_category
- category_theory.regular_epi_category.has_sizeof_inst
def
category_theory.regular_epi_of_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.regular_epi_category C]
(f : X ⟶ Y)
[category_theory.epi f] :
In a category in which every epimorphism is regular, we can express every epimorphism as a coequalizer. This is not an instance because it would create an instance loop.
@[protected, instance]
noncomputable
def
category_theory.regular_epi_category_of_split_epi_category
{C : Type u₁}
[category_theory.category C]
[category_theory.split_epi_category C] :
Equations
- category_theory.regular_epi_category_of_split_epi_category = {regular_epi_of_epi := λ (_x _x_1 : C) (f : _x ⟶ _x_1) (_x_2 : category_theory.epi f), category_theory.regular_epi.of_split_epi f}
@[protected, instance]