English
The map composition equals the restricted derivative after base change: map R S A B composed with D R A yields a derivation-based composition.
Русский
Сжатие отображения через композицию эквивалентно композиции, основанной на производной после изменения базы.
LaTeX
$$$(\\mathrm{map}\\,R\\,S\\,A\\,B) \\circ (\\mathrm{D}\\,R\\,A) = (\\mathrm{D}\\,S\\,B) \\restrictionScalars R \\circ \\mathrm{compAlgebraMap}$$$
Lean4
/-- This is a special case of `kerTotal_map` where `R = S`.
The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/R}` is spanned by the image of the
kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `da` with `a : A`.
-/
theorem kerTotal_map' [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective (algebraMap A B)) :
(KaehlerDifferential.kerTotal R A ⊔ Submodule.span A (Set.range fun x ↦ .single (algebraMap R A x) 1)).map
finsupp_map =
(KaehlerDifferential.kerTotal R B).restrictScalars _ :=
by
rw [Submodule.map_sup, ← kerTotal_map R R A B h, Submodule.map_span, ← Set.range_comp]
congr
ext; simp [IsScalarTower.algebraMap_eq R A B]
