English
The canonical base-change description identifies Ω_{B/S} as the base change of Ω_{A/R} along R → S, via the pushout map.
Русский
Каноническое описание базового изменения идентифицирует Ω_{B/S} как базовую смену Ω_{A/R} вдоль отображения R → S через пуш-аут-отображение.
LaTeX
$$$\\text{IsBaseChange } S\\big((\\mathrm{map}\\, R\\, S\\, A\\, B).\\restrictScalars\\ R\\big)$$$
Lean4
/-- If `B` is the tensor product of `S` and `A` over `R`,
then `Ω[B⁄S]` is the base change of `Ω[A⁄R]` along `R → S`.
-/
theorem isBaseChange [h : Algebra.IsPushout R S A B] : IsBaseChange S ((map R S A B).restrictScalars R) :=
by
convert (TensorProduct.isBaseChange R Ω[A⁄R] S).comp (IsBaseChange.ofEquiv (tensorKaehlerEquiv R S A B))
refine LinearMap.ext fun x ↦ ?_
simp only [LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, mk_apply,
tensorKaehlerEquiv_tmul, one_smul]
