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] : 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) : (CategoryTheory.Limits.kernel f.op).unop ≅ CategoryTheory.Limits.cokernel f

The kernel of f.op is the opposite of cokernel f.

Equations

• One or more equations did not get rendered due to their size.

@[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

@[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 ⋯

def CategoryTheory.cokernelOpUnop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.cokernel f.op).unop ≅ CategoryTheory.Limits.kernel f

The cokernel of f.op is the opposite of kernel f.

Equations

• One or more equations did not get rendered due to their size.

@[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) : { unop := CategoryTheory.Limits.kernel g.unop } ≅ CategoryTheory.Limits.cokernel g

The kernel of g.unop is the opposite of cokernel g.

Equations

• CategoryTheory.kernelUnopOp g = (CategoryTheory.cokernelOpUnop g.unop).op

@[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) : { unop := CategoryTheory.Limits.cokernel g.unop } ≅ CategoryTheory.Limits.kernel g

The cokernel of g.unop is the opposite of kernel g.

Equations

• CategoryTheory.cokernelUnopOp g = (CategoryTheory.kernelOpUnop g.unop).op

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) : (CategoryTheory.Limits.cokernel.π f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelOpUnop f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.eqToHom ⋯))

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) : (CategoryTheory.Limits.kernel.ι f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.kernelOpUnop f).inv)

@[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

@[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 ⋯

def CategoryTheory.kernelOpOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.kernel f.op ≅ { unop := CategoryTheory.Limits.cokernel f }

The kernel of f.op is the opposite of cokernel f.

Equations

• CategoryTheory.kernelOpOp f = (CategoryTheory.kernelOpUnop f).op.symm

@[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) : CategoryTheory.Limits.cokernel f.op ≅ { unop := CategoryTheory.Limits.kernel f }

The cokernel of f.op is the opposite of kernel f.

Equations

• CategoryTheory.cokernelOpOp f = (CategoryTheory.cokernelOpUnop f).op.symm

@[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

@[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 ⋯

def CategoryTheory.kernelUnopUnop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.Limits.kernel g.unop ≅ (CategoryTheory.Limits.cokernel g).unop

The kernel of g.unop is the opposite of cokernel g.

Equations

• CategoryTheory.kernelUnopUnop g = (CategoryTheory.kernelUnopOp g).unop.symm

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) : (CategoryTheory.Limits.kernel.ι g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) (CategoryTheory.kernelUnopOp g).inv)

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) : (CategoryTheory.Limits.cokernel.π g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelUnopOp g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯))

@[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 ⋯

@[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

def CategoryTheory.cokernelUnopUnop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.Limits.cokernel g.unop ≅ (CategoryTheory.Limits.kernel g).unop

The cokernel of g.unop is the opposite of kernel g.

Equations

• CategoryTheory.cokernelUnopUnop g = (CategoryTheory.cokernelUnopOp g).unop.symm

def CategoryTheory.imageUnopOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A ⟶ B) : { unop := CategoryTheory.Limits.image g.unop } ≅ CategoryTheory.Limits.image g

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.

def CategoryTheory.imageOpOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) : { unop := CategoryTheory.Limits.image f } ≅ CategoryTheory.Limits.image f.op

The opposite of the image of f is the image of f.op.

Equations

• CategoryTheory.imageOpOp f = CategoryTheory.imageUnopOp f.op

def CategoryTheory.imageOpUnop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.image f.op).unop ≅ CategoryTheory.Limits.image f

The image of f.op is the opposite of the image of f.

Equations

• CategoryTheory.imageOpUnop f = (CategoryTheory.imageUnopOp f.op).unop

def CategoryTheory.imageUnopUnop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.Limits.image g).unop ≅ CategoryTheory.Limits.image g.unop

The image of g is the opposite of the image of g.unop.

Equations

• CategoryTheory.imageUnopUnop g = (CategoryTheory.imageUnopOp g).unop

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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.unop).op (CategoryTheory.imageUnopOp g).hom = CategoryTheory.Limits.factorThruImage g

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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).hom (CategoryTheory.Limits.image.ι g) = (CategoryTheory.Limits.factorThruImage g.unop).op

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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) (CategoryTheory.imageUnopOp g).inv = (CategoryTheory.Limits.image.ι g.unop).op

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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).inv (CategoryTheory.Limits.factorThruImage g.unop).op = CategoryTheory.Limits.image.ι g