Module

Dedekind.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Dedekind

8 declarations indexed from sourceView source ↗

Module documentation

Prime divisors finite on a Dedekind model

This file identifies a prime divisor of a fraction field which is finite on a Dedekind model with the height-one prime at its center. In particular, the center is automatically nonzero and determines the valuation subring.

Imports2

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Basic
Mathlib.RingTheory.DedekindDomain.AdicValuation

Imported by2

theorem

centerAlong_ne_bot

L41 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerAlong_ne_bot

Documentation

The center on a Dedekind model cannot be the zero ideal.

Indeed, if it were zero, every nonzero denominator from S would become a unit in the valuation ring. Since F is the fraction field of S, this would put every element of F in the valuation ring, contradicting the properness forced by its DVR structure.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem centerAlong_ne_bot
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong (IsScalarTower.toAlgHom K S F)) :
    v.centerAlong (IsScalarTower.toAlgHom K S F) hfinite ≠ ⊥

def

centerHeightOneSpectrum

L79 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerHeightOneSpectrum

Documentation

The nonzero prime of a Dedekind model obtained as the center of v.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

def centerHeightOneSpectrum
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong (IsScalarTower.toAlgHom K S F)) :
    IsDedekindDomain.HeightOneSpectrum S

theorem

centerHeightOneSpectrum_asIdeal

L88 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerHeightOneSpectrum_asIdeal

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem centerHeightOneSpectrum_asIdeal
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong (IsScalarTower.toAlgHom K S F)) :
    (v.centerHeightOneSpectrum hfinite).asIdeal =
      v.centerAlong (IsScalarTower.toAlgHom K S F) hfinite

theorem

valuationSubringAtCenter_le

L99 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.valuationSubringAtCenter_le

Documentation

The canonical valuation subring obtained by localizing the Dedekind model at the center is contained in the valuation subring of v.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem valuationSubringAtCenter_le
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong (IsScalarTower.toAlgHom K S F)) :
    IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F
        (v.centerHeightOneSpectrum hfinite) ≤
      v.valuationSubring

theorem

valuationSubringAtCenter_eq

L124 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.valuationSubringAtCenter_eq

Documentation

The valuation subring of a prime divisor finite on a Dedekind model is exactly the canonical localization at its center.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem valuationSubringAtCenter_eq
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong (IsScalarTower.toAlgHom K S F)) :
    IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F
        (v.centerHeightOneSpectrum hfinite) =
      v.valuationSubring

theorem

ext_valuationSubring

L135 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.ext_valuationSubring

Documentation

Prime-divisor structures are determined by their valuation subrings.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem ext_valuationSubring
    {v₁ v₂ : FunctionFieldPrimeDivisor K F}
    (h : v₁.valuationSubring = v₂.valuationSubring) :
    v₁ = v₂

theorem

valuationSubring_eq_of_centerAlong_eq

L149 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.valuationSubring_eq_of_centerAlong_eq

Documentation

Two prime divisors finite on the same Dedekind model and having the same center have the same valuation subring.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem valuationSubring_eq_of_centerAlong_eq
    (v₁ v₂ : FunctionFieldPrimeDivisor K F)
    (hfinite₁ : v₁.FiniteAlong (IsScalarTower.toAlgHom K S F))
    (hfinite₂ : v₂.FiniteAlong (IsScalarTower.toAlgHom K S F))
    (hcenter :
      v₁.centerAlong (IsScalarTower.toAlgHom K S F) hfinite₁ =
        v₂.centerAlong (IsScalarTower.toAlgHom K S F) hfinite₂) :
    v₁.valuationSubring = v₂.valuationSubring

theorem

eq_of_centerAlong_eq

L178 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.eq_of_centerAlong_eq

Documentation

On a Dedekind model, a finite prime divisor is uniquely determined by its center.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open IsLocalRing
universe u v w
variable {K : Type u} {S : Type v} {F : Type w}
  [Field K] [CommRing S] [IsDedekindDomain S] [Field F]
  [Algebra K S] [Algebra K F] [Algebra S F] [IsScalarTower K S F]
  [IsFractionRing S F]

Lean source · statement

theorem eq_of_centerAlong_eq
    (v₁ v₂ : FunctionFieldPrimeDivisor K F)
    (hfinite₁ : v₁.FiniteAlong (IsScalarTower.toAlgHom K S F))
    (hfinite₂ : v₂.FiniteAlong (IsScalarTower.toAlgHom K S F))
    (hcenter :
      v₁.centerAlong (IsScalarTower.toAlgHom K S F) hfinite₁ =
        v₂.centerAlong (IsScalarTower.toAlgHom K S F) hfinite₂) :
    v₁ = v₂

Module documentation

Prime divisors finite on a Dedekind model

Declarations