category_theory.abelian.opposite

@[protected, instance]

def category_theory.opposite.abelian (C : Type u_1) [category_theory.category C] [category_theory.abelian C] :

Equations

category_theory.opposite.abelian C = category_theory.abelian.mk

@[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

category_theory.kernel_op_unop f = {hom := (category_theory.limits.kernel.lift f.op (category_theory.limits.cokernel.π f).op _).unop, inv := category_theory.limits.cokernel.desc f (category_theory.limits.kernel.ι f.op).unop _, hom_inv_id' := _, inv_hom_id' := _}

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

category_theory.cokernel_op_unop f = {hom := category_theory.limits.kernel.lift f (category_theory.limits.cokernel.π f.op).unop _, inv := (category_theory.limits.cokernel.desc f.op (category_theory.limits.kernel.ι f).op _).unop, hom_inv_id' := _, inv_hom_id' := _}

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

category_theory.kernel_unop_op g = (category_theory.cokernel_op_unop g.unop).op

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

category_theory.cokernel_unop_op g = (category_theory.kernel_op_unop g.unop).op

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

category_theory.kernel_op_op f = (category_theory.kernel_op_unop f).op.symm

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

category_theory.cokernel_op_op f = (category_theory.cokernel_op_unop f).op.symm

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

category_theory.kernel_unop_unop g = (category_theory.kernel_unop_op g).unop.symm

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

category_theory.cokernel_unop_unop g = (category_theory.cokernel_unop_op g).unop.symm

source

noncomputable def category_theory.image_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.image g.unop) ≅ category_theory.limits.image g

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

Equations

category_theory.image_unop_op g = (category_theory.abelian.image_iso_image g.unop).op ≪≫ (category_theory.cokernel_op_op (category_theory.limits.cokernel.π g.unop)).symm ≪≫ category_theory.limits.cokernel_iso_of_eq _ ≪≫ category_theory.limits.cokernel_epi_comp (category_theory.cokernel_unop_op g).hom (category_theory.limits.kernel.ι g ≫ category_theory.eq_to_hom category_theory.image_unop_op._proof_10) ≪≫ category_theory.limits.cokernel_comp_is_iso (category_theory.limits.kernel.ι g) (category_theory.eq_to_hom category_theory.image_unop_op._proof_10) ≪≫ category_theory.abelian.coimage_iso_image' g

source

noncomputable def category_theory.image_op_op {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :

opposite.op (category_theory.limits.image f) ≅ category_theory.limits.image f.op

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

Equations

category_theory.image_op_op f = category_theory.image_unop_op f.op

source

noncomputable def category_theory.image_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.image f.op) ≅ category_theory.limits.image f

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

Equations

category_theory.image_op_unop f = (category_theory.image_unop_op f.op).unop

source

noncomputable def category_theory.image_unop_unop {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :

opposite.unop (category_theory.limits.image g) ≅ category_theory.limits.image g.unop

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

Equations

category_theory.image_unop_unop g = (category_theory.image_unop_op g).unop

source

theorem category_theory.image_ι_op_comp_image_unop_op_hom {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :

(category_theory.limits.image.ι g.unop).op ≫ (category_theory.image_unop_op g).hom = category_theory.limits.factor_thru_image g

source

theorem category_theory.image_unop_op_hom_comp_image_ι {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :

(category_theory.image_unop_op g).hom ≫ category_theory.limits.image.ι g = (category_theory.limits.factor_thru_image g.unop).op

source

theorem category_theory.factor_thru_image_comp_image_unop_op_inv {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :

category_theory.limits.factor_thru_image g ≫ (category_theory.image_unop_op g).inv = (category_theory.limits.image.ι g.unop).op

source

theorem category_theory.image_unop_op_inv_comp_op_factor_thru_image {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) :

(category_theory.image_unop_op g).inv ≫ (category_theory.limits.factor_thru_image g.unop).op = category_theory.limits.image.ι g

mathlib3 documentation

The opposite of an abelian category is abelian. #