Documentation

Mathlib.CategoryTheory.Preadditive.Opposite

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

source
@[instance_reducible]
instance CategoryTheory.instPreadditiveOpposite (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] :
Preadditive Cᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance CategoryTheory.moduleEndLeft (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} :
Module (End X)ᵐᵒᵖ (X ⟶ Y)
Equations
source
@[simp]
theorem CategoryTheory.unop_add (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (f g : X ⟶ Y) :
(f + g).unop = f.unop + g.unop
source
@[simp]
theorem CategoryTheory.unop_sub (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (f g : X ⟶ Y) :
(f - g).unop = f.unop - g.unop
source
@[simp]
theorem CategoryTheory.unop_zsmul (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (k : ℤ) (f : X ⟶ Y) :
(k • f).unop = k • f.unop
source
@[simp]
theorem CategoryTheory.unop_neg (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : Cᵒᵖ} (f : X ⟶ Y) :
(-f).unop = -f.unop
source
@[simp]
theorem CategoryTheory.op_add (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) :
(f + g).op = f.op + g.op
source
@[simp]
theorem CategoryTheory.op_sub (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) :
(f - g).op = f.op - g.op
source
@[simp]
theorem CategoryTheory.op_zsmul (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (k : ℤ) (f : X ⟶ Y) :
(k • f).op = k • f.op
source
@[simp]
theorem CategoryTheory.op_neg (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) :
(-f).op = -f.op
source
def CategoryTheory.unopHom {C : Type u_1} [Category.{v_1, 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
Instances For
    source
    @[simp]
    theorem CategoryTheory.unopHom_apply {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (X Y : Cᵒᵖ) (f : X ⟶ Y) :
    (unopHom X Y) f = f.unop
    source
    @[simp]
    theorem CategoryTheory.unop_sum {C : Type u_1} [Category.{v_1, 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
    source
    def CategoryTheory.opHom {C : Type u_1} [Category.{v_1, 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
    Instances For
      source
      @[simp]
      theorem CategoryTheory.opHom_apply {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (X Y : C) (f : X ⟶ Y) :
      (opHom X Y) f = f.op
      source
      @[simp]
      theorem CategoryTheory.op_sum {C : Type u_1} [Category.{v_1, 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
      source
      def CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (G : C) :
      (G ⟶ G) ≃ₗ[(End G)ᵐᵒᵖ] (End G)ᵐᵒᵖ

      G ⟶ G and (End G)ᵐᵒᵖ are isomorphic as (End G)ᵐᵒᵖ-modules.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (G : C) (f : G ⟶ G) :
        (homSelfLinearEquivEndMulOpposite G) f = { unop' := { asHom := f } }
        source
        @[simp]
        theorem CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (G : C) (x✝ : (End G)ᵐᵒᵖ) :
        (homSelfLinearEquivEndMulOpposite G).symm x✝ = match x✝ with | { unop' := f } => f.asHom
        source
        instance CategoryTheory.Functor.op_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {D : Type u_2} [Category.{v_2, u_2} D] [Preadditive D] (F : Functor C D) [F.Additive] :
        F.op.Additive
        source
        instance CategoryTheory.Functor.rightOp_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {D : Type u_2} [Category.{v_2, u_2} D] [Preadditive D] (F : Functor Cᵒᵖ D) [F.Additive] :
        F.rightOp.Additive
        source
        instance CategoryTheory.Functor.leftOp_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {D : Type u_2} [Category.{v_2, u_2} D] [Preadditive D] (F : Functor C Dᵒᵖ) [F.Additive] :
        F.leftOp.Additive
        source
        instance CategoryTheory.Functor.unop_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {D : Type u_2} [Category.{v_2, u_2} D] [Preadditive D] (F : Functor Cᵒᵖ Dᵒᵖ) [F.Additive] :
        F.unop.Additive