# The opposite of an abelian category is abelian. #

Equations
• = CategoryTheory.Abelian.mk
@[simp]
theorem CategoryTheory.kernelOpUnop_inv {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.inv =
@[simp]
theorem CategoryTheory.kernelOpUnop_hom {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.hom = ().unop
def CategoryTheory.kernelOpUnop {C : Type u_1} [] {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_inv {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.inv = ().unop
@[simp]
theorem CategoryTheory.cokernelOpUnop_hom {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.hom =
def CategoryTheory.cokernelOpUnop {C : Type u_1} [] {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} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.inv =
@[simp]
theorem CategoryTheory.kernelUnopOp_hom {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.hom = ().op
def CategoryTheory.kernelUnopOp {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
{ unop := }

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

Equations
Instances For
@[simp]
theorem CategoryTheory.cokernelUnopOp_hom {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.hom =
@[simp]
theorem CategoryTheory.cokernelUnopOp_inv {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.inv = ().op
def CategoryTheory.cokernelUnopOp {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
{ unop := }

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

Equations
Instances For
theorem CategoryTheory.cokernel.π_op {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.kernel.ι_op {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.kernelOpOp_hom {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.hom = ().op
@[simp]
theorem CategoryTheory.kernelOpOp_inv {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.inv =
def CategoryTheory.kernelOpOp {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
{ unop := }

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

Equations
• = .op.symm
Instances For
@[simp]
theorem CategoryTheory.cokernelOpOp_hom {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.cokernelOpOp_inv {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
.inv = ().op
def CategoryTheory.cokernelOpOp {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
{ unop := }

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

Equations
Instances For
@[simp]
theorem CategoryTheory.kernelUnopUnop_hom {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.hom = ().unop
@[simp]
theorem CategoryTheory.kernelUnopUnop_inv {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.inv =
def CategoryTheory.kernelUnopUnop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.unop

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

Equations
• = .unop.symm
Instances For
theorem CategoryTheory.kernel.ι_unop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
theorem CategoryTheory.cokernel.π_unop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
@[simp]
theorem CategoryTheory.cokernelUnopUnop_hom {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.hom =
@[simp]
theorem CategoryTheory.cokernelUnopUnop_inv {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.inv = ().unop
def CategoryTheory.cokernelUnopUnop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.unop

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

Equations
• = .unop.symm
Instances For
def CategoryTheory.imageUnopOp {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
{ unop := }

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} [] {X : C} {Y : C} (f : X Y) :
{ unop := }

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

Equations
Instances For
def CategoryTheory.imageOpUnop {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
().unop

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

Equations
• = ().unop
Instances For
def CategoryTheory.imageUnopUnop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
.unop

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} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
theorem CategoryTheory.imageUnopOp_hom_comp_image_ι {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :
theorem CategoryTheory.factorThruImage_comp_imageUnopOp_inv {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A B) :