Magnitude conjecture

MagnitudeConjecture.CategoryTheory.OppositeLinear

Linear structure on an opposite category #

The opposite of a k-linear category is k-linear, with scalar action transported through morphism reversal.

source
@[instance_reducible]
instance MagnitudeConjecture.CoveringHom.oppositeLinear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] :
CategoryTheory.Linear k Cᵒᵖ

The opposite of a linear category carries the same scalar action on Hom spaces.

source
def MagnitudeConjecture.CoveringHom.oppositeHomLinearEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : Cᵒᵖ) :
(X ⟶ Y) ≃ₗ[k] Opposite.unop Y ⟶ Opposite.unop X

Reversing an opposite-category morphism is a linear equivalence.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.CoveringHom.opposite_unop_smul {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : Cᵒᵖ} (r : k) (f : X ⟶ Y) :
    (r • f).unop = r • f.unop
    source
    @[simp]
    theorem MagnitudeConjecture.CoveringHom.opposite_op_smul {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} (r : k) (f : X ⟶ Y) :
    (r • f).op = r • f.op
    source
    instance MagnitudeConjecture.CoveringHom.functorOpLinear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear k F] :
    CategoryTheory.Functor.Linear k F.op

    The opposite of a linear functor is linear for the transported linear structures on the opposite categories.

    source
    instance MagnitudeConjecture.CoveringHom.functorRightOpLinear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Functor.Linear k F] :
    CategoryTheory.Functor.Linear k F.rightOp

    Turning a functor out of an opposite category around on both sides preserves linearity.