toRationalMap_toPartialMap — Mathlib

English

A rational map is recovered by composing the partial map with the rational map; formally, f equals the rational map obtained from its partial map.

Русский

Рациональная карта восстанавливается через частичную карту; формально, f равна рациональной карте, полученной из своей частичной карты.

LaTeX

$$$$ \operatorname{toRationalMap}(\operatorname{toPartialMap}(f)) = f. $$$$

Lean4

@[simp]
theorem toRationalMap_toPartialMap [IsReduced X] [Y.IsSeparated] (f : X ⤏ Y) : f.toPartialMap.toRationalMap = f :=
  by
  obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
  trans (f.toRationalMap.toPartialMap.restrict _ f.dense_domain f.le_domain_toRationalMap).toRationalMap
  · simp
  · congr 1
    exact PartialMap.ext _ f rfl (by simpa using f.toPartialMap_toRationalMap_restrict)

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