Evaluation after scalar extension

This file defines the canonical pairing between the scalar extensions of a module and its linear dual. It sends an R-linear functional extended to A to the corresponding A-linear functional on the scalar extension of its domain. For a finite projective module, this map is an equivalence.

Main declarations

• TauCeti.Module.Dual.baseChangeEvaluation: the canonical scalar-extended evaluation map.
• TauCeti.Module.Dual.baseChangeEvaluation_one_tmul: evaluation at a scalar-extended functional with coefficient one is its base change.
• TauCeti.Module.Dual.baseChangeEvaluation_tmul: its value on two pure tensors.
• Module.Dual.baseChangeEvaluation_one_tmul_baseChange: naturality of evaluation with respect to a base-changed linear map.
• TauCeti.Module.Dual.baseChangeEvaluationEquiv: scalar extension commutes with the dual of a finite projective module.
• TauCeti.Module.Dual.baseChange_coord: base-changed dual basis elements recover the coordinates in the base-changed basis.
• TauCeti.Module.Dual.eq_of_baseChange_eq: base changes of all dual elements jointly separate vectors when the original module is free.

References

The finite-projective equivalence is assembled from Mathlib's dualTensorHomEquiv and LinearMap.liftBaseChangeEquiv.

def TauCeti.Module.Dual.baseChangeEvaluation {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] : TensorProduct R A (Module.Dual R M) →ₗ[A] Module.Dual A (TensorProduct R A M)

The canonical pairing of scalar extensions, as the map sending a scalar-extended R-linear functional to an A-linear functional on the scalar extension of its domain.

This map needs no finiteness hypothesis; for finite projective M it is an equivalence, see baseChangeEvaluationEquiv.

Equations

• TauCeti.Module.Dual.baseChangeEvaluation = LinearMap.liftBaseChange A (Module.Dual.baseChange A)

theorem TauCeti.Module.Dual.baseChangeEvaluation_one_tmul {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] (φ : Module.Dual R M) : baseChangeEvaluation (1 ⊗ₜ[R] φ) = (Module.Dual.baseChange A) φ

Evaluating at the pure tensor 1 ⊗ φ is the base change of φ.

@[simp]

theorem TauCeti.Module.Dual.baseChangeEvaluation_tmul {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] (a b : A) (φ : Module.Dual R M) (m : M) : (baseChangeEvaluation (a ⊗ₜ[R] φ)) (b ⊗ₜ[R] m) = a * b * (algebraMap R A) (φ m)

On pure tensors, scalar-extended evaluation is ⟨a ⊗ φ, b ⊗ m⟩ = a * b * algebraMap R A (φ m).

@[simp]

theorem Module.Dual.baseChangeEvaluation_one_tmul_baseChange {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] {N : Type u_1} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (φ : Dual R N) (t : TensorProduct R A M) : (TauCeti.Module.Dual.baseChangeEvaluation (1 ⊗ₜ[R] φ)) ((LinearMap.baseChange A f) t) = (TauCeti.Module.Dual.baseChangeEvaluation (1 ⊗ₜ[R] (φ ∘ₗ f))) t

Evaluation against a base-changed functional is natural with respect to the base change of a linear map.

noncomputable def TauCeti.Module.Dual.baseChangeEvaluationEquiv {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] [Module.Finite R M] [Module.Projective R M] : TensorProduct R A (Module.Dual R M) ≃ₗ[A] Module.Dual A (TensorProduct R A M)

Scalar extension commutes with the linear dual of a finite projective module.

Equations

• TauCeti.Module.Dual.baseChangeEvaluationEquiv = LinearEquiv.ofBijective TauCeti.Module.Dual.baseChangeEvaluation ⋯

@[simp]

theorem TauCeti.Module.Dual.baseChangeEvaluationEquiv_apply {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] [Module.Finite R M] [Module.Projective R M] (z : TensorProduct R A (Module.Dual R M)) : baseChangeEvaluationEquiv z = baseChangeEvaluation z

The finite-projective equivalence is the canonical scalar-extended evaluation map.

@[simp]

theorem TauCeti.Module.Dual.baseChange_coord {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] {ι : Type u_1} (b : Module.Basis ι R M) (i : ι) (z : TensorProduct R A M) : ((IsBaseChange.basis b ⋯).repr z) i = ((Module.Dual.baseChange A) (b.coord i)) z

A coordinate in a base-changed basis is evaluation against the base change of the corresponding element of the dual basis.

theorem TauCeti.Module.Dual.eq_of_baseChange_eq {R : Type u} {M : Type w} {A : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] [Module.Free R M] {x y : TensorProduct R A M} (h : ∀ (φ : Module.Dual R M), ((Module.Dual.baseChange A) φ) x = ((Module.Dual.baseChange A) φ) y) : x = y

If M is free, the base changes of its R-linear functionals jointly separate vectors in A ⊗[R] M.