English
If A is formally smooth over R, then B ⊗R A is formally smooth over B.
Русский
Если A формально гладко над R, то B ⊗R A формально гладко над B.
LaTeX
$$$[\operatorname{FormallySmooth} R A] \Rightarrow \operatorname{FormallySmooth} B (B \otimes_R A)$$$
Lean4
instance base_change [FormallySmooth R A] : FormallySmooth B (B ⊗[R] A) :=
by
constructor
intro C _ _ I hI f
letI := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
refine ⟨TensorProduct.productLeftAlgHom (Algebra.ofId B C) ?_, ?_⟩
· exact FormallySmooth.lift I ⟨2, hI⟩ ((f.restrictScalars R).comp TensorProduct.includeRight)
· apply AlgHom.restrictScalars_injective R
apply TensorProduct.ext'
intro b a
suffices algebraMap B _ b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a) by simpa [Algebra.ofId_apply]
rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
