CategoryTheory.Limits.PreservesKernel.iso_hom
theorem CategoryTheory.Limits.PreservesKernel.iso_hom :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
[inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
[inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
(CategoryTheory.Limits.PreservesKernel.iso G f).hom = CategoryTheory.Limits.kernelComparison f G
This theorem states that, for any categories `C` and `D` with zero morphisms, a functor `G` from `C` to `D` that preserves zero morphisms, and a morphism `f` from `X` to `Y` in `C` that has a kernel, if `G` preserves the limit of the parallel pair of `f` and `0`, then the morphism defined by the isomorphism between the kernels of `f` and `G.map(f)` is the same as the kernel comparison of `f` and `G`. This means that the process of mapping `f` to `D` and then taking the kernel is equivalent to first taking the kernel in `C` and then mapping to `D` under certain conditions on `G`.
More concisely: If functor G from categories C and D with zero morphisms preserves limits and zero morphisms, and preserves kernels of morphisms in C, then the kernel of G(f) is isomorphic to the image of the kernel of f under G, for any morphism f in C with a kernel.
|
CategoryTheory.Limits.PreservesCokernel.iso_inv
theorem CategoryTheory.Limits.PreservesCokernel.iso_inv :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
[inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
[inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
(CategoryTheory.Limits.PreservesCokernel.iso G f).inv = CategoryTheory.Limits.cokernelComparison f G
The theorem `CategoryTheory.Limits.PreservesCokernel.iso_inv` states that for any categories `C` and `D` with zero morphisms, and a functor `G` from `C` to `D` that preserves zero morphisms, given objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y` that has a cokernel in both `C` and `D`, and assuming the functor `G` preserves the colimit of the parallel pair consisting of `f` and the zero morphism, then the inverse of the preserving cokernel isomorphism of `G` mapping `f` is equal to the cokernel comparison of `f` with `G`. In simpler terms, it states that under certain conditions, we can relate the inverse of a certain isomorphism involving cokernels to a notion called cokernel comparison.
More concisely: Given functors between zero-morphism categories `G: C -> D` that preserve zero morphisms, if `f: X -> Y` in `C` has cokernels `K` in both `C` and `D` and `G` preserves the colimit of `(f, 0_on_X)`, then `iso_inv(G.mapCokernel f) = cokernelComparison f G`.
|