Definitions and basic properties of regular and normal monomorphisms and epimorphisms.
A regular monomorphism is a morphism that is the equalizer of some parallel pair. A normal monomorphism is a morphism that is the kernel of some other morphism.
We give the constructions
split_mono → regular_mononormal_mono → regular_mono, andregular_mono → monoas well as the dual constructions for regular and normal epimorphisms. Additionally, we give the constructionregular_epi ⟶ strong_epi.
@[class]
structure
category_theory.regular_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C} :
(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.
@[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.
Equations
- _ = _
@[instance]
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) _ _}
@[instance]
def
category_theory.regular_mono.of_split_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.split_mono f] :
Every split monomorphism is a regular monomorphism.
Equations
- category_theory.regular_mono.of_split_mono f = {Z := Y, left := 𝟙 Y, right := category_theory.retraction f ≫ f, w := _, is_limit := category_theory.limits.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) :
k ≫ category_theory.regular_mono.left = k ≫ category_theory.regular_mono.right → {l // l ≫ f = k}
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) :
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) :
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.
def
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.normal_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C] :
(X ⟶ Y) → Type (max u₁ v₁)
- Z : C
- g : Y ⟶ category_theory.normal_mono.Z f
- w : f ≫ category_theory.normal_mono.g = 0
- is_limit : category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι f category_theory.normal_mono.w)
A normal monomorphism is a morphism which is the kernel of some morphism.
def
category_theory.equivalence_reflects_normal_mono
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[category_theory.is_equivalence F]
{X Y : C}
{f : X ⟶ Y} :
If F is an equivalence and F.map f is a normal mono, then f is a normal mono.
Equations
- category_theory.equivalence_reflects_normal_mono F hf = {Z := F.obj_preimage (category_theory.normal_mono.Z (F.map f)), g := category_theory.full.preimage (category_theory.normal_mono.g ≫ (F.fun_obj_preimage_iso (category_theory.normal_mono.Z (F.map f))).inv), w := _, is_limit := category_theory.limits.reflects_limit.reflects (⇑(category_theory.limits.is_limit.of_cone_equiv (category_theory.limits.cones.postcompose_equivalence (category_theory.limits.comp_nat_iso F))) (((category_theory.limits.is_kernel.of_comp_iso category_theory.normal_mono.g (F.map (category_theory.full.preimage (category_theory.normal_mono.g ≫ (F.fun_obj_preimage_iso (category_theory.normal_mono.Z (F.map f))).inv))) (F.fun_obj_preimage_iso (category_theory.normal_mono.Z (F.map f))) _ category_theory.normal_mono.is_limit).of_iso_limit (category_theory.limits.of_ι_congr _)).of_iso_limit (category_theory.limits.iso_of_ι ((category_theory.limits.cones.postcompose_equivalence (category_theory.limits.comp_nat_iso F)).functor.obj (F.map_cone (category_theory.limits.kernel_fork.of_ι f _)))).symm))}
@[instance]
def
category_theory.normal_mono.regular_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[I : category_theory.normal_mono f] :
Every normal monomorphism is a regular monomorphism.
Equations
- category_theory.normal_mono.regular_mono f = {Z := category_theory.normal_mono.Z f I, left := category_theory.normal_mono.g I, right := 0, w := _, is_limit := category_theory.normal_mono.is_limit I}
def
category_theory.normal_mono.lift'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{W : C}
(f : X ⟶ Y)
[category_theory.normal_mono f]
(k : W ⟶ Y) :
k ≫ category_theory.normal_mono.g = 0 → {l // l ≫ f = k}
If f is a normal mono, then any map k : W ⟶ Y such that k ≫ normal_mono.g = 0 induces
a morphism l : W ⟶ X such that l ≫ f = k.
def
category_theory.normal_of_is_pullback_snd_of_normal
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[hn : category_theory.normal_mono h]
(comm : f ≫ h = g ≫ k) :
The second leg of a pullback cone is a normal monomorphism if the right component is too.
See also pullback.snd_of_mono for the basic monomorphism version, and
normal_of_is_pullback_fst_of_normal for the flipped version.
Equations
- category_theory.normal_of_is_pullback_snd_of_normal comm t = {Z := category_theory.normal_mono.Z h hn, g := k ≫ category_theory.normal_mono.g, w := _, is_limit := let gr : category_theory.regular_mono g := category_theory.regular_of_is_pullback_snd_of_regular comm t in _.mpr category_theory.regular_mono.is_limit}
def
category_theory.normal_of_is_pullback_fst_of_normal
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[hn : category_theory.normal_mono k]
(comm : f ≫ h = g ≫ k) :
The first leg of a pullback cone is a normal monomorphism if the left component is too.
See also pullback.fst_of_mono for the basic monomorphism version, and
normal_of_is_pullback_snd_of_normal for the flipped version.
@[class]
structure
category_theory.regular_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C} :
(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.
@[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.
Equations
- _ = _
@[instance]
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) _ _}
@[instance]
def
category_theory.regular_epi.of_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.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.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) :
category_theory.regular_epi.left ≫ k = category_theory.regular_epi.right ≫ k → {l // f ≫ l = 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) :
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) :
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.
def
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.
@[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] :
Equations
- category_theory.strong_epi_of_regular_epi f = {epi := _, has_lift := λ (X_1 Y_1 : C) (u : X ⟶ X_1) (v : Y ⟶ Y_1) (z : X_1 ⟶ Y_1) (_inst_2_1 : category_theory.mono z) (h : u ≫ z = f ≫ v), (category_theory.regular_epi.desc' f u _).cases_on (λ (t : Y ⟶ X_1) (ht : f ≫ t = u), {lift := t, fac_left := ht, fac_right := _})}
@[class]
structure
category_theory.normal_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C] :
(X ⟶ Y) → Type (max u₁ v₁)
- W : C
- g : category_theory.normal_epi.W f ⟶ X
- w : category_theory.normal_epi.g ≫ f = 0
- is_colimit : category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π f category_theory.normal_epi.w)
A normal epimorphism is a morphism which is the cokernel of some morphism.
def
category_theory.equivalence_reflects_normal_epi
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[category_theory.is_equivalence F]
{X Y : C}
{f : X ⟶ Y} :
If F is an equivalence and F.map f is a normal epi, then f is a normal epi.
Equations
- category_theory.equivalence_reflects_normal_epi F hf = {W := F.obj_preimage (category_theory.normal_epi.W (F.map f)), g := category_theory.full.preimage ((F.fun_obj_preimage_iso (category_theory.normal_epi.W (F.map f))).hom ≫ category_theory.normal_epi.g), w := _, is_colimit := category_theory.limits.reflects_colimit.reflects (⇑(category_theory.limits.is_colimit.of_cocone_equiv (category_theory.limits.cocones.precompose_equivalence (category_theory.limits.comp_nat_iso F).symm)) (((category_theory.limits.is_cokernel.of_iso_comp category_theory.normal_epi.g (F.map (category_theory.full.preimage ((F.fun_obj_preimage_iso (category_theory.normal_epi.W (F.map f))).hom ≫ category_theory.normal_epi.g))) (F.fun_obj_preimage_iso (category_theory.normal_epi.W (F.map f))).symm _ category_theory.normal_epi.is_colimit).of_iso_colimit (category_theory.limits.of_π_congr _)).of_iso_colimit (category_theory.limits.iso_of_π ((category_theory.limits.cocones.precompose_equivalence (category_theory.limits.comp_nat_iso F).symm).functor.obj (F.map_cocone (category_theory.limits.cokernel_cofork.of_π f _)))).symm))}
@[instance]
def
category_theory.normal_epi.regular_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[I : category_theory.normal_epi f] :
Every normal epimorphism is a regular epimorphism.
Equations
- category_theory.normal_epi.regular_epi f = {W := category_theory.normal_epi.W f I, left := category_theory.normal_epi.g I, right := 0, w := _, is_colimit := category_theory.normal_epi.is_colimit I}
def
category_theory.normal_epi.desc'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{W : C}
(f : X ⟶ Y)
[category_theory.normal_epi f]
(k : X ⟶ W) :
category_theory.normal_epi.g ≫ k = 0 → {l // f ≫ l = k}
If f is a normal epi, then every morphism k : X ⟶ W satisfying normal_epi.g ≫ k = 0
induces l : Y ⟶ W such that f ≫ l = k.
def
category_theory.normal_of_is_pushout_snd_of_normal
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[gn : category_theory.normal_epi g]
(comm : f ≫ h = g ≫ k) :
The second leg of a pushout cocone is a normal epimorphism if the right component is too.
See also pushout.snd_of_epi for the basic epimorphism version, and
normal_of_is_pushout_fst_of_normal for the flipped version.
Equations
- category_theory.normal_of_is_pushout_snd_of_normal comm t = {W := category_theory.normal_epi.W g gn, g := category_theory.normal_epi.g ≫ f, w := _, is_colimit := let hn : category_theory.regular_epi h := category_theory.regular_of_is_pushout_snd_of_regular comm t in _.mpr category_theory.regular_epi.is_colimit}
def
category_theory.normal_of_is_pushout_fst_of_normal
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q R S : C}
{f : P ⟶ Q}
{g : P ⟶ R}
{h : Q ⟶ S}
{k : R ⟶ S}
[hn : category_theory.normal_epi f]
(comm : f ≫ h = g ≫ k) :
The first leg of a pushout cocone is a normal epimorphism if the left component is too.
See also pushout.fst_of_epi for the basic epimorphism version, and
normal_of_is_pushout_snd_of_normal for the flipped version.