English
Equality of kernels: the kernel of the linear combination map equals the kernel total kernel.
Русский
Согласование ядер: ядро линейного отображения равно ядру полной карты.
LaTeX
$$$\\ker(\\mathrm{Finsupp.linearCombination}(S,\\mathrm{D}(R,S))) = \\mathrm{kerTotal}(R,S)$$$
Lean4
theorem kerTotal_eq :
LinearMap.ker (Finsupp.linearCombination S (KaehlerDifferential.D R S)) = KaehlerDifferential.kerTotal R S :=
by
apply le_antisymm
· conv_rhs => rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]
rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]
exact LinearMap.ker_le_ker_comp _ _
· rw [KaehlerDifferential.kerTotal, Submodule.span_le]
rintro _ ((⟨⟨x, y⟩, rfl⟩ | ⟨⟨x, y⟩, rfl⟩) | ⟨x, rfl⟩) <;> simp [LinearMap.mem_ker]
