The opposite of an abelian category is abelian. #

source

instance CategoryTheory.instAbelianOppositeOpposite (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :

CategoryTheory.Abelian Cᵒᵖ

source

@[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 (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.kernel.ι f.op).unop = 0)

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π f)).op = 0)).unop

source

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.

Instances For

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) f).op = 0)).unop

source

@[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 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f.op).unop f = 0)

source

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.

Instances For

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g.unop) g.unop).op = 0)

source

@[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 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g.unop.op).unop g.unop = 0)).op

source

def CategoryTheory.kernelUnopOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A ⟶ B) :

Opposite.op (CategoryTheory.Limits.kernel g.unop) ≅ CategoryTheory.Limits.cokernel g

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

Instances For

source

@[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 (_ : CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.Limits.kernel.ι g.unop.op).unop = 0)).op

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.Limits.cokernel.π g.unop)).op = 0)

source

def CategoryTheory.cokernelUnopOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A : Cᵒᵖ} {B : Cᵒᵖ} (g : A ⟶ B) :

Opposite.op (CategoryTheory.Limits.cokernel g.unop) ≅ CategoryTheory.Limits.kernel g

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

Instances For

source

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 (_ : X = (Opposite.op X).unop)))

source

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 (_ : (Opposite.op Y).unop = Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.kernelOpUnop f).inv)

source

@[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 (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.kernel.ι f.op).unop = 0)).op

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π f)).op = 0)

source

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 ≅ Opposite.op (CategoryTheory.Limits.cokernel f)

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

Instances For

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) f).op = 0)

source

@[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 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f.op).unop f = 0)).op

source

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 ≅ Opposite.op (CategoryTheory.Limits.kernel f)

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

Instances For

source

@[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 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g.unop.op).unop g.unop = 0)

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g.unop) g.unop).op = 0)).unop

source

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.

Instances For

source

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 (_ : Opposite.op B.unop = B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) (CategoryTheory.kernelUnopOp g).inv)

source

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 (_ : A = Opposite.op A.unop)))

source

@[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 (_ : CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.Limits.kernel.ι g.unop.op).unop = 0)

source

@[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 (_ : (CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.Limits.cokernel.π g.unop)).op = 0)).unop

source

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.

Instances For

source

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

Opposite.op (CategoryTheory.Limits.image g.unop) ≅ CategoryTheory.Limits.image g

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

Instances For

source

def CategoryTheory.imageOpOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) :

Opposite.op (CategoryTheory.Limits.image f) ≅ CategoryTheory.Limits.image f.op

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

source

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

source

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

source

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