ext_of_isAffine — Mathlib

English

If Y is affine and f,g: X ⟶ Y have the same underlying appTop maps, then f = g.

Русский

Если Y аффинна и два морфизма f,g: X ⟶ Y имеют одинаковые отображения appTop, то f = g.

LaTeX

$$$\\text{If } [IsAffine(Y)] \\text{ and } f.appTop = g.appTop, \\text{ then } f=g$$$

Lean4

theorem ext_of_isAffine {X Y : Scheme} [IsAffine Y] {f g : X ⟶ Y} (e : f.appTop = g.appTop) : f = g := by
  rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]

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