Module

IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates.lean

Nyll.AlgebraicCurves.Valuations.IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates

5 declarations indexed from sourceView source ↗

Module documentation

Discrete valuation rings dominating noetherian local domains

This file constructs a height-one prime in a finitely generated subalgebra of the fraction field and uses its integral closure to obtain a discrete valuation ring dominating the local domain.

Imports35

Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Algebra.Subalgebra.Basic
Mathlib.Algebra.Algebra.Tower
Mathlib.Data.Finset.Max
Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.RingTheory.Adjoin.FG
Mathlib.RingTheory.DedekindDomain.Basic
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.RingTheory.DedekindDomain.Dvr
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.Ideal.Height
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Maximal
Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.LocalRing.LocalSubring
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.Localization.LocalizationLocalization
Mathlib.RingTheory.Localization.Submodule
Mathlib.RingTheory.Noetherian.Defs
Mathlib.RingTheory.Valuation.Basic
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Tactic.Ext
Mathlib.Tactic.NormNum.Basic
Mathlib.Tactic.Push
Mathlib.Tactic.Set
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsNoetherianRing_of_ringKrullDim_le_one_of_finiteDimensional_subalgebra

Imported by5

theorem

dimensionLEOne_of_ringKrullDim_le_one

L67 ↗

AlgebraicCurves.Valuations.Proofs.IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates.DvrDomination.dimensionLEOne_of_ringKrullDim_le_one

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates
universe u v
open IsLocalRing
namespace DvrDomination

Lean source · statement

theorem dimensionLEOne_of_ringKrullDim_le_one (C : Type u) [CommRing C] [IsDomain C]
    (h : ringKrullDim C ≤ 1) : Ring.DimensionLEOne C

theorem

exists_dvr_of_height_le_one

L92 ↗

AlgebraicCurves.Valuations.Proofs.IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates.DvrDomination.exists_dvr_of_height_le_one

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates
universe u v
open IsLocalRing
namespace DvrDomination
section StepB
variable {K : Type v} [Field K]

Lean source · statement

theorem exists_dvr_of_height_le_one (S : Subring K) [IsNoetherianRing S] [IsFractionRing S K]
    (P : Ideal S) [hP : P.IsPrime] (hP0 : P ≠ ⊥) (hP1 : P.height ≤ 1) :
    ∃ V : ValuationSubring K, IsDiscreteValuationRing ↥V ∧ S ≤ V.toSubring ∧
      ∀ s : S, s ∈ P ↔ (s : K) ∈ V.nonunits

theorem

exists_subalgebra_prime_height_le_one

L188 ↗

AlgebraicCurves.Valuations.Proofs.IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates.DvrDomination.exists_subalgebra_prime_height_le_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates
universe u v
open IsLocalRing
namespace DvrDomination
section StepA
variable {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsLocalRing R]
variable {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K]
omit [IsDomain R] in

Lean source · statement

theorem exists_subalgebra_prime_height_le_one (hR : ¬ IsField R) :
    ∃ (S : Subalgebra R K) (P : Ideal ↥S) (_ : P.IsPrime),
      IsNoetherianRing ↥S ∧ P ≠ ⊥ ∧ P.height ≤ 1 ∧
      ∀ r : R, r ∈ maximalIdeal R ↔ algebraMap R ↥S r ∈ P

theorem

main

L318 ↗

AlgebraicCurves.Valuations.Proofs.IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates.DvrDomination.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates
universe u v
open IsLocalRing
namespace DvrDomination

Lean source · statement

theorem main
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsLocalRing R] (hR : ¬ IsField R)
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :
    ∃ V : ValuationSubring K, IsDiscreteValuationRing ↥V ∧
      (∀ r : R, algebraMap R K r ∈ V) ∧
      (∀ r : R, r ∈ maximalIdeal R ↔ algebraMap R K r ∈ V.nonunits)

theorem

exists_valuationSubring_isDiscreteValuationRing_dominates

L342 ↗

IsLocalRing.exists_valuationSubring_isDiscreteValuationRing_dominates

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates
universe u v
open IsLocalRing

Lean source · statement

theorem _root_.IsLocalRing.exists_valuationSubring_isDiscreteValuationRing_dominates
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsLocalRing R] (hR : ¬ IsField R)
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :
    ∃ V : ValuationSubring K, IsDiscreteValuationRing ↥V ∧
      (∀ r : R, algebraMap R K r ∈ V) ∧
      (∀ r : R, r ∈ maximalIdeal R ↔ algebraMap R K r ∈ V.nonunits)

Module documentation

Discrete valuation rings dominating noetherian local domains

Declarations

dimensionLEOne_of_ringKrullDim_le_one

exists_dvr_of_height_le_one

exists_subalgebra_prime_height_le_one

main

exists_valuationSubring_isDiscreteValuationRing_dominates