The opposite of an abelian category is abelian. #
instance
CategoryTheory.instAbelianOpposite
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
:
Equations
- CategoryTheory.instAbelianOpposite C = CategoryTheory.Abelian.mk
@[simp]
theorem
CategoryTheory.kernelOpUnop_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.kernelOpUnop f).inv = CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯
@[simp]
theorem
CategoryTheory.kernelOpUnop_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.kernelOpUnop f).hom = (CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯).unop
def
CategoryTheory.kernelOpUnop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The kernel of f.op
is the opposite of cokernel f
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.cokernelOpUnop_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.cokernelOpUnop f).hom = CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯
@[simp]
theorem
CategoryTheory.cokernelOpUnop_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.cokernelOpUnop f).inv = (CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯).unop
def
CategoryTheory.cokernelOpUnop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The cokernel of f.op
is the opposite of kernel f
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.kernelUnopOp_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.kernelUnopOp g).inv = CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯
@[simp]
theorem
CategoryTheory.kernelUnopOp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.kernelUnopOp g).hom = (CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯).op
def
CategoryTheory.kernelUnopOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
The kernel of g.unop
is the opposite of cokernel g
.
Equations
- CategoryTheory.kernelUnopOp g = (CategoryTheory.cokernelOpUnop g.unop).op
Instances For
@[simp]
theorem
CategoryTheory.cokernelUnopOp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.cokernelUnopOp g).hom = CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯
@[simp]
theorem
CategoryTheory.cokernelUnopOp_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.cokernelUnopOp g).inv = (CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯).op
def
CategoryTheory.cokernelUnopOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
The cokernel of g.unop
is the opposite of kernel g
.
Equations
- CategoryTheory.cokernelUnopOp g = (CategoryTheory.kernelOpUnop g.unop).op
Instances For
theorem
CategoryTheory.cokernel.π_op
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.kernel.ι_op
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.kernelOpOp_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.kernelOpOp f).inv = CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯
@[simp]
theorem
CategoryTheory.kernelOpOp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.kernelOpOp f).hom = (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯).op
def
CategoryTheory.kernelOpOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The kernel of f.op
is the opposite of cokernel f
.
Equations
- CategoryTheory.kernelOpOp f = (CategoryTheory.kernelOpUnop f).op.symm
Instances For
@[simp]
theorem
CategoryTheory.cokernelOpOp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.cokernelOpOp f).hom = CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯
@[simp]
theorem
CategoryTheory.cokernelOpOp_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.cokernelOpOp f).inv = (CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯).op
def
CategoryTheory.cokernelOpOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The cokernel of f.op
is the opposite of kernel f
.
Equations
- CategoryTheory.cokernelOpOp f = (CategoryTheory.cokernelOpUnop f).op.symm
Instances For
@[simp]
theorem
CategoryTheory.kernelUnopUnop_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.kernelUnopUnop g).inv = CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯
@[simp]
theorem
CategoryTheory.kernelUnopUnop_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.kernelUnopUnop g).hom = (CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯).unop
def
CategoryTheory.kernelUnopUnop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
The kernel of g.unop
is the opposite of cokernel g
.
Equations
- CategoryTheory.kernelUnopUnop g = (CategoryTheory.kernelUnopOp g).unop.symm
Instances For
theorem
CategoryTheory.kernel.ι_unop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
theorem
CategoryTheory.cokernel.π_unop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
@[simp]
theorem
CategoryTheory.cokernelUnopUnop_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.cokernelUnopUnop g).inv = (CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯).unop
@[simp]
theorem
CategoryTheory.cokernelUnopUnop_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
(CategoryTheory.cokernelUnopUnop g).hom = CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯
def
CategoryTheory.cokernelUnopUnop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
The cokernel of g.unop
is the opposite of kernel g
.
Equations
- CategoryTheory.cokernelUnopUnop g = (CategoryTheory.cokernelUnopOp g).unop.symm
Instances For
def
CategoryTheory.imageUnopOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
The opposite of the image of g.unop
is the image of g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.imageOpOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The opposite of the image of f
is the image of f.op
.
Equations
Instances For
def
CategoryTheory.imageOpUnop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The image of f.op
is the opposite of the image of f
.
Equations
- CategoryTheory.imageOpUnop f = (CategoryTheory.imageUnopOp f.op).unop
Instances For
def
CategoryTheory.imageUnopUnop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
The image of g
is the opposite of the image of g.unop.
Equations
Instances For
theorem
CategoryTheory.image_ι_op_comp_imageUnopOp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
theorem
CategoryTheory.imageUnopOp_hom_comp_image_ι
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
theorem
CategoryTheory.factorThruImage_comp_imageUnopOp_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
:
theorem
CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Abelian C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
(g : A ⟶ B)
: