Module

valuationRing_stalk_of_smoothOfRelativeDimension_one.lean

Nyll.AlgebraicCurves.Geometry.Schemes.valuationRing_stalk_of_smoothOfRelativeDimension_one

4 declarations indexed from sourceView source ↗

Module documentation

Valuation stalks of integral smooth curves

The stalks of an integral scheme smooth of relative dimension one over a field are valuation rings, as shown using local standard-smooth presentations.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Unramified.LocalRing
Mathlib.Tactic.Algebraize

Imported by4

theorem

valuationRing_of_surjective

L38 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.valuationRing_stalk_of_smoothOfRelativeDimension_one.SmoothCurveStalk.valuationRing_of_surjective

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace valuationRing_stalk_of_smoothOfRelativeDimension_one
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace SmoothCurveStalk

Lean source · statement

theorem valuationRing_of_surjective {A B : Type*} [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsDomain B] (f : A →+* B) (hf : Function.Surjective f) : ValuationRing B

theorem

valuationRing_localization_atPrime

L48 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.valuationRing_stalk_of_smoothOfRelativeDimension_one.SmoothCurveStalk.valuationRing_localization_atPrime

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace valuationRing_stalk_of_smoothOfRelativeDimension_one
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace SmoothCurveStalk

Lean source · statement

theorem valuationRing_localization_atPrime {R B : Type*} [CommRing R] [CommRing B]
    [Algebra R B] [IsDomain B] [IsNoetherianRing B] [Algebra.EssFiniteType R B]
    (q : Ideal B) [q.IsPrime] [Algebra.IsUnramifiedAt R q] (hp : (q.under R).IsPrincipal) :
    ValuationRing (Localization.AtPrime q)

theorem

isPrincipalIdealRing_mvPolynomial_fin_one

L65 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.valuationRing_stalk_of_smoothOfRelativeDimension_one.SmoothCurveStalk.isPrincipalIdealRing_mvPolynomial_fin_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace valuationRing_stalk_of_smoothOfRelativeDimension_one
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace SmoothCurveStalk

Lean source · statement

theorem isPrincipalIdealRing_mvPolynomial_fin_one (K : Type*) [Field K] :
    IsPrincipalIdealRing (MvPolynomial (Fin 1) K)

theorem