English
The symmetrized base-change isomorphism interacts with the derivation map D in a specific way: applying the inverse of the base-change isomorphism to the derivation coming from the algebra map matches the simple tensor product of scalars with the derivation on the source. This is a compatibility check between the Kahler base-change isomorphism and derivations.
Русский
Симметрическая базовая изоморфия Каэлера совместима с отображением производной D в точном виде: применение обратного базового изоморфизма к производной, полученной из алгебраической карты, совпадает с тензорным произведением скаляров с производной на источнике. Это совместимость базового изменения Каэлера и дифференциалов.
LaTeX
$$$(\\text{tensorKaehlerEquivOfFormallyEtale}(R,S,T))^{-1}(D_{R,T}(\\text{algebraMap}_{S\\to T}(s))) = 1 \\otimes D_{R,S}(s).$$$
Lean4
theorem tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap [Algebra.FormallyEtale S T] (s : S) :
(tensorKaehlerEquivOfFormallyEtale R S T).symm (D R T (algebraMap S T s)) = 1 ⊗ₜ D R S s := by
rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul, one_smul, map_D]
