equiv_iff_of_domain_eq_of_isSeparated

English

Two reduced-to-separated partial maps with the same domain are equivalent if and only if they are equal.

Русский

Две частичные карты от редуцированной к разделимой схеме с одинаковой областью определения эквивалентны тогда и только тогда, когда они равны.

LaTeX

$$$f,equiv g\text{ on }X.PartialMap Y\iff f = g$ when $f.domain = g.domain$.$$

Lean4

/-- Two partial maps from reduced schemes to separated schemes with the same domain are equivalent
if and only if they are equal. -/
theorem equiv_iff_of_domain_eq_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)]
    {f g : X.PartialMap Y} (hfg : f.domain = g.domain) [f.IsOver S] [g.IsOver S] : f.equiv g ↔ f = g :=
  by
  rw [equiv_iff_of_isSeparated_of_le (S := S) f.dense_domain le_rfl hfg.le]
  obtain ⟨Uf, _, f⟩ := f
  obtain ⟨Ug, _, g⟩ := g
  obtain rfl : Uf = Ug := hfg
  simp

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