Base change of divided power algebras

For a commutative R-algebra S and an R-module M, the canonical map S ⊗[R] Γ_R(M) → Γ_S(S ⊗[R] M), s ⊗ dp R n m ↦ s • dp S n (1 ⊗ m), is an isomorphism of S-algebras. It preserves the grading, so it restricts to S-linear equivalences S ⊗[R] Γ^d_R(M) ≃ Γ^d_S(S ⊗[R] M) of homogeneous pieces, taking 1 ⊗ dp R d m to dp S d (1 ⊗ m). No flatness of S and no freeness or finiteness of M is assumed.

Main declarations

• DividedPowerAlgebra.baseChangeEquiv: the S-algebra isomorphism S ⊗[R] Γ_R(M) ≃ₐ[S] Γ_S(S ⊗[R] M).
• DividedPowerAlgebra.baseChangeEquiv_tmul, DividedPowerAlgebra.baseChangeEquiv_pow_tmul_dp and DividedPowerAlgebra.baseChangeEquiv_symm_dp: its values in both directions.
• DividedPowerAlgebra.baseChangeHomogeneousEquiv: the S-linear isomorphism S ⊗[R] Γ^d_R(M) ≃ₗ[S] Γ^d_S(S ⊗[R] M) on homogeneous pieces.

Implementation notes

The inverse sends dp S n x, for any x : S ⊗[R] M, to the X ^ n-coefficient of the divided-power exponential DividedPowerAlgebra.exp x, which takes values in S ⊗[R] Γ_R(M). This is well defined because the coefficients of the exponential satisfy the defining relations of Γ_S(S ⊗[R] M), and the universal property DividedPowerAlgebra.lift' applies. The layout follows Mathlib's base change of exterior algebras, ExteriorAlgebra.baseChangeEquiv.

References

• [N. Roby, Lois polynômes et lois formelles en théorie des modules (1963), Théorème III.3][Roby-1963]
• The ambient DividedPowerAlgebra, its functorial map and lift' are the Mathlib formalization by Antoine Chambert-Loir and María Inés de Frutos-Fernández.

noncomputable def DividedPowerAlgebra.baseChangeEquiv (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] : TensorProduct R S (DividedPowerAlgebra R M) ≃ₐ[S] DividedPowerAlgebra S (TensorProduct R S M)

Base change of divided power algebras: for a commutative R-algebra S, the canonical map S ⊗[R] Γ_R(M) → Γ_S(S ⊗[R] M) is an isomorphism of S-algebras. No flatness is assumed.

@[simp]

theorem DividedPowerAlgebra.baseChangeEquiv_tmul (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (s : S) (z : DividedPowerAlgebra R M) : (baseChangeEquiv R M S) (s ⊗ₜ[R] z) = s • (map S ((TensorProduct.mk R S M) 1)) z

The base change isomorphism sends s ⊗ z to s times the image of z under the functorial map M → S ⊗[R] M, m ↦ 1 ⊗ m.

theorem DividedPowerAlgebra.baseChangeEquiv_pow_tmul_dp (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (s : S) (n : ℕ) (m : M) : (baseChangeEquiv R M S) ((s ^ n) ⊗ₜ[R] dp R n m) = dp S n (s ⊗ₜ[R] m)

The base change isomorphism sends s ^ n ⊗ dp R n m to dp S n (s ⊗ m).

theorem DividedPowerAlgebra.baseChangeEquiv_one_tmul_dp (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (n : ℕ) (m : M) : (baseChangeEquiv R M S) (1 ⊗ₜ[R] dp R n m) = dp S n (1 ⊗ₜ[R] m)

The base change isomorphism sends 1 ⊗ dp R n m to dp S n (1 ⊗ m).

theorem DividedPowerAlgebra.baseChangeEquiv_symm_dp (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (n : ℕ) (x : TensorProduct R S M) : (baseChangeEquiv R M S).symm (dp S n x) = (PowerSeries.coeff n) (exp x)

The inverse of the base change isomorphism sends dp S n x to the X ^ n-coefficient of the divided-power exponential of x.

@[simp]

theorem DividedPowerAlgebra.baseChangeEquiv_symm_dp_tmul (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (n : ℕ) (s : S) (m : M) : (baseChangeEquiv R M S).symm (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m

The inverse of the base change isomorphism sends dp S n (s ⊗ m) to s ^ n ⊗ dp R n m.

noncomputable def DividedPowerAlgebra.baseChangeHomogeneousEquiv (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (d : ℕ) : TensorProduct R S ↥(homogeneousSubmodule d) ≃ₗ[S] ↥(homogeneousSubmodule d)

Base change of homogeneous divided powers: for a commutative R-algebra S, the base change isomorphism restricts to an S-linear isomorphism S ⊗[R] Γ^d_R(M) ≃ₗ[S] Γ^d_S(S ⊗[R] M) taking 1 ⊗ dp R d m to dp S d (1 ⊗ m) (baseChangeHomogeneousEquiv_one_tmul_dp). No flatness is assumed.

theorem DividedPowerAlgebra.coe_baseChangeHomogeneousEquiv_apply (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (d : ℕ) (z : TensorProduct R S ↥(homogeneousSubmodule d)) : ↑((baseChangeHomogeneousEquiv R M S d) z) = (baseChangeEquiv R M S) ((LinearMap.baseChange S (homogeneousSubmodule d).subtype) z)

The base change isomorphism of homogeneous pieces is the restriction of baseChangeEquiv.

@[simp]

theorem DividedPowerAlgebra.baseChangeHomogeneousEquiv_one_tmul_dp (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (d : ℕ) (m : M) : (baseChangeHomogeneousEquiv R M S d) (1 ⊗ₜ[R] ⟨dp R d m, ⋯⟩) = ⟨dp S d (1 ⊗ₜ[R] m), ⋯⟩

The base change isomorphism of homogeneous pieces sends 1 ⊗ dp R d m to dp S d (1 ⊗ m).

@[simp]

theorem DividedPowerAlgebra.baseChangeHomogeneousEquiv_symm_dp_tmul (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] (d : ℕ) (s : S) (m : M) : (baseChangeHomogeneousEquiv R M S d).symm ⟨dp S d (s ⊗ₜ[R] m), ⋯⟩ = (s ^ d) ⊗ₜ[R] ⟨dp R d m, ⋯⟩

The inverse of the base change isomorphism of homogeneous pieces sends dp S d (s ⊗ m) to s ^ d ⊗ dp R d m.