Magnitude conjecture

QuotientSubmoduleEquidistribution.RepresentationTheory.Contragredient

The contragredient action on a vector-space dual #

This is the concrete algebraic core used to instantiate AlignedBiduality with D = Hom_k(-, k).

source
def QuotientSubmoduleEquidistribution.Contragredient.dualActionHom (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] :
Rᵐᵒᵖ →+* Module.End K (Module.Dual K X)

The action of Rᵐᵒᵖ on the K-linear dual, encoded as a ring homomorphism into the K-linear endomorphism ring.

Instances For
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.Contragredient.dualActionHom_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] (r : Rᵐᵒᵖ) (f : Module.Dual K X) (x : X) :
    (((dualActionHom K R X) r) f) x = f (MulOpposite.unop r • x)
    source
    @[reducible]
    def QuotientSubmoduleEquidistribution.Contragredient.dualModule (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 X)

    The resulting left Rᵐᵒᵖ-module structure on the dual.

    Instances For
      source
      theorem QuotientSubmoduleEquidistribution.Contragredient.dualIsScalarTower (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] :
      IsScalarTower K Rᵐᵒᵖ (Module.Dual K X)

      The contragredient action restricts to the original K-vector-space structure.

      source
      theorem QuotientSubmoduleEquidistribution.Contragredient.dual_finite_of_finiteDimensional (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] :
      Module.Finite Rᵐᵒᵖ (Module.Dual K X)

      A finite-dimensional vector-space dual is finitely generated over the opposite algebra.

      source
      def QuotientSubmoduleEquidistribution.Contragredient.dualMap {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] {Y : Type u_1} [AddCommGroup Y] [Module K Y] [Module R Y] [IsScalarTower K R Y] (g : X →ₗ[R] Y) :
      Module.Dual K Y →ₗ[Rᵐᵒᵖ] Module.Dual K X

      The ordinary K-linear dual map is linear for the contragredient Rᵐᵒᵖ-actions.

      Instances For
        source
        @[simp]
        theorem QuotientSubmoduleEquidistribution.Contragredient.dualMap_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] {Y : Type u_1} [AddCommGroup Y] [Module K Y] [Module R Y] [IsScalarTower K R Y] (g : X →ₗ[R] Y) (f : Module.Dual K Y) (x : X) :
        ((dualMap g) f) x = f (g x)
        source
        def QuotientSubmoduleEquidistribution.Contragredient.dualFGObj (K : Type uK) (R : Type uR) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) :
        FGModuleCat Rᵐᵒᵖ

        On a finite-dimensional algebra, the contragredient dual of every finitely generated module is again a finitely generated module over the opposite algebra.

        Instances For