Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ContragredientLinear

Linearity of finite-dimensional contragredient duality #

The vendored contragredient equivalence is packaged additively. Its action on morphisms is also linear over the central coefficient field. Recording that fact lets a linear Morita equivalence be transported to the opposite module categories without changing scalars.

source
@[instance_reducible]
def QuotientSubmoduleEquidistribution.Contragredient.moduleCategoryOppositeLinear (k R : Type u) [Field k] [Ring R] [Algebra k R] :
CategoryTheory.Linear k (FGModuleCat R)ᵒᵖ
Instances For
    source
    @[instance_reducible]
    def QuotientSubmoduleEquidistribution.Contragredient.oppositeModuleCategoryOppositeLinear (k R : Type u) [Field k] [Ring R] [Algebra k R] :
    CategoryTheory.Linear k (FGModuleCat Rᵐᵒᵖ)ᵒᵖ
    Instances For
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.dualFunctor_additive (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      (dualFunctor k R).Additive
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.dualFunctor_linear (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      CategoryTheory.Functor.Linear k (dualFunctor k R)
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.reverseDualFunctor_additive (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      (reverseDualFunctor k R).Additive
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.reverseDualFunctor_linear (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      CategoryTheory.Functor.Linear k (reverseDualFunctor k R)
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence_functor_additive (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      (dualityEquivalence k R).functor.Additive
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence_functor_linear (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      CategoryTheory.Functor.Linear k (dualityEquivalence k R).functor
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence_inverse_additive (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      (dualityEquivalence k R).inverse.Additive
      source
      instance QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence_inverse_linear (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] :
      CategoryTheory.Functor.Linear k (dualityEquivalence k R).inverse