English
If R → T is surjective on stalks, then the base change map S → S ⊗_R T is also surjective on stalks.
Русский
Если R → T сюръективно на стэках, то отображение базового изменения S → S ⊗_R T также сюръективно на стэках.
LaTeX
$$$\\text{If } (R \\to T)\\text{ has surjective on stalks, then } (S \\to S \\otimes_R T)\\text{ does as well.}$$$
Lean4
theorem baseChange [Algebra R T] [Algebra R S] (hf : (algebraMap R T).SurjectiveOnStalks) :
(algebraMap S (S ⊗[R] T)).SurjectiveOnStalks :=
by
let g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
intro J hJ
rw [surjective_localRingHom_iff]
intro x
obtain ⟨t, r, a, ht, e⟩ := hf.exists_mul_eq_tmul x (J.comap g) inferInstance
refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩
· intro H
simp only [Algebra.algebraMap_eq_smul_one (A := S), Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
id_apply, smul_tmul, ← Algebra.algebraMap_eq_smul_one (A := T)] at H
rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht
exact ht (J.mul_mem_right _ H)
· simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHomCompTriple.comp_apply,
Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one, id_apply, ← e]
rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]
