mathlib documentation

category_theory.abelian.opposite

The opposite of an abelian category is abelian. #

source
@[protected, instance]
def category_theory.opposite.abelian (C : Type u_1) [category_theory.category C] [category_theory.abelian C] :
category_theory.abelian Cᵒᵖ
Equations
source
@[simp]
theorem category_theory.kernel_op_unop_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.kernel_op_unop f).hom = (category_theory.limits.kernel.lift f.op (category_theory.limits.cokernel.π f).op _).unop
source
@[simp]
theorem category_theory.kernel_op_unop_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.kernel_op_unop f).inv = category_theory.limits.cokernel.desc f (category_theory.limits.kernel.ι f.op).unop _
source
noncomputable def category_theory.kernel_op_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
opposite.unop (category_theory.limits.kernel f.op) ≅ category_theory.limits.cokernel f

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

Equations
source
@[simp]
theorem category_theory.cokernel_op_unop_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.cokernel_op_unop f).hom = category_theory.limits.kernel.lift f (category_theory.limits.cokernel.π f.op).unop _
source
noncomputable def category_theory.cokernel_op_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
opposite.unop (category_theory.limits.cokernel f.op) ≅ category_theory.limits.kernel f

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

Equations
source
@[simp]
theorem category_theory.cokernel_op_unop_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.cokernel_op_unop f).inv = (category_theory.limits.cokernel.desc f.op (category_theory.limits.kernel.ι f).op _).unop
source
@[simp]
theorem category_theory.kernel_unop_op_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.kernel_unop_op g).inv = category_theory.limits.cokernel.desc g (category_theory.limits.kernel.ι g.unop).op _
source
noncomputable def category_theory.kernel_unop_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
opposite.op (category_theory.limits.kernel g.unop) ≅ category_theory.limits.cokernel g

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

Equations
source
@[simp]
theorem category_theory.kernel_unop_op_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.kernel_unop_op g).hom = (category_theory.limits.kernel.lift g.unop (category_theory.limits.cokernel.π g).unop _).op
source
noncomputable def category_theory.cokernel_unop_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
opposite.op (category_theory.limits.cokernel g.unop) ≅ category_theory.limits.kernel g

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

Equations
source
@[simp]
theorem category_theory.cokernel_unop_op_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.cokernel_unop_op g).inv = (category_theory.limits.cokernel.desc g.unop (category_theory.limits.kernel.ι g).unop _).op
source
@[simp]
theorem category_theory.cokernel_unop_op_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.cokernel_unop_op g).hom = category_theory.limits.kernel.lift g (category_theory.limits.cokernel.π g.unop).op _
source
theorem category_theory.cokernel.π_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.limits.cokernel.π f.op).unop = (category_theory.cokernel_op_unop f).hom ≫ category_theory.limits.kernel.ι f ≫ category_theory.eq_to_hom _
source
theorem category_theory.kernel.ι_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.limits.kernel.ι f.op).unop = category_theory.eq_to_hom _ ≫ category_theory.limits.cokernel.π f ≫ (category_theory.kernel_op_unop f).inv
source
noncomputable def category_theory.kernel_op_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
category_theory.limits.kernel f.op ≅ opposite.op (category_theory.limits.cokernel f)

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

Equations
source
@[simp]
theorem category_theory.kernel_op_op_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.kernel_op_op f).hom = (category_theory.limits.cokernel.desc f (category_theory.limits.kernel.ι f.op).unop _).op
source
@[simp]
theorem category_theory.kernel_op_op_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.kernel_op_op f).inv = category_theory.limits.kernel.lift f.op (category_theory.limits.cokernel.π f).op _
source
@[simp]
theorem category_theory.cokernel_op_op_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.cokernel_op_op f).hom = category_theory.limits.cokernel.desc f.op (category_theory.limits.kernel.ι f).op _
source
noncomputable def category_theory.cokernel_op_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
category_theory.limits.cokernel f.op ≅ opposite.op (category_theory.limits.kernel f)

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

Equations
source
@[simp]
theorem category_theory.cokernel_op_op_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :
(category_theory.cokernel_op_op f).inv = (category_theory.limits.kernel.lift f (category_theory.limits.cokernel.π f.op).unop _).op
source
@[simp]
theorem category_theory.kernel_unop_unop_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.kernel_unop_unop g).inv = category_theory.limits.kernel.lift g.unop (category_theory.limits.cokernel.π g).unop _
source
noncomputable def category_theory.kernel_unop_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
category_theory.limits.kernel g.unop ≅ opposite.unop (category_theory.limits.cokernel g)

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

Equations
source
@[simp]
theorem category_theory.kernel_unop_unop_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.kernel_unop_unop g).hom = (category_theory.limits.cokernel.desc g (category_theory.limits.kernel.ι g.unop).op _).unop
source
theorem category_theory.kernel.ι_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.limits.kernel.ι g.unop).op = category_theory.eq_to_hom _ ≫ category_theory.limits.cokernel.π g ≫ (category_theory.kernel_unop_op g).inv
source
theorem category_theory.cokernel.π_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.limits.cokernel.π g.unop).op = (category_theory.cokernel_unop_op g).hom ≫ category_theory.limits.kernel.ι g ≫ category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.cokernel_unop_unop_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.cokernel_unop_unop g).inv = (category_theory.limits.kernel.lift g (category_theory.limits.cokernel.π g.unop).op _).unop
source
@[simp]
theorem category_theory.cokernel_unop_unop_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
(category_theory.cokernel_unop_unop g).hom = category_theory.limits.cokernel.desc g.unop (category_theory.limits.kernel.ι g).unop _
source
noncomputable def category_theory.cokernel_unop_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :
category_theory.limits.cokernel g.unop ≅ opposite.unop (category_theory.limits.kernel g)

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

Equations