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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.