English
The kernel of map f is characterized by a simple equality using map_simp and kerTotal identifications.
Русский
Ядро отображения описывается простым равенством через map_simp и идентификации kerTotal.
LaTeX
$$$\\ker(\\mathrm{map}\\,R\\,R\\,A\\,B) = \\kerTotal(R,A) \\text{ composed with simplifications}$$$
Lean4
theorem ker_map :
LinearMap.ker (KaehlerDifferential.map R S A B) =
(((kerTotal S B).restrictScalars A).comap finsupp_map).map (Finsupp.linearCombination (M := Ω[A⁄R]) A (D R A)) :=
by
rw [← Submodule.map_comap_eq_of_surjective (linearCombination_surjective R A) (LinearMap.ker _)]
congr 1
ext x
simp only [Submodule.mem_comap, LinearMap.mem_ker, Finsupp.apply_linearCombination, ← kerTotal_eq,
Submodule.restrictScalars_mem]
simp only [linearCombination_apply, Function.comp_apply, LinearMap.coe_comp, lmapDomain_apply,
Finsupp.mapRange.linearMap_apply]
rw [Finsupp.sum_mapRange_index, Finsupp.sum_mapDomain_index]
· simp
· simp
· simp [add_smul]
· simp
