English
If S → T is a formally étale algebra map, then T is a base change of the map map: R → R with respect to S and T. In particular, the canonical base-change morphism associated to the étale map is bijective, encapsulating a base-change property of étale morphisms.
Русский
Если S → T — формально этиальная карта алгебр, то T является базовым изменением карты map: R → R относительно S и T. В частности биективность связанного отображения базового изменения отражает свойство оснований эtale.
LaTeX
$$$\\text{IsBaseChange}(T, \\mathrm{map}_{R,R,S,T})$$$
Lean4
theorem isBaseChange_of_formallyEtale [Algebra.FormallyEtale S T] : IsBaseChange T (map R R S T) :=
by
change Function.Bijective _
convert (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1
change _ = ((tensorKaehlerEquivOfFormallyEtale R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)
congr!
ext
simp
