Theorems · Theorem · algebraic geometry

AlgebraicGeometry.ext_of_apply_eq

∀ {X Y : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [IsAlgClosed K] {f g : X ⟶ Y}
  (i : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsSeparated i]
  [AlgebraicGeometry.LocallyOfFiniteType i] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f i)] (S : Set ↥X),
  IsLocallyClosed S →
    Dense S →
      (∀ x ∈ S, IsClosed {x} → f x = g x) →
        CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i → f = g

Let X and Y be locally of finite type K-schemes with K algebraically closed and Y separated over K. Suppose X is reduced, then two K-morphisms f g : X ⟶ Y are equal if they are equal on the closed points of a dense locally closed subset of X.

Defined in

Mathlib.AlgebraicGeometry.AlgClosed.Basic

Cited by

1 results in Mathlib

Foundations

Depth 232 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldIsAlgClosedAlgebraicGeometry.IsSeparatedAlgebraicGeometry.LocallyOfFiniteTypeAlgebraicGeometry.IsReducedAlgebraicGeometry.LocallyOfFiniteType