English
Let R, A, B be rings with A a commutative R-algebra and B an A-algebra such that the ring homomorphism A → B is surjective. Then the natural map on Kaehler differentials arising from base change, mapBaseChange, is surjective; i.e., every element of Ω_{B/R} is the image of some element of Ω_{A/R} ⊗_A B.
Русский
Пусть R, A, B — кольца, A — коммутативное R-обобщение, B — A-обобщение и отображение A → B сюръективно. Тогда естественный переход между дифференциалами Кэйлера, вызванный базовым изменением, отображение mapBaseChange, сюръективен; любой элемент Ω_{B/R} лежит в образе некоторого элемента Ω_{A/R} ⊗_A B.
LaTeX
$$$$\forall \omega \in \Omega_{B/R}, \exists \xi \in \Omega_{A/R} \otimes_A B \text{ такая, что } \mathrm{mapBaseChange}_{R,A,B}(\xi) = \omega.$$$$
Lean4
theorem mapBaseChange_surjective (h : Function.Surjective (algebraMap A B)) :
Function.Surjective (KaehlerDifferential.mapBaseChange R A B) :=
by
have := subsingleton_of_surjective A B h
rw [← LinearMap.range_eq_top, range_mapBaseChange, ← top_le_iff]
exact fun x _ ↦ Subsingleton.elim _ _
