Definitions and basic properties of normal monomorphisms and epimorphisms. #
A normal monomorphism is a morphism that is the kernel of some other morphism.
We give the construction normal_mono → regular_mono (category_theory.normal_mono.regular_mono)
as well as the dual construction for normal epimorphisms. We show equivalences reflect normal
monomorphisms (category_theory.equivalence_reflects_normal_mono), and that the pullback of a
normal monomorphism is normal (category_theory.normal_of_is_pullback_snd_of_normal).
@[class]
structure
category_theory.normal_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : 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}
(hf : category_theory.normal_mono (F.map f)) :
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.obj_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.obj_obj_preimage_iso (category_theory.normal_mono.Z (F.map f))).inv))) (F.obj_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))}
@[protected, 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)
(h : k ≫ category_theory.normal_mono.g = 0) :
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)
(t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm)) :
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)
(t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm)) :
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.normal_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : 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}
(hf : category_theory.normal_epi (F.map f)) :
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.obj_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.obj_obj_preimage_iso (category_theory.normal_epi.W (F.map f))).hom ≫ category_theory.normal_epi.g))) (F.obj_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))}
@[protected, 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)
(h : category_theory.normal_epi.g ≫ k = 0) :
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)
(t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h k comm)) :
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)
(t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h k comm)) :
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.
def
category_theory.normal_epi_of_normal_mono_unop
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
(m : category_theory.normal_mono f.unop) :
A normal mono becomes a normal epi in the opposite category.
Equations
- category_theory.normal_epi_of_normal_mono_unop f m = {W := opposite.op (category_theory.normal_mono.Z f.unop), g := category_theory.normal_mono.g.op, w := _, is_colimit := category_theory.limits.is_colimit.of_π f _ (λ (Z' : Cᵒᵖ) (g' : X ⟶ Z') (w' : category_theory.normal_mono.g.op ≫ g' = 0), (category_theory.limits.kernel_fork.is_limit.lift' category_theory.normal_mono.is_limit g'.unop _).val.op) _ _}
def
category_theory.normal_mono_of_normal_epi_unop
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
(m : category_theory.normal_epi f.unop) :
A normal epi becomes a normal mono in the opposite category.
Equations
- category_theory.normal_mono_of_normal_epi_unop f m = {Z := opposite.op (category_theory.normal_epi.W f.unop), g := category_theory.normal_epi.g.op, w := _, is_limit := category_theory.limits.is_limit.of_ι f _ (λ (Z' : Cᵒᵖ) (g' : Z' ⟶ Y) (w' : g' ≫ category_theory.normal_epi.g.op = 0), (category_theory.limits.cokernel_cofork.is_colimit.desc' category_theory.normal_epi.is_colimit g'.unop _).val.op) _ _}