English
The range of kerCotangentToTensor equals the restricted kernel of the map after base change.
Русский
Образ kerCotangentToTensor равен ограниченному ядру после базового изменения.
LaTeX
$$$\\mathrm{range}(\\kerCotangentToTensor\\,R\\,A\\,B) = (\\ker(\\mathrm{mapBaseChange}\\,R\\,A\\,B)).\\text{restrictScalars } A$$$
Lean4
/-- Given the commutative diagram
```
A --→ B
↑ ↑
| |
R --→ S
```
The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/S}` is spanned by the image of the
kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `ds` with `s : S`.
See `kerTotal_map'` for the special case where `R = S`.
-/
theorem kerTotal_map [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B]
(h : Function.Surjective (algebraMap A B)) :
(KaehlerDifferential.kerTotal R A).map finsupp_map ⊔
Submodule.span A (Set.range fun x : S => .single (algebraMap S B x) (1 : B)) =
(KaehlerDifferential.kerTotal S B).restrictScalars _ :=
by
rw [KaehlerDifferential.kerTotal, Submodule.map_span, KaehlerDifferential.kerTotal,
Submodule.restrictScalars_span _ _ h]
simp_rw [Set.image_union, Submodule.span_union, ← Set.image_univ, Set.image_image, Set.image_univ, map_sub, map_add]
simp only [LinearMap.comp_apply, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, Finsupp.mapRange.linearMap_apply,
Finsupp.mapRange_single, Algebra.linearMap_apply, map_one, map_add, map_mul]
simp_rw [sup_assoc, ← (h.prodMap h).range_comp]
congr!
rw [sup_eq_right]
apply Submodule.span_mono
simp_rw [← IsScalarTower.algebraMap_apply R A B, IsScalarTower.algebraMap_apply R S B]
exact Set.range_comp_subset_range (algebraMap R S) fun x => Finsupp.single (algebraMap S B x) (1 : B)
