map_surjective_of_surjective — Mathlib

English

The range of kerCotangentToTensor matches the restricted kernel after base change.

Русский

Образ kerCotangentToTensor совпадает с ограниченным ядром после изменения базы.

LaTeX

$$$\\mathrm{range}(\\kerCotangentToTensor\\,R\\,A\\,B) = \\mathrm{restrictScalars} _ A (\\kerTotal(R,B))$$$

Lean4

theorem map_surjective_of_surjective (h : Function.Surjective (algebraMap A B)) :
    Function.Surjective (KaehlerDifferential.map R S A B) :=
  by
  rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← @Submodule.restrictScalars_top A B, ← span_range_derivation,
    Submodule.restrictScalars_span _ _ h, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  obtain ⟨y, rfl⟩ := h x
  rw [← KaehlerDifferential.map_D R S A B]
  exact ⟨_, rfl⟩

Похожие утверждения