Module

SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_section.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_section

1 declaration indexed from sourceView source ↗

Module documentation

Discrete valuation stalks along a section

A section of an integral smooth curve over a field determines a closed point whose stalk is a discrete valuation ring.

Imports2

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_isClosed

Imported by4

theorem

isDiscreteValuationRing_stalk_of_section

L33 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.isDiscreteValuationRing_stalk_of_section

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_section
universe u
open CategoryTheory AlgebraicGeometry IsLocalRing

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothOfRelativeDimension.isDiscreteValuationRing_stalk_of_section
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k))
    [IsIntegral X] [SmoothOfRelativeDimension 1 f]
    (p : Spec (CommRingCat.of k) ⟶ X) (hp : p ≫ f = 𝟙 _) :
    IsDiscreteValuationRing (X.presheaf.stalk (p.base (IsLocalRing.closedPoint k)))

Module documentation

Discrete valuation stalks along a section

Declarations

isDiscreteValuationRing_stalk_of_section