Module

Eq_of_range_stalk_eq.lean

Nyll.AlgebraicCurves.Models.Eq_of_range_stalk_eq

1 declaration indexed from sourceView source ↗

Module documentation

Eq of range stalk eq

Points of an integral curve are identified by the images of their local rings in the function field.

Imports2

Imported by15

theorem

eq_of_range_stalk_eq

L31 ↗

AlgebraicCurve.eq_of_range_stalk_eq

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Eq_of_range_stalk_eq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u

Lean source · statement

theorem _root_.AlgebraicCurve.eq_of_range_stalk_eq
    {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (x y : C)
    (h : (algebraMap (C.presheaf.stalk x) C.functionField).range =
      (algebraMap (C.presheaf.stalk y) C.functionField).range) :
    x = y

Module documentation

Eq of range stalk eq

Declarations

eq_of_range_stalk_eq