Base change of a rational vector space along ℤ → ℚ

A ℚ-vector space is already its own extension of scalars from ℤ to ℚ: any additive map out of it into a ℚ-module is automatically ℚ-linear, which is exactly the universal property IsBaseChange asks for. Consequently, for a ℚ-algebra A, the concrete tensor product A ⊗[ℚ] U is a base change of U along ℤ → A, not merely along ℚ → A.

This is what allows a ℚ-vector space to be fed to constructions that take an integral module together with an abstract model of its complexification, such as the conjugation and the pure Hodge structures of TauCeti/Geometry/Hodge/.

Main results

• TauCeti.isBaseChange_rat_id: the identity of a ℚ-vector space, viewed as ℤ-linear, exhibits it as its own rationalification.
• TauCeti.isBaseChange_ratTensorMap: for a ℚ-algebra A, the map u ↦ 1 ⊗ₜ u exhibits A ⊗[ℚ] U as the base change of U along ℤ → A.

theorem TauCeti.isBaseChange_rat_id (U : Type u) [AddCommGroup U] [Module ℚ U] : IsBaseChange ℚ (↑ℤ LinearMap.id)

A ℚ-vector space is its own rationalification: the identity map, viewed as a map of ℤ-modules, exhibits U as the extension of scalars of U along ℤ → ℚ.

def TauCeti.ratTensorMap (A : Type v) [CommRing A] [Algebra ℚ A] (U : Type u) [AddCommGroup U] [Module ℚ U] : U →ₗ[ℤ] TensorProduct ℚ A U

The canonical map of a rational vector space into its scalar extension A ⊗[ℚ] U, viewed as a map of ℤ-modules.

Equations

• TauCeti.ratTensorMap A U = ↑ℤ ((TensorProduct.mk ℚ A U) 1) ∘ₗ ↑ℤ LinearMap.id

@[simp]

theorem TauCeti.ratTensorMap_apply (A : Type v) [CommRing A] [Algebra ℚ A] (U : Type u) [AddCommGroup U] [Module ℚ U] (u : U) : (ratTensorMap A U) u = 1 ⊗ₜ[ℚ] u

theorem TauCeti.isBaseChange_ratTensorMap (A : Type v) [CommRing A] [Algebra ℚ A] (U : Type u) [AddCommGroup U] [Module ℚ U] : IsBaseChange A (ratTensorMap A U)

For a ℚ-algebra A, the tensor product A ⊗[ℚ] U of a rational vector space is a base change of U along ℤ → A, and not only along ℚ → A.