Scalar extensions of modules

A flat module embeds in its scalar extension along a faithful semiring algebra. The map m ↦ 1 ⊗ m identifies it with the submodule of unit pure tensors, which is free whenever the original module is free. For a module with a basis, this submodule is the span over the original semiring of the base-changed basis.

The canonical identification (E ⊗[K] L) ⊗[L] V ≃ E ⊗[K] V is linear over E, although L acts on the right component of the scalar-extended algebra. This identification compares scalar extension of an underlying K-module with scalar extension of an L-module, and is used when a construction over L/K is transported along K → E.

The construction uses Mathlib's Algebra.TensorProduct.commRight, TensorProduct.AlgebraTensorModule.cancelBaseChange, and TensorProduct.comm.

With B acting on the left factor instead, TensorProduct.cancelBaseChangeLeft is the R-linear identification (B ⊗[R] P) ⊗[B] N ≃ P ⊗[R] N for an R-module P. Under it, tensoring a B-linear map over B with the B-module B ⊗[R] P becomes tensoring the underlying R-linear map with P (TensorProduct.cancelBaseChangeLeft_lTensor), so the two are injective together (LinearMap.injective_lTensor_iff_injective_lTensor_restrictScalars). When P is an R-algebra, the first is extension of scalars along B → B ⊗[R] P; for P = κ(p), this compares base change to the fibre ring B ⊗[R] κ(p) with base change to κ(p).

Main declarations

• Module.Basis.range_mk_one_eq_span: the unit pure tensors are the span over the original semiring of a base-changed basis.
• TensorProduct.unitTmulEquiv: a flat module is equivalent to its unit-tensor image under a faithful scalar extension.
• TensorProduct.free_range_mk_one: the unit-tensor image of a free module is free.
• TensorProduct.cancelBaseChangeRight and TensorProduct.cancelBaseChangeLeft: cancelling a scalar-extended algebra identifies two iterated scalar extensions.
• TensorProduct.exists_rTensor_section, TensorProduct.exists_smul_linearMap_eq_self: after tensoring over R with a division ring Q that is an R-algebra, a surjection has an R-linear section, and after tensoring with any R-algebra Q, multiplication by an element whose image in Q is a unit has an R-linear right inverse.
• TensorProduct.AlgebraTensorModule.cancelBaseChangeTensor: tensoring with two scalar-extended modules cancels both copies of the extended coefficient ring.

def TensorProduct.cancelBaseChangeRight (K : Type u_1) (L : Type u_2) (E : Type u_3) (V : Type u_4) [CommSemiring K] [CommSemiring L] [CommSemiring E] [Algebra K L] [Algebra K E] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] : TensorProduct L (TensorProduct K E L) V ≃ₗ[E] TensorProduct K E V

Cancelling the scalar-extended algebra identifies extension of an L-module with extension of its underlying K-module. The map sends (e ⊗ l) ⊗ v to e ⊗ (l • v).

@[simp]

theorem TensorProduct.cancelBaseChangeRight_tmul (K : Type u_1) (L : Type u_2) (E : Type u_3) (V : Type u_4) [CommSemiring K] [CommSemiring L] [CommSemiring E] [Algebra K L] [Algebra K E] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (e : E) (l : L) (v : V) : (cancelBaseChangeRight K L E V) (e ⊗ₜ[K] l ⊗ₜ[L] v) = e ⊗ₜ[K] (l • v)

The cancellation equivalence acts by the L-scalar on the vector component.

@[simp]

theorem TensorProduct.cancelBaseChangeRight_symm_tmul (K : Type u_1) (L : Type u_2) (E : Type u_3) (V : Type u_4) [CommSemiring K] [CommSemiring L] [CommSemiring E] [Algebra K L] [Algebra K E] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (e : E) (v : V) : (cancelBaseChangeRight K L E V).symm (e ⊗ₜ[K] v) = e ⊗ₜ[K] 1 ⊗ₜ[L] v

The inverse cancellation inserts the unit of L in the scalar-extended algebra.

def TensorProduct.cancelBaseChangeLeft (R : Type u_1) (B : Type u_2) (P : Type u_3) [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] (N : Type u_4) [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] : TensorProduct B (TensorProduct R B P) N ≃ₗ[R] TensorProduct R P N

Cancelling B on the left identifies the tensor product over B of the B-module B ⊗[R] P with a B-module N with the tensor product over R of P and the underlying R-module of N. The map sends (b ⊗ p) ⊗ n to p ⊗ (b • n).

@[simp]

theorem TensorProduct.cancelBaseChangeLeft_tmul (R : Type u_1) (B : Type u_2) (P : Type u_3) [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] (b : B) (p : P) (n : N) : (cancelBaseChangeLeft R B P N) (b ⊗ₜ[R] p ⊗ₜ[B] n) = p ⊗ₜ[R] (b • n)

The left cancellation equivalence moves the B-scalar onto the module component.

@[simp]

theorem TensorProduct.cancelBaseChangeLeft_symm_tmul (R : Type u_1) (B : Type u_2) (P : Type u_3) [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] (p : P) (n : N) : (cancelBaseChangeLeft R B P N).symm (p ⊗ₜ[R] n) = 1 ⊗ₜ[R] p ⊗ₜ[B] n

The inverse left cancellation inserts the unit of B in the left factor of B ⊗[R] P.

theorem TensorProduct.cancelBaseChangeLeft_lTensor {R : Type u_1} {B : Type u_2} {P : Type u_3} [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} {N' : Type u_5} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] [AddCommMonoid N'] [Module R N'] [Module B N'] [IsScalarTower R B N'] (f : N →ₗ[B] N') (z : TensorProduct B (TensorProduct R B P) N) : (cancelBaseChangeLeft R B P N') ((LinearMap.lTensor (TensorProduct R B P) f) z) = (LinearMap.lTensor P (↑R f)) ((cancelBaseChangeLeft R B P N) z)

Through cancelBaseChangeLeft, tensoring a B-linear map f over B with B ⊗[R] P is tensoring the underlying R-linear map of f with P.

def TensorProduct.AlgebraTensorModule.cancelBaseChangeTensor (R : Type u_7) (B : Type u_8) (N : Type u_9) (P : Type u_10) (Q : Type u_11) [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] : TensorProduct B N (TensorProduct B (TensorProduct R B P) (TensorProduct R B Q)) ≃ₗ[B] TensorProduct R N (TensorProduct R P Q)

Tensoring a module with two scalar-extended modules cancels both extended coefficient rings. The map sends n ⊗ ((b ⊗ p) ⊗ (c ⊗ q)) to (b * c) • n ⊗ (p ⊗ q).

@[simp]

theorem TensorProduct.AlgebraTensorModule.cancelBaseChangeTensor_tmul {R : Type u_1} {B : Type u_2} {P : Type u_3} [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (n : N) (b c : B) (p : P) (q : Q) : (cancelBaseChangeTensor R B N P Q) (n ⊗ₜ[B] (b ⊗ₜ[R] p ⊗ₜ[B] (c ⊗ₜ[R] q))) = ((b * c) • n) ⊗ₜ[R] (p ⊗ₜ[R] q)

Cancellation moves both scalar coefficients onto the unextended module factor.

@[simp]

theorem TensorProduct.AlgebraTensorModule.cancelBaseChangeTensor_symm_tmul {R : Type u_1} {B : Type u_2} {P : Type u_3} [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (n : N) (p : P) (q : Q) : (cancelBaseChangeTensor R B N P Q).symm (n ⊗ₜ[R] (p ⊗ₜ[R] q)) = n ⊗ₜ[B] (1 ⊗ₜ[R] p ⊗ₜ[B] (1 ⊗ₜ[R] q))

The inverse cancellation inserts the unit scalar into each extended module factor.

@[simp]

theorem TensorProduct.AlgebraTensorModule.cancelBaseChangeTensor_tmul_distribBaseChange {R : Type u_1} {B : Type u_2} {P : Type u_3} [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (n : N) (b : B) (z : TensorProduct R P Q) : (cancelBaseChangeTensor R B N P Q) (n ⊗ₜ[B] (distribBaseChange R B P Q) (b ⊗ₜ[R] z)) = (b • n) ⊗ₜ[R] z

Cancellation after distributing scalar extension recovers the original tensor factor.

theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_rTensor {R : Type u_1} {B : Type u_2} {P : Type u_3} [CommSemiring R] [CommSemiring B] [Algebra R B] [AddCommMonoid P] [Module R P] {N : Type u_4} {N' : Type u_5} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] [AddCommMonoid N'] [Module R N'] [Module B N'] [IsScalarTower R B N'] (f : N →ₗ[B] N') (z : TensorProduct B N (TensorProduct R B P)) : (cancelBaseChange R B B N' P) ((LinearMap.rTensor (TensorProduct R B P) f) z) = (LinearMap.rTensor P (↑R f)) ((cancelBaseChange R B B N P) z)

Tensor cancellation commutes with tensoring the underlying linear map on the right.

theorem LinearMap.injective_lTensor_iff_injective_lTensor_restrictScalars {R : Type u_1} {B : Type u_2} [CommSemiring R] [CommSemiring B] [Algebra R B] (P : Type u_3) [AddCommMonoid P] [Module R P] {N : Type u_4} {N' : Type u_5} [AddCommMonoid N] [Module R N] [Module B N] [IsScalarTower R B N] [AddCommMonoid N'] [Module R N'] [Module B N'] [IsScalarTower R B N'] (f : N →ₗ[B] N') : Function.Injective ⇑(lTensor (TensorProduct R B P) f) ↔ Function.Injective ⇑(lTensor P (↑R f))

Tensoring a B-linear map over B with B ⊗[R] P gives an injective map exactly when tensoring its underlying R-linear map with P does.

theorem Module.Basis.range_mk_one_eq_span {R : Type u} {K : Type v} {M : Type w} [CommSemiring R] [Semiring K] [Algebra R K] [AddCommMonoid M] [Module R M] {ι : Type u_1} (b : Basis ι R M) : ((TensorProduct.mk R K M) 1).range = Submodule.span R (Set.range ⇑(baseChange K b))

The unit pure tensors are the R-span of the base change of any basis.

noncomputable def TensorProduct.unitTmulEquiv (R : Type u) (K : Type v) (M : Type w) [CommSemiring R] [Semiring K] [Algebra R K] [AddCommMonoid M] [Module R M] [FaithfulSMul R K] [Module.Flat R M] : M ≃ₗ[R] ↥((mk R K M) 1).range

A flat module is canonically isomorphic to the module of unit pure tensors in its scalar extension along a faithful algebra.

@[simp]

theorem TensorProduct.coe_unitTmulEquiv_apply {R : Type u} {K : Type v} {M : Type w} [CommSemiring R] [Semiring K] [Algebra R K] [AddCommMonoid M] [Module R M] [FaithfulSMul R K] [Module.Flat R M] (m : M) : ↑((unitTmulEquiv R K M) m) = 1 ⊗ₜ[R] m

The unit-tensor equivalence sends a vector to its unit pure tensor. This equation characterizes the equivalence.

@[simp]

theorem TensorProduct.unitTmulEquiv_symm_tmul {R : Type u} {K : Type v} {M : Type w} [CommSemiring R] [Semiring K] [Algebra R K] [AddCommMonoid M] [Module R M] [FaithfulSMul R K] [Module.Flat R M] (m : M) (h : 1 ⊗ₜ[R] m ∈ ((mk R K M) 1).range) : (unitTmulEquiv R K M).symm ⟨1 ⊗ₜ[R] m, h⟩ = m

The inverse unit-tensor equivalence recovers a vector from its unit pure tensor.

instance TensorProduct.free_range_mk_one {R : Type u} {K : Type v} {M : Type w} [CommSemiring R] [Semiring K] [Algebra R K] [AddCommMonoid M] [Module R M] [FaithfulSMul R K] [Module.Free R M] : Module.Free R ↥((mk R K M) 1).range

The module of unit pure tensors is free whenever the original module is free.

theorem TensorProduct.exists_rTensor_section {R : Type u_1} [CommSemiring R] (Q : Type u_2) [DivisionRing Q] [Algebra R Q] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {g : N →ₗ[R] P} (hg : Function.Surjective ⇑g) : ∃ (s : TensorProduct R P Q →ₗ[R] TensorProduct R N Q), ∀ (x : TensorProduct R P Q), ((AlgebraTensorModule.rTensor R Q) g) (s x) = x

A surjection of R-modules has an R-linear section after tensoring with a division ring Q over R, because P ⊗[R] Q is a free Q-module.

theorem TensorProduct.exists_smul_linearMap_eq_self {R : Type u_1} [CommSemiring R] (Q : Type u_2) [Semiring Q] [Algebra R Q] {P : Type u_3} [AddCommMonoid P] [Module R P] {n : R} (hn : IsUnit ((algebraMap R Q) n)) : ∃ (u : TensorProduct R P Q →ₗ[R] TensorProduct R P Q), ∀ (x : TensorProduct R P Q), n • u x = x

If the image of n : R in Q is a unit, multiplication by n on P ⊗[R] Q has an R-linear right inverse.