equiv_toPartialMap_iff_of_isSeparated

English

A reduced-to-separated partial map f is equivalent to a morphism g if and only if f.hom = f.domain.ι ≫ g.

Русский

Частичная карта f эквивалентна морфизму g тогда и только тогда, когда f.hom = f.domain.ι ∘ g.

LaTeX

$$$f\equiv g.f \,?\;f\hom = f.domain.ι \circ g$$$

Lean4

/-- A partial map from a reduced scheme to a separated scheme is equivalent to a morphism
if and only if it is equal to the restriction of the morphism. -/
theorem equiv_toPartialMap_iff_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)]
    {f : X.PartialMap Y} {g : X ⟶ Y} [f.IsOver S] [g.IsOver S] : f.equiv g.toPartialMap ↔ f.hom = f.domain.ι ≫ g :=
  by
  rw [equiv_iff_of_isSeparated (S := S), ← cancel_epi (X.isoOfEq (inf_top_eq f.domain)).hom]
  simp
  rfl

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