Definitions and basic properties of normal monomorphisms and epimorphisms. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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).
We also define classes normal_mono_category and normal_epi_category for classes in which
every monomorphism or epimorphism is normal, and deduce that these categories are
regular_mono_categorys resp. regular_epi_categorys.
- 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.
Instances for category_theory.normal_mono
- category_theory.normal_mono.has_sizeof_inst
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))}
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}
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.
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}
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.
- normal_mono_of_mono : Π {X Y : C} (f : X ⟶ Y) [_inst_3 : category_theory.mono f], category_theory.normal_mono f
A normal mono category is a category in which every monomorphism is normal.
Instances of this typeclass
Instances of other typeclasses for category_theory.normal_mono_category
- category_theory.normal_mono_category.has_sizeof_inst
In a category in which every monomorphism is normal, we can express every monomorphism as a kernel. This is not an instance because it would create an instance loop.
Equations
- category_theory.regular_mono_category_of_normal_mono_category = {regular_mono_of_mono := λ (_x _x_1 : C) (f : _x ⟶ _x_1) (_x_2 : category_theory.mono f), category_theory.normal_mono.regular_mono f}
- 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.
Instances for category_theory.normal_epi
- category_theory.normal_epi.has_sizeof_inst
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))}
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}
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.
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}
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.
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.cokernel_cofork.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) _ _}
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.kernel_fork.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) _ _}
- normal_epi_of_epi : Π {X Y : C} (f : X ⟶ Y) [_inst_3 : category_theory.epi f], category_theory.normal_epi f
A normal epi category is a category in which every epimorphism is normal.
Instances of this typeclass
Instances of other typeclasses for category_theory.normal_epi_category
- category_theory.normal_epi_category.has_sizeof_inst
In a category in which every epimorphism is normal, we can express every epimorphism as a kernel. This is not an instance because it would create an instance loop.
Equations
- category_theory.regular_epi_category_of_normal_epi_category = {regular_epi_of_epi := λ (_x _x_1 : C) (f : _x ⟶ _x_1) (_x_2 : category_theory.epi f), category_theory.normal_epi.regular_epi f}