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ᵒᵖ

Equations

CategoryTheory.instAbelianOppositeOpposite C = CategoryTheory.Abelian.mk

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 ⋯

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 ⋯).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.

Equations

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

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 ⋯).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 ⋯

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.

Equations

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

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 ⋯

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 ⋯).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.

Equations

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

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 ⋯).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 ⋯

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.

Equations

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

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 ⋯))

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 ⋯) (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 ⋯).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 ⋯

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.

Equations

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

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 ⋯

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 ⋯).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.

Equations

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

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 ⋯

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 ⋯).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.

Equations

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

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 ⋯) (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 ⋯))

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 ⋯

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 ⋯).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.

Equations

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

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.

Equations

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

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.

Equations

CategoryTheory.imageOpOp f = CategoryTheory.imageUnopOp 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.

Equations

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

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.

Equations

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

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

Documentation

Mathlib.CategoryTheory.Abelian.Opposite

The opposite of an abelian category is abelian. #