Documentation

TauCeti.Algebra.MonoidAlgebra.Dual

Duality over a finite group algebra #

For a finite group G and a commutative semiring R, the group algebra R[G] is a symmetric Frobenius algebra. Taking the coefficient at the identity identifies the R[G]-linear dual Hom_{R[G]}(M, R[G]) with the R-linear dual Hom_R(M, R). The action on the latter is the contragredient action: op a sends ψ to the functional m ↦ ψ(a • m).

This file constructs that equivalence explicitly and proves its naturality under precomposition. The range statement is the bridge used to express an Auslander--Reiten transpose through an ordinary base-ring dual. The contragredient action and precomposition need only semiring coefficients and also apply to arbitrary monoids. The range comparison uses commutative semiring coefficients; over a commutative ring, the corresponding quotient comparison is base-ring linear.

Main definitions #

Main results #

References #

source
@[instance_reducible]
noncomputable instance TauCeti.MonoidAlgebra.instModuleDualContragredient {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [SMulCommClass R (MonoidAlgebra R G) M] :
Module (MonoidAlgebra R G)ᵐᵒᵖ (Module.Dual R M)

The contragredient action of a monoid algebra on a base-ring dual.

Equations
  • One or more equations did not get rendered due to their size.
source
instance TauCeti.MonoidAlgebra.instIsScalarTowerDualContragredient {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] :
IsScalarTower R (MonoidAlgebra R G)ᵐᵒᵖ (Module.Dual R M)

The contragredient action restricts to the usual base-ring action on the dual.

source
noncomputable def LinearMap.contragredientDualMap {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [SMulCommClass R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [SMulCommClass R (MonoidAlgebra R G) N] [CompatibleSMul M N R (MonoidAlgebra R G)] (f : M →ₗ[MonoidAlgebra R G] N) :
Module.Dual R N →ₗ[(MonoidAlgebra R G)ᵐᵒᵖ] Module.Dual R M

Precomposition with a monoid-algebra linear map, on base-ring duals equipped with the contragredient action. Scalar compatibility ensures that the map is also base-ring linear.

Equations
Instances For
    source
    @[simp]
    theorem LinearMap.contragredientDualMap_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [SMulCommClass R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [SMulCommClass R (MonoidAlgebra R G) N] [CompatibleSMul M N R (MonoidAlgebra R G)] (f : M →ₗ[MonoidAlgebra R G] N) (ψ : Module.Dual R N) (m : M) :
    (f.contragredientDualMap ψ) m = ψ (f m)

    Contragredient dual precomposition evaluates by applying the original map first.

    source
    theorem LinearMap.contragredientDualMap_eq_dualMap {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) :
    ↑R f.contragredientDualMap = (↑R f).dualMap

    Restricting contragredient dual precomposition to the base ring gives the usual dual map.

    source
    theorem LinearMap.restrictScalars_range_contragredientDualMap {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) :
    Submodule.restrictScalars R f.contragredientDualMap.range = (↑R f).dualMap.range

    The functionals on M that extend along f, described as the range of contragredient dual precomposition and as the range of the base-ring dual map, agree as base-ring submodules.

    source
    noncomputable def LinearMap.quotientRangeContragredientDualMapEquiv {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) :
    (Module.Dual R M ⧸ f.contragredientDualMap.range) ≃ₗ[R] Module.Dual R M ⧸ (↑R f).dualMap.range

    The quotients of Hom_R(M, R) by the range of contragredient dual precomposition and by the range of the base-ring dual map agree as base-ring modules.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem LinearMap.quotientRangeContragredientDualMapEquiv_mk {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) (ψ : Module.Dual R M) :
      f.quotientRangeContragredientDualMapEquiv (Submodule.Quotient.mk ψ) = Submodule.Quotient.mk ψ

      LinearMap.quotientRangeContragredientDualMapEquiv sends the class of a functional to its class.

      source
      @[simp]
      theorem LinearMap.quotientRangeContragredientDualMapEquiv_symm_mk {R : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) (ψ : Module.Dual R M) :
      f.quotientRangeContragredientDualMapEquiv.symm (Submodule.Quotient.mk ψ) = Submodule.Quotient.mk ψ

      The inverse quotient comparison sends the class of a functional to its class.

      source
      noncomputable def TauCeti.MonoidAlgebra.dualLinearEquiv {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [Finite G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] :
      Module.Dual (MonoidAlgebra R G) M ≃ₗ[(MonoidAlgebra R G)ᵐᵒᵖ] Module.Dual R M

      For a finite group, taking the coefficient at the identity identifies the group-algebra linear dual with the base-ring dual carrying the contragredient action.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.MonoidAlgebra.dualLinearEquiv_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [Finite G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] (φ : Module.Dual (MonoidAlgebra R G) M) (m : M) :
        (dualLinearEquiv φ) m = (φ m).coeff 1

        The forward group-algebra duality map takes the coefficient at the identity.

        source
        @[simp]
        theorem TauCeti.MonoidAlgebra.dualLinearEquiv_symm_apply_coeff {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [Finite G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] (ψ : Module.Dual R M) (m : M) (g : G) :
        ((dualLinearEquiv.symm ψ) m).coeff g = ψ (MonoidAlgebra.single g⁻¹ 1 • m)

        The inverse group-algebra duality map records the translates of a functional as its coefficients.

        source
        theorem LinearMap.dualLinearEquiv_comp_lcomp {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [Finite G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] {N : Type u_4} [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) :
        ↑TauCeti.MonoidAlgebra.dualLinearEquiv ∘ₗ lcomp (MonoidAlgebra R G)ᵐᵒᵖ (MonoidAlgebra R G) f = f.contragredientDualMap ∘ₗ ↑TauCeti.MonoidAlgebra.dualLinearEquiv

        Group-algebra precomposition becomes contragredient base-ring precomposition under dualLinearEquiv.

        source
        theorem LinearMap.map_range_lcomp_dualLinearEquiv {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [Finite G] [AddCommMonoid M] [Module (MonoidAlgebra R G) M] [Module R M] [IsScalarTower R (MonoidAlgebra R G) M] {N : Type u_4} [AddCommMonoid N] [Module (MonoidAlgebra R G) N] [Module R N] [IsScalarTower R (MonoidAlgebra R G) N] (f : M →ₗ[MonoidAlgebra R G] N) :
        Submodule.map (↑TauCeti.MonoidAlgebra.dualLinearEquiv) (lcomp (MonoidAlgebra R G)ᵐᵒᵖ (MonoidAlgebra R G) f).range = f.contragredientDualMap.range

        The coefficient-at-one duality carries the range of group-algebra precomposition to the range of contragredient base-ring precomposition.