The dual of a right module as a left module

For a right module N over a semiring A whose right action commutes with a base commutative semiring k, the duality D = Hom_k(-, k) turns N into a left A-module: a scalar a acts on a functional φ by precomposition with multiplication by a, (a • φ) x = φ (x * a). Precomposition reverses composition, which is exactly what exchanges the two sides.

This file records that action as the ring homomorphism TauCeti.dualRightAction.

On the other side, a semiring A with a k-module structure commuting with left multiplication acts on the right of the dual of its left regular module by (ψ · c) b = ψ (c * b), which Mathlib writes as the domain action DomMulAct.mk c • ψ. A k-linear map A → Module.Dual k A that is right A-linear for this action is determined by its value at 1; this is TauCeti.dualLinearMap_apply_apply.

Main definitions

• TauCeti.dualRightAction: the left action of A on the k-dual of a right A-module, as a ring homomorphism into the k-linear endomorphisms of the dual.

Main results

• TauCeti.dualLinearMap_apply_apply: a right A-linear map from A to its dual is determined by its value at 1.

Implementation notes

The action is deliberately not installed as a Module A (Module.Dual k N) instance: the underlying type of Module.Dual k N is a type of linear maps, which already carries the codomain-scaling Module instances of Mathlib.Algebra.Module.LinearMap.Defs, and a second Module structure matching every dual would make instance search on those types depend on an undetermined right-module structure. A consumer that wants the left module structure on one particular dual builds it with Module.compHom, which pins the right-module structure being dualized.

def TauCeti.dualRightAction (k : Type u) (N : Type w) {A : Type v} [CommSemiring k] [Semiring A] [AddCommMonoid N] [Module k N] [Module Aᵐᵒᵖ N] [SMulCommClass Aᵐᵒᵖ k N] : A →+* Module.End k (Module.Dual k N)

The duality D = Hom_k(-, k) turns a right A-module N into a left A-module: the scalar a sends a functional φ to x ↦ φ (x * a). This records that action as a ring homomorphism from A to the k-linear endomorphisms of Module.Dual k N.

Precomposition reverses composition, which is exactly what makes a right action on N into a left action on its dual; the hypothesis SMulCommClass Aᵐᵒᵖ k N is what makes multiplication by a a k-linear endomorphism of N in the first place.

Equations

• TauCeti.dualRightAction k N = { toFun := fun (a : A) => LinearMap.dualMap ((Module.toModuleEnd k N) (MulOpposite.op a)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.dualRightAction_apply_apply (k : Type u) (N : Type w) {A : Type v} [CommSemiring k] [Semiring A] [AddCommMonoid N] [Module k N] [Module Aᵐᵒᵖ N] [SMulCommClass Aᵐᵒᵖ k N] (a : A) (φ : Module.Dual k N) (x : N) : (((dualRightAction k N) a) φ) x = φ (MulOpposite.op a • x)

theorem TauCeti.dualLinearMap_apply_apply {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Module k A] [SMulCommClass k A A] {e : A →ₗ[k] Module.Dual k A} (he : ∀ (a c : A), e (a * c) = DomMulAct.mk c • e a) (a b : A) : (e a) b = (e 1) (a * b)

A k-linear map from A to its dual that is right A-linear, for the action DomMulAct.mk c • ψ = ψ (c * ·) on the dual, is determined by its value at 1.