# mathlibdocumentation

category_theory.abelian.opposite

# The opposite of an abelian category is abelian. #

@[protected, instance]
def category_theory.opposite.abelian (C : Type u_1)  :
Equations
@[simp]
theorem category_theory.kernel_op_unop_hom {C : Type u_1} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.kernel_op_unop_inv {C : Type u_1} {X Y : C} (f : X Y) :
noncomputable def category_theory.kernel_op_unop {C : Type u_1} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.cokernel_op_unop_hom {C : Type u_1} {X Y : C} (f : X Y) :
noncomputable def category_theory.cokernel_op_unop {C : Type u_1} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.cokernel_op_unop_inv {C : Type u_1} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.kernel_unop_op_inv {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
noncomputable def category_theory.kernel_unop_op {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :

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

Equations
@[simp]
theorem category_theory.kernel_unop_op_hom {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
noncomputable def category_theory.cokernel_unop_op {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :

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

Equations
@[simp]
theorem category_theory.cokernel_unop_op_inv {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
@[simp]
theorem category_theory.cokernel_unop_op_hom {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
theorem category_theory.cokernel.π_op {C : Type u_1} {X Y : C} (f : X Y) :
theorem category_theory.kernel.ι_op {C : Type u_1} {X Y : C} (f : X Y) :
noncomputable def category_theory.kernel_op_op {C : Type u_1} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.kernel_op_op_hom {C : Type u_1} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.kernel_op_op_inv {C : Type u_1} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.cokernel_op_op_hom {C : Type u_1} {X Y : C} (f : X Y) :
noncomputable def category_theory.cokernel_op_op {C : Type u_1} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.cokernel_op_op_inv {C : Type u_1} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.kernel_unop_unop_inv {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
noncomputable def category_theory.kernel_unop_unop {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :

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

Equations
@[simp]
theorem category_theory.kernel_unop_unop_hom {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
theorem category_theory.kernel.ι_unop {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
theorem category_theory.cokernel.π_unop {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
@[simp]
theorem category_theory.cokernel_unop_unop_inv {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
@[simp]
theorem category_theory.cokernel_unop_unop_hom {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :
noncomputable def category_theory.cokernel_unop_unop {C : Type u_1} {A B : Cᵒᵖ} (g : A B) :

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

Equations