English
A variant of the map compatibility for relative Kaehler differentials; explicit equality of KaehlerDifferential.map applied to morphisms and R.map f.
Русский
Вариант совместимости отображения KaehlerDifferential для относительных дифференциалов; явное равенство отображения KaehlerDifferential.apply к morphism и R.map f.
LaTeX
$$$\mathrm{LinearMap}.coerce\_d( ((relativeDifferentials' φ').map f) )\; x = \mathrm{KaehlerDifferential.d}(R.map f x)$$$
Lean4
@[simp]
theorem relativeDifferentials'_map_d {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : R.obj X) :
DFunLike.coe (α := CommRingCat.KaehlerDifferential (φ'.app X)) (β := fun _ ↦
CommRingCat.KaehlerDifferential (φ'.app Y))
(ModuleCat.Hom.hom (R := ↑(R.obj X)) ((relativeDifferentials' φ').map f))
(CommRingCat.KaehlerDifferential.d x) =
CommRingCat.KaehlerDifferential.d (R.map f x) :=
CommRingCat.KaehlerDifferential.map_d (φ'.naturality f) _