Scalar extension of linear Hom spaces

The canonical map from A ⊗[R] Hom_R(M,N) to Hom_A(A ⊗[R] M, A ⊗[R] N) sends a ⊗ f to a • f.baseChange A. It is an equivalence when M is finite projective; no finiteness condition is needed on N or on the commutative value algebra A. This comparison allows a scalar-extended Hom representation to act on scalar-extended vectors.

The equivalence uses Mathlib's lTensorHomEquivHomLTensor and LinearMap.liftBaseChangeEquiv, following the construction of TauCeti.Module.Dual.baseChangeEvaluationEquiv.

noncomputable def LinearMap.baseChangeTensorHom (R : Type u) (A : Type v) (M : Type w) (N : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct R A (M →ₗ[R] N) →ₗ[A] TensorProduct R A M →ₗ[A] TensorProduct R A N

The canonical scalar-extension map on linear Hom spaces.

Equations

• LinearMap.baseChangeTensorHom R A M N = LinearMap.liftBaseChange A (LinearMap.baseChangeHom R A M N)

@[simp]

theorem LinearMap.baseChangeTensorHom_tmul {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a : A) (f : M →ₗ[R] N) : (baseChangeTensorHom R A M N) (a ⊗ₜ[R] f) = a • baseChange A f

A pure tensor acts by the scalar multiple of the base-changed linear map.

@[simp]

theorem LinearMap.baseChangeTensorHom_distribBaseChange_symm_tmul {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (ξ : TensorProduct R A (Module.Dual R M)) (η : TensorProduct R A N) (z : TensorProduct R A M) : ((baseChangeTensorHom R A M N) ((baseChange A (dualTensorHom R M N)) ((TensorProduct.AlgebraTensorModule.distribBaseChange R A (Module.Dual R M) N).symm (ξ ⊗ₜ[A] η)))) z = (TauCeti.Module.Dual.baseChangeEvaluation ξ) z • η

Scalar extension of a rank-one map evaluates by the scalar-extended dual pairing. The tensor comparison assembles the scalar-extended functional and target vector.

noncomputable def LinearMap.baseChangeTensorHomEquiv {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] : TensorProduct R A (M →ₗ[R] N) ≃ₗ[A] TensorProduct R A M →ₗ[A] TensorProduct R A N

Scalar extension commutes with linear Hom out of a finite projective module.

Equations

• LinearMap.baseChangeTensorHomEquiv = LinearEquiv.ofBijective (LinearMap.baseChangeTensorHom R A M N) ⋯

@[simp]

theorem LinearMap.baseChangeTensorHomEquiv_apply {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] (z : TensorProduct R A (M →ₗ[R] N)) : baseChangeTensorHomEquiv z = (baseChangeTensorHom R A M N) z

The Hom comparison equivalence is the canonical scalar-extension map.

@[simp]

theorem LinearMap.baseChangeTensorHomEquiv_symm_baseChange {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] (f : M →ₗ[R] N) : baseChangeTensorHomEquiv.symm (baseChange A f) = 1 ⊗ₜ[R] f

The inverse Hom comparison sends a base-changed map to the corresponding tensor with scalar coefficient one.