Base change along a ring epimorphism, and rational vector spaces

If R → S is an epimorphism of commutative rings (Algebra.IsEpi R S), then an S-module is already its own extension of scalars from R to S: the identity, viewed as R-linear, exhibits it as such a base change. The main instance is ℤ → ℚ: any additive map out of a ℚ-vector space into a ℚ-module is automatically ℚ-linear. 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_restrictScalars_id: for an epimorphism R → S, the identity of an S-module, viewed as R-linear, exhibits it as its own base change along R → S.
• 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_restrictScalars_id (R : Type u_1) (S : Type u_2) (U : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra.IsEpi R S] [AddCommMonoid U] [Module R U] [Module S U] [IsScalarTower R S U] : IsBaseChange S (↑R LinearMap.id)

If R → S is an epimorphism of commutative rings, then every S-module U is its own base change along R → S: the identity map, viewed as a map of R-modules, exhibits U as the extension of scalars of U from R to S. For ℤ → ℚ, this says that a ℚ-vector space is its own rationalification.

def TauCeti.ratTensorMap (A : Type u_1) [CommRing A] [Algebra ℚ A] (U : Type u_2) [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.

@[simp]

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

theorem TauCeti.isBaseChange_ratTensorMap (A : Type u_1) [CommRing A] [Algebra ℚ A] (U : Type u_2) [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.