isOver_iff — Mathlib

English

A morphism f is over S iff it factors correctly through the structure morphism to S.

Русский

Морфизм f является над S тогда и только тогда, когда он факторизуется через структурный морфизм к S.

LaTeX

$$$f.IsOver S \iff f.compHom (Y \downarrow S) = (X \downarrow S).toRationalMap$$$

Lean4

theorem isOver_iff [X.Over S] [Y.Over S] {f : X ⤏ Y} : f.IsOver S ↔ f.compHom (Y ↘ S) = (X ↘ S).toRationalMap :=
  by
  constructor
  · intro h
    obtain ⟨g, hg, e⟩ := f.exists_partialMap_over S
    rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
  · intro e
    obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
    obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp e
    exact ⟨⟨f.restrict U hU hUl, by simpa using e, by simp⟩⟩

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