The opposite of an abelian category is abelian.

@[instance_reducible]

instance CategoryTheory.instAbelianOpposite (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] : Abelian Cᵒᵖ

Equations

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

noncomputable def CategoryTheory.kernelOpUnop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (Limits.kernel f.op) ≅ 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.

@[simp]

theorem CategoryTheory.kernelOpUnop_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (kernelOpUnop f).hom = (Limits.kernel.lift f.op (Limits.cokernel.π f).op ⋯).unop

@[simp]

theorem CategoryTheory.kernelOpUnop_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (kernelOpUnop f).inv = Limits.cokernel.desc f (Limits.kernel.ι f.op).unop ⋯

noncomputable def CategoryTheory.cokernelOpUnop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (Limits.cokernel f.op) ≅ 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.

@[simp]

theorem CategoryTheory.cokernelOpUnop_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (cokernelOpUnop f).inv = (Limits.cokernel.desc f.op (Limits.kernel.ι f).op ⋯).unop

@[simp]

theorem CategoryTheory.cokernelOpUnop_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (cokernelOpUnop f).hom = Limits.kernel.lift f (Limits.cokernel.π f.op).unop ⋯

noncomputable def CategoryTheory.kernelUnopOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (Limits.kernel g.unop) ≅ Limits.cokernel g

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

Equations

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

@[simp]

theorem CategoryTheory.kernelUnopOp_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (kernelUnopOp g).inv = Limits.cokernel.desc g (Limits.kernel.ι g.unop).op ⋯

@[simp]

theorem CategoryTheory.kernelUnopOp_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (kernelUnopOp g).hom = (Limits.kernel.lift g.unop (Limits.cokernel.π g).unop ⋯).op

noncomputable def CategoryTheory.cokernelUnopOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (Limits.cokernel g.unop) ≅ Limits.kernel g

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

Equations

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

@[simp]

theorem CategoryTheory.cokernelUnopOp_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (cokernelUnopOp g).hom = Limits.kernel.lift g (Limits.cokernel.π g.unop).op ⋯

@[simp]

theorem CategoryTheory.cokernelUnopOp_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (cokernelUnopOp g).inv = (Limits.cokernel.desc g.unop (Limits.kernel.ι g).unop ⋯).op

theorem CategoryTheory.cokernel.π_op {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (Limits.cokernel.π f.op).unop = CategoryStruct.comp (cokernelOpUnop f).hom (CategoryStruct.comp (Limits.kernel.ι f) (eqToHom ⋯))

theorem CategoryTheory.kernel.ι_op {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (Limits.kernel.ι f.op).unop = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Limits.cokernel.π f) (kernelOpUnop f).inv)

noncomputable def CategoryTheory.kernelOpOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : Limits.kernel f.op ≅ Opposite.op (Limits.cokernel f)

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

Equations

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

@[simp]

theorem CategoryTheory.kernelOpOp_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (kernelOpOp f).hom = (Limits.cokernel.desc f (Limits.kernel.ι f.op).unop ⋯).op

@[simp]

theorem CategoryTheory.kernelOpOp_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (kernelOpOp f).inv = Limits.kernel.lift f.op (Limits.cokernel.π f).op ⋯

noncomputable def CategoryTheory.cokernelOpOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : Limits.cokernel f.op ≅ Opposite.op (Limits.kernel f)

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

Equations

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

@[simp]

theorem CategoryTheory.cokernelOpOp_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (cokernelOpOp f).inv = (Limits.kernel.lift f (Limits.cokernel.π f.op).unop ⋯).op

@[simp]

theorem CategoryTheory.cokernelOpOp_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (cokernelOpOp f).hom = Limits.cokernel.desc f.op (Limits.kernel.ι f).op ⋯

noncomputable def CategoryTheory.kernelUnopUnop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Limits.kernel g.unop ≅ Opposite.unop (Limits.cokernel g)

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

Equations

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

@[simp]

theorem CategoryTheory.kernelUnopUnop_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (kernelUnopUnop g).inv = Limits.kernel.lift g.unop (Limits.cokernel.π g).unop ⋯

@[simp]

theorem CategoryTheory.kernelUnopUnop_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (kernelUnopUnop g).hom = (Limits.cokernel.desc g (Limits.kernel.ι g.unop).op ⋯).unop

theorem CategoryTheory.kernel.ι_unop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (Limits.kernel.ι g.unop).op = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Limits.cokernel.π g) (kernelUnopOp g).inv)

theorem CategoryTheory.cokernel.π_unop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (Limits.cokernel.π g.unop).op = CategoryStruct.comp (cokernelUnopOp g).hom (CategoryStruct.comp (Limits.kernel.ι g) (eqToHom ⋯))

noncomputable def CategoryTheory.cokernelUnopUnop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Limits.cokernel g.unop ≅ Opposite.unop (Limits.kernel g)

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

Equations

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

@[simp]

theorem CategoryTheory.cokernelUnopUnop_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (cokernelUnopUnop g).inv = (Limits.kernel.lift g (Limits.cokernel.π g.unop).op ⋯).unop

@[simp]

theorem CategoryTheory.cokernelUnopUnop_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (cokernelUnopUnop g).hom = Limits.cokernel.desc g.unop (Limits.kernel.ι g).unop ⋯

noncomputable def CategoryTheory.imageUnopOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (Limits.image g.unop) ≅ 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.

noncomputable def CategoryTheory.imageOpOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.op (Limits.image f) ≅ 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

noncomputable def CategoryTheory.imageOpUnop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (Limits.image f.op) ≅ Limits.image f

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

Equations

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

noncomputable def CategoryTheory.imageUnopUnop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.unop (Limits.image g) ≅ Limits.image g.unop

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

Equations

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

theorem CategoryTheory.image_ι_op_comp_imageUnopOp_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryStruct.comp (Limits.image.ι g.unop).op (imageUnopOp g).hom = Limits.factorThruImage g

theorem CategoryTheory.imageUnopOp_hom_comp_image_ι {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryStruct.comp (imageUnopOp g).hom (Limits.image.ι g) = (Limits.factorThruImage g.unop).op

theorem CategoryTheory.factorThruImage_comp_imageUnopOp_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryStruct.comp (Limits.factorThruImage g) (imageUnopOp g).inv = (Limits.image.ι g.unop).op

theorem CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryStruct.comp (imageUnopOp g).inv (Limits.factorThruImage g.unop).op = Limits.image.ι g