NYLL
Module

SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_isClosed.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_isClosed
1 declaration indexed from sourceView source ↗

Module documentation

Discrete valuation stalks at closed points of smooth curves

An integral scheme smooth of relative dimension one over a field has a discrete valuation ring as its stalk at every closed point.

Imports3
Imported by5

Declarations

theorem

isDiscreteValuationRing_stalk_of_isClosed

L33 ↗
AlgebraicGeometry.SmoothOfRelativeDimension.isDiscreteValuationRing_stalk_of_isClosed
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_isClosed
universe u
open CategoryTheory AlgebraicGeometry IsLocalRing
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothOfRelativeDimension.isDiscreteValuationRing_stalk_of_isClosed
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k))
    [IsIntegral X] [SmoothOfRelativeDimension 1 f]
    (x : X) (hx : IsClosed ({x} : Set X)) :
    IsDiscreteValuationRing (X.presheaf.stalk x)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.