exact_mapBaseChange_map — Mathlib

English

The range of kerCotangentToTensor coincides with the restricted kernel under the base change map.

Русский

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

LaTeX

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

Lean4

/-- The sequence `B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0` is exact.
Also see `KaehlerDifferential.map_surjective`. -/
theorem exact_mapBaseChange_map : Function.Exact (mapBaseChange R A B) (map R A B B) :=
  SetLike.ext_iff.mp (range_mapBaseChange R A B).symm

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