Kernels and cokernels in C and Cᵒᵖ #
We construct kernels and cokernels in the opposite categories.
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{X Y Q : C}
(p : Y ⟶ Q)
{f : X ⟶ Y}
(w : CategoryStruct.comp f p = 0)
(h : IsColimit (CokernelCofork.ofπ p w))
:
IsLimit (KernelFork.ofι p.op ⋯)
A colimit cokernel cofork gives a limit kernel fork in the opposite category
Equations
Instances For
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{X Y Q : Cᵒᵖ}
(p : Y ⟶ Q)
{f : X ⟶ Y}
(w : CategoryStruct.comp f p = 0)
(h : IsColimit (CokernelCofork.ofπ p w))
:
IsLimit (KernelFork.ofι p.unop ⋯)
A colimit cokernel cofork in the opposite category gives a limit kernel fork in the original category
Equations
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofιOp
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{K X Y : C}
(i : K ⟶ X)
{f : X ⟶ Y}
(w : CategoryStruct.comp i f = 0)
(h : IsLimit (KernelFork.ofι i w))
:
IsColimit (CokernelCofork.ofπ i.op ⋯)
A limit kernel fork gives a colimit cokernel cofork in the opposite category
Equations
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{K X Y : Cᵒᵖ}
(i : K ⟶ X)
{f : X ⟶ Y}
(w : CategoryStruct.comp i f = 0)
(h : IsLimit (KernelFork.ofι i w))
:
IsColimit (CokernelCofork.ofπ i.unop ⋯)
A limit kernel fork in the opposite category gives a colimit cokernel cofork in the original category