Documentation

Mathlib.CategoryTheory.Preadditive.Opposite

If `C` is preadditive, `Cᵒᵖ` has a natural preadditive structure. #

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

Preadditive Cᵒᵖ

Equations

CategoryTheory.instPreadditiveOpposite C = { homGroup := fun (X Y : Cᵒᵖ) => (CategoryTheory.opEquiv X Y).addCommGroup, add_comp := ⋯, comp_add := ⋯ }

instance CategoryTheory.moduleEndLeft (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} :

Module (End X)ᵐᵒᵖ (X ⟶ Y)

Equations

CategoryTheory.moduleEndLeft C = Module.mk ⋯ ⋯

@[simp]

theorem CategoryTheory.unop_add (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (f g : X ⟶ Y) :

(f + g).unop = f.unop + g.unop

@[simp]

theorem CategoryTheory.unop_zsmul (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (k : ℤ) (f : X ⟶ Y) :

(k • f).unop = k • f.unop

@[simp]

theorem CategoryTheory.unop_neg (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (f : X ⟶ Y) :

(-f).unop = -f.unop

@[simp]

theorem CategoryTheory.op_add (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) :

(f + g).op = f.op + g.op

@[simp]

theorem CategoryTheory.op_zsmul (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (k : ℤ) (f : X ⟶ Y) :

(k • f).op = k • f.op

@[simp]

theorem CategoryTheory.op_neg (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) :

(-f).op = -f.op

def CategoryTheory.unopHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (X Y : Cᵒᵖ) :

(X ⟶ Y) →+ (Opposite.unop Y ⟶ Opposite.unop X)

unop induces morphisms of monoids on hom groups of a preadditive category

Equations

CategoryTheory.unopHom X Y = AddMonoidHom.mk' (fun (f : X ⟶ Y) => f.unop) ⋯

Instances For

@[simp]

theorem CategoryTheory.unopHom_apply {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (X Y : Cᵒᵖ) (f : X ⟶ Y) :

(unopHom X Y) f = f.unop

@[simp]

theorem CategoryTheory.unop_sum {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (X Y : Cᵒᵖ) {ι : Type u_2} (s : Finset ι) (f : ι → (X ⟶ Y)) :

(s.sum f).unop = ∑ i ∈ s, (f i).unop

def CategoryTheory.opHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (X Y : C) :

(X ⟶ Y) →+ (Opposite.op Y ⟶ Opposite.op X)

op induces morphisms of monoids on hom groups of a preadditive category

Equations

CategoryTheory.opHom X Y = AddMonoidHom.mk' (fun (f : X ⟶ Y) => f.op) ⋯

Instances For

@[simp]

theorem CategoryTheory.opHom_apply {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (X Y : C) (f : X ⟶ Y) :

(opHom X Y) f = f.op

@[simp]

theorem CategoryTheory.op_sum {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (X Y : C) {ι : Type u_2} (s : Finset ι) (f : ι → (X ⟶ Y)) :

(s.sum f).op = ∑ i ∈ s, (f i).op

instance CategoryTheory.Functor.op_additive {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {D : Type u_2} [Category.{u_4, u_2} D] [Preadditive D] (F : Functor C D) [F.Additive] :

instance CategoryTheory.Functor.rightOp_additive {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {D : Type u_2} [Category.{u_4, u_2} D] [Preadditive D] (F : Functor Cᵒᵖ D) [F.Additive] :

F.rightOp.Additive

instance CategoryTheory.Functor.leftOp_additive {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {D : Type u_2} [Category.{u_4, u_2} D] [Preadditive D] (F : Functor C Dᵒᵖ) [F.Additive] :

F.leftOp.Additive

instance CategoryTheory.Functor.unop_additive {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {D : Type u_2} [Category.{u_4, u_2} D] [Preadditive D] (F : Functor Cᵒᵖ Dᵒᵖ) [F.Additive] :

F.unop.Additive