ext_of_isDominant_of_isSeparated'

English

Let X be a scheme over S and Y over S; if ι: W → X is dominant and ι ≫ f = ι ≫ g, then f = g when X is reduced and Y is separated.

Русский

Пусть X и Y — схемы над S; если ι: W → X доминантна и ι ≫ f = ι ≫ g, тогда f = g, когда X редуцирована и Y разделима.

LaTeX

$$ext_of_isDominant_of_isSeparated (Y \uparrow S) (ι) (hU)$$

Lean4

/-- Suppose `X` is a reduced `S`-scheme and `Y` is a separated `S`-scheme.
For any `S`-morphisms `f g : X ⟶ Y`, `f = g` if `ι ≫ f = ι ≫ g` for some dominant `ι`.
-/
theorem ext_of_isDominant_of_isSeparated' [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)] {f g : X ⟶ Y}
    [f.IsOver S] [g.IsOver S] {W} (ι : W ⟶ X) [IsDominant ι] (hU : ι ≫ f = ι ≫ g) : f = g :=
  ext_of_isDominant_of_isSeparated (Y ↘ S) (by simp) ι hU

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