Magnitude conjecture

QuotientSubmoduleEquidistribution.RepresentationTheory.Biduality

Linearity of finite-dimensional bidual evaluation #

This verifies the load-bearing algebraic fact needed to turn the concrete contragredient functor into an equivalence: after identifying Rᵐᵒᵖᵐᵒᵖ with R, evaluation into the double dual is R-linear.

source
@[reducible]
def QuotientSubmoduleEquidistribution.Contragredient.bidualModule (K : Type uK) (R : Type uR) (X : Type uX) [Field K] [Ring R] [Algebra K R] [AddCommGroup X] [Module K X] [Module R X] [IsScalarTower K R X] :
Module R (Module.Dual K (Module.Dual K X))

Regard the double contragredient dual as an R-module through the canonical ring equivalence R ≃+* Rᵐᵒᵖᵐᵒᵖ.

Instances For
    source
    def QuotientSubmoduleEquidistribution.Contragredient.bidualEval (K : Type uK) (R : Type uR) (X : Type uX) [Field K] [Ring R] [Algebra K R] [AddCommGroup X] [Module K X] [Module R X] [IsScalarTower K R X] :
    X →ₗ[R] Module.Dual K (Module.Dual K X)

    Evaluation into the double contragredient dual is R-linear.

    Instances For
      source
      @[simp]
      theorem QuotientSubmoduleEquidistribution.Contragredient.bidualEval_apply (K : Type uK) (R : Type uR) (X : Type uX) [Field K] [Ring R] [Algebra K R] [AddCommGroup X] [Module K X] [Module R X] [IsScalarTower K R X] (x : X) (f : Module.Dual K X) :
      ((bidualEval K R X) x) f = f x
      source
      noncomputable def QuotientSubmoduleEquidistribution.Contragredient.bidualLinearEquiv (K : Type uK) (R : Type uR) (X : Type uX) [Field K] [Ring R] [Algebra K R] [AddCommGroup X] [Module K X] [Module R X] [IsScalarTower K R X] [FiniteDimensional K X] :
      X ≃ₗ[R] Module.Dual K (Module.Dual K X)

      Finite-dimensional biduality, now bundled over the algebra rather than only over the base field.

      Instances For