Preserving (co)kernels #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Constructions to relate the notions of preserving (co)kernels and reflecting (co)kernels to concrete (co)forks.
In particular, we show that kernel_comparison f g G is an isomorphism iff G preserves
the limit of the parallel pair f,0, as well as the dual result.
def
category_theory.limits.is_limit_map_cone_fork_equiv'
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Z ⟶ X}
(w : h ≫ f = 0) :
The map of a kernel fork is a limit iff
the kernel fork consisting of the mapped morphisms is a limit.
This essentially lets us commute kernel_fork.of_ι with functor.map_cone.
This is a variant of is_limit_map_cone_fork_equiv for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Equations
- category_theory.limits.is_limit_map_cone_fork_equiv' G w = (category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.parallel_pair.ext (category_theory.iso.refl ((category_theory.limits.parallel_pair f 0 ⋙ G).obj category_theory.limits.walking_parallel_pair.zero)) (category_theory.iso.refl ((category_theory.limits.parallel_pair f 0 ⋙ G).obj category_theory.limits.walking_parallel_pair.one)) _ _) (G.map_cone (category_theory.limits.kernel_fork.of_ι h w))).symm.trans (category_theory.limits.is_limit.equiv_iso_limit (category_theory.limits.fork.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.parallel_pair.ext (category_theory.iso.refl ((category_theory.limits.parallel_pair f 0 ⋙ G).obj category_theory.limits.walking_parallel_pair.zero)) (category_theory.iso.refl ((category_theory.limits.parallel_pair f 0 ⋙ G).obj category_theory.limits.walking_parallel_pair.one)) _ _).hom).obj (G.map_cone (category_theory.limits.kernel_fork.of_ι h w))).X) _))
def
category_theory.limits.is_limit_fork_map_of_is_limit'
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Z ⟶ X}
(w : h ≫ f = 0)
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G]
(l : category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι h w)) :
The property of preserving kernels expressed in terms of kernel forks.
This is a variant of is_limit_fork_map_of_is_limit for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
noncomputable
def
category_theory.limits.is_limit_of_has_kernel_of_preserves_limit
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G] :
If G preserves kernels and C has them, then the fork constructed of the mapped morphisms of
a kernel fork is a limit.
@[protected, instance]
def
category_theory.limits.category_theory.functor.map.has_kernel
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G] :
noncomputable
def
category_theory.limits.preserves_kernel.of_iso_comparison
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel (G.map f)]
[i : category_theory.is_iso (category_theory.limits.kernel_comparison f G)] :
If the kernel comparison map for G at f is an isomorphism, then G preserves the
kernel of f.
Equations
- category_theory.limits.preserves_kernel.of_iso_comparison G f = category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.kernel_is_kernel f) (⇑((category_theory.limits.is_limit_map_cone_fork_equiv' G _).symm) (category_theory.limits.kernel_is_kernel (G.map f)).of_point_iso)
noncomputable
def
category_theory.limits.preserves_kernel.iso
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel (G.map f)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G] :
If G preserves the kernel of f, then the kernel comparison map for G at f is
an isomorphism.
@[simp]
theorem
category_theory.limits.preserves_kernel.iso_hom
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel (G.map f)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G] :
@[protected, instance]
def
category_theory.limits.kernel_comparison.category_theory.is_iso
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel (G.map f)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G] :
theorem
category_theory.limits.kernel_map_comp_preserves_kernel_iso_inv
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel (G.map f)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[category_theory.limits.has_kernel g]
[category_theory.limits.has_kernel (G.map g)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : f ≫ q = p ≫ g) :
category_theory.limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) _ ≫ (category_theory.limits.preserves_kernel.iso G g).inv = (category_theory.limits.preserves_kernel.iso G f).inv ≫ G.map (category_theory.limits.kernel.map f g p q hpq)
theorem
category_theory.limits.kernel_map_comp_preserves_kernel_iso_inv_assoc
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel (G.map f)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[category_theory.limits.has_kernel g]
[category_theory.limits.has_kernel (G.map g)]
[category_theory.limits.preserves_limit (category_theory.limits.parallel_pair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : f ≫ q = p ≫ g)
{X'_1 : D}
(f' : G.obj (category_theory.limits.kernel g) ⟶ X'_1) :
category_theory.limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) _ ≫ (category_theory.limits.preserves_kernel.iso G g).inv ≫ f' = (category_theory.limits.preserves_kernel.iso G f).inv ≫ G.map (category_theory.limits.kernel.map f g p q hpq) ≫ f'
def
category_theory.limits.is_colimit_map_cocone_cofork_equiv'
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
(w : f ≫ h = 0) :
The map of a cokernel cofork is a colimit iff
the cokernel cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute cokernel_cofork.of_π with functor.map_cocone.
This is a variant of is_colimit_map_cocone_cofork_equiv for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Equations
- category_theory.limits.is_colimit_map_cocone_cofork_equiv' G w = (category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.parallel_pair.ext (category_theory.iso.refl ((category_theory.limits.parallel_pair (G.map f) 0).obj category_theory.limits.walking_parallel_pair.zero)) (category_theory.iso.refl ((category_theory.limits.parallel_pair (G.map f) 0).obj category_theory.limits.walking_parallel_pair.one)) _ _) (G.map_cocone (category_theory.limits.cokernel_cofork.of_π h w))).symm.trans (category_theory.limits.is_colimit.equiv_iso_colimit (category_theory.limits.cofork.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.parallel_pair.ext (category_theory.iso.refl ((category_theory.limits.parallel_pair (G.map f) 0).obj category_theory.limits.walking_parallel_pair.zero)) (category_theory.iso.refl ((category_theory.limits.parallel_pair (G.map f) 0).obj category_theory.limits.walking_parallel_pair.one)) _ _).hom).obj (G.map_cocone (category_theory.limits.cokernel_cofork.of_π h w))).X) _))
def
category_theory.limits.is_colimit_cofork_map_of_is_colimit'
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
(w : f ≫ h = 0)
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G]
(l : category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π h w)) :
The property of preserving cokernels expressed in terms of cokernel coforks.
This is a variant of is_colimit_cofork_map_of_is_colimit for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
noncomputable
def
category_theory.limits.is_colimit_of_has_cokernel_of_preserves_colimit
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G] :
If G preserves cokernels and C has them, then the cofork constructed of the mapped morphisms of
a cokernel cofork is a colimit.
@[protected, instance]
def
category_theory.limits.category_theory.functor.map.has_cokernel
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G] :
noncomputable
def
category_theory.limits.preserves_cokernel.of_iso_comparison
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (G.map f)]
[i : category_theory.is_iso (category_theory.limits.cokernel_comparison f G)] :
If the cokernel comparison map for G at f is an isomorphism, then G preserves the
cokernel of f.
Equations
- category_theory.limits.preserves_cokernel.of_iso_comparison G f = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.cokernel_is_cokernel f) (⇑((category_theory.limits.is_colimit_map_cocone_cofork_equiv' G _).symm) (category_theory.limits.cokernel_is_cokernel (G.map f)).of_point_iso)
noncomputable
def
category_theory.limits.preserves_cokernel.iso
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (G.map f)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G] :
If G preserves the cokernel of f, then the cokernel comparison map for G at f is
an isomorphism.
@[simp]
theorem
category_theory.limits.preserves_cokernel.iso_inv
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (G.map f)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G] :
@[protected, instance]
def
category_theory.limits.cokernel_comparison.category_theory.is_iso
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (G.map f)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G] :
theorem
category_theory.limits.preserves_cokernel_iso_comp_cokernel_map_assoc
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (G.map f)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[category_theory.limits.has_cokernel g]
[category_theory.limits.has_cokernel (G.map g)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : f ≫ q = p ≫ g)
{X'_1 : D}
(f' : category_theory.limits.cokernel (G.map g) ⟶ X'_1) :
(category_theory.limits.preserves_cokernel.iso G f).hom ≫ category_theory.limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) _ ≫ f' = G.map (category_theory.limits.cokernel.map f g p q hpq) ≫ (category_theory.limits.preserves_cokernel.iso G g).hom ≫ f'
theorem
category_theory.limits.preserves_cokernel_iso_comp_cokernel_map
{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]
(G : C ⥤ D)
[G.preserves_zero_morphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (G.map f)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[category_theory.limits.has_cokernel g]
[category_theory.limits.has_cokernel (G.map g)]
[category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : f ≫ q = p ≫ g) :
(category_theory.limits.preserves_cokernel.iso G f).hom ≫ category_theory.limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) _ = G.map (category_theory.limits.cokernel.map f g p q hpq) ≫ (category_theory.limits.preserves_cokernel.iso G g).hom