Module

OverDVR.lean

Nyll.AlgebraicCurves.Places.OverDVR

50 declarations indexed from sourceView source ↗

Module documentation

OverDVR

Places above a discrete valuation ring correspond to height-one primes of its integral closure, with finite fibres over a base place.

Imports5

Nyll.AlgebraicCurves.Divisors.Maps
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.RamificationInertia.Basic
Mathlib.RingTheory.DedekindDomain.Factorization
Mathlib.Algebra.Polynomial.Lifts

Imported by91

theorem

ord_nonneg_of_mem

L38 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

ord_eq_zero_iff_adicValuation_eq_one

L53 ↗

AlgebraicCurve.Place.ord_eq_zero_iff_adicValuation_eq_one

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_eq_zero_iff_adicValuation_eq_one {f : F} (hf : f ≠ 0) :
    v.ord f = 0 ↔ v.adicValuation f = 1

theorem

ord_neg

L72 ↗

AlgebraicCurve.Place.ord_neg

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section IntegrallyClosed
open Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

Lean source · statement

theorem ord_neg (f : F) : w.ord (-f) = w.ord f

theorem

mem_of_eval_monic_eq_zero

L75 ↗

AlgebraicCurve.Place.mem_of_eval_monic_eq_zero

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section IntegrallyClosed
open Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

Lean source · statement

theorem mem_of_eval_monic_eq_zero {P : Polynomial F} (hP : P.Monic)
    (hcoeff : ∀ i, P.coeff i ∈ w.toValuationSubring) {x : F} (hx : P.eval x = 0) :
    x ∈ w.toValuationSubring

theorem

mem_maximalIdeal_iff_ord_pos

L89 ↗

AlgebraicCurve.Place.mem_maximalIdeal_iff_ord_pos

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section IntegrallyClosed
open Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

Lean source · statement

theorem mem_maximalIdeal_iff_ord_pos {x : F} (hx : x ≠ 0)
    (hmem : x ∈ w.toValuationSubring) :
    (⟨x, hmem⟩ : w.toValuationSubring) ∈ IsLocalRing.maximalIdeal w.toValuationSubring ↔
      0 < w.ord x

def

chartHom

L107 ↗

AlgebraicCurve.Place.chartHom

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)

Lean source · statement

def chartHom (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    R →+* w.toValuationSubring

theorem

coe_chartHom

L113 ↗

AlgebraicCurve.Place.coe_chartHom

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
omit [IsDedekindDomain R] [IsFractionRing R F] in

Lean source · statement

theorem coe_chartHom (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) (r : R) :
    (chartHom w hw r : F) = algebraMap R F r

def

center

L118 ↗

AlgebraicCurve.Place.center

Documentation

The centre ideal obtained by pulling back the maximal ideal of the place.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

def center (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) : Ideal R

instance

(anonymous instance)

L121 ↗

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

instance (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    (center R w hw).IsPrime

theorem

mem_center_iff

L126 ↗

AlgebraicCurve.Place.mem_center_iff

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
omit [IsDedekindDomain R] [IsFractionRing R F] in

Lean source · statement

theorem mem_center_iff (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) {r : R} :
    r ∈ center R w hw ↔
      (⟨algebraMap R F r, hw r⟩ : w.toValuationSubring) ∈
        IsLocalRing.maximalIdeal w.toValuationSubring

theorem

mem_center_iff_ord_pos

L132 ↗

AlgebraicCurve.Place.mem_center_iff_ord_pos

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

theorem mem_center_iff_ord_pos (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring)
    {r : R} (hr : r ≠ 0) :
    r ∈ center R w hw ↔ 0 < w.ord (algebraMap R F r)

theorem

inv_algebraMap_mem

L140 ↗

AlgebraicCurve.Place.inv_algebraMap_mem

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
omit [IsDedekindDomain R] [IsFractionRing R F] in

Lean source · statement

theorem inv_algebraMap_mem (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring)
    {s : R} (hs : IsUnit (chartHom w hw s)) :
    (algebraMap R F s)⁻¹ ∈ w.toValuationSubring

theorem

center_ne_bot

L153 ↗

AlgebraicCurve.Place.center_ne_bot

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

theorem center_ne_bot (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    center R w hw ≠ ⊥

def

centerHeightOneSpectrum

L171 ↗

AlgebraicCurve.Place.centerHeightOneSpectrum

Documentation

The centre regarded as a height-one prime of the base ring.

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

def centerHeightOneSpectrum (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    HeightOneSpectrum R

theorem

centerHeightOneSpectrum_asIdeal

L175 ↗

AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem centerHeightOneSpectrum_asIdeal
    (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    (centerHeightOneSpectrum R w hw).asIdeal = center R w hw

theorem

valuationSubringAtPrime_centerHeightOneSpectrum_le

L179 ↗

AlgebraicCurve.Place.valuationSubringAtPrime_centerHeightOneSpectrum_le

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem valuationSubringAtPrime_centerHeightOneSpectrum_le
    (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    HeightOneSpectrum.valuationSubringAtPrime F (centerHeightOneSpectrum R w hw) ≤
      w.toValuationSubring

theorem

toValuationSubring_eq_of_forall_mem

L188 ↗

AlgebraicCurve.Place.toValuationSubring_eq_of_forall_mem

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem toValuationSubring_eq_of_forall_mem
    (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    w.toValuationSubring =
      HeightOneSpectrum.valuationSubringAtPrime F (centerHeightOneSpectrum R w hw)

theorem

finite_setOf_forall_mem_and_ord_pos

L195 ↗

AlgebraicCurve.Place.finite_setOf_forall_mem_and_ord_pos

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem finite_setOf_forall_mem_and_ord_pos {r₀ : R} (hr₀ : r₀ ≠ 0) :
    {w : Place K F | (∀ r : R, algebraMap R F r ∈ w.toValuationSubring) ∧
      0 < w.ord (algebraMap R F r₀)}.Finite

def

valuationSubringAlgebra

L222 ↗

AlgebraicCurve.Place.valuationSubringAlgebra

Documentation

The valuation-subring algebra structure induced by the original field extension map.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in

Lean source · statement

def valuationSubringAlgebra (v : Place K F) : Algebra v.toValuationSubring F'

abbrev

integralClosureAt

L231 ↗

AlgebraicCurve.Place.integralClosureAt

Documentation

The integral closure of the base place valuation subring in the extension field.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

abbrev integralClosureAt : Type _

instance

(anonymous instance)

L233 ↗

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : IsDedekindDomain (integralClosureAt F' v)

instance

(anonymous instance)

L236 ↗

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : IsFractionRing (integralClosureAt F' v) F'

instance

(anonymous instance)

L239 ↗

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : Module.Finite v.toValuationSubring (integralClosureAt F' v)

theorem

algebraMap_integralClosureAt_injective

L244 ↗

AlgebraicCurve.Place.algebraMap_integralClosureAt_injective

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F']
  [Algebra.IsSeparable F F'] in

Lean source · statement

theorem algebraMap_integralClosureAt_injective :
    Function.Injective
      (algebraMap v.toValuationSubring (integralClosureAt F' v))

instance

(anonymous instance)

L256 ↗

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : Module.IsTorsionFree v.toValuationSubring (integralClosureAt F' v)

theorem

maximalIdeal_ne_bot

L264 ↗

AlgebraicCurve.Place.maximalIdeal_ne_bot

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

theorem maximalIdeal_ne_bot :
    IsLocalRing.maximalIdeal v.toValuationSubring ≠ ⊥

theorem

forall_mem_of_restrict_eq

L277 ↗

AlgebraicCurve.Place.forall_mem_of_restrict_eq

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in

Lean source · statement

theorem forall_mem_of_restrict_eq (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    algebraMap (integralClosureAt F' v) F' c ∈ w.toValuationSubring

def

fiberCenter

L293 ↗

AlgebraicCurve.Place.fiberCenter

Documentation

The height-one centre of an extending place in the integral closure.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

def fiberCenter (hw : w.restrict F = v) : HeightOneSpectrum (integralClosureAt F' v)

theorem

mem_fiberCenter_iff_ord_pos

L296 ↗

AlgebraicCurve.Place.mem_fiberCenter_iff_ord_pos

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem mem_fiberCenter_iff_ord_pos (hw : w.restrict F = v) {c : integralClosureAt F' v}
    (hc : c ≠ 0) :
    c ∈ (fiberCenter F' v hw).asIdeal ↔
      0 < w.ord (algebraMap (integralClosureAt F' v) F' c)

theorem

toValuationSubring_eq_of_restrict_eq

L302 ↗

AlgebraicCurve.Place.toValuationSubring_eq_of_restrict_eq

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem toValuationSubring_eq_of_restrict_eq (hw : w.restrict F = v) :
    w.toValuationSubring =
      HeightOneSpectrum.valuationSubringAtPrime F' (fiberCenter F' v hw)

theorem

mem_maximalIdeal_iff_ord_pos'

L307 ↗

AlgebraicCurve.Place.mem_maximalIdeal_iff_ord_pos'

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem mem_maximalIdeal_iff_ord_pos' {r : v.toValuationSubring} (hr : r ≠ 0) :
    r ∈ IsLocalRing.maximalIdeal v.toValuationSubring ↔
      0 < v.ord (algebraMap v.toValuationSubring F r)

theorem

algebraMap_integralClosureAt_ne_zero

L317 ↗

AlgebraicCurve.Place.algebraMap_integralClosureAt_ne_zero

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F']
  [Algebra.IsSeparable F F'] in

Lean source · statement

theorem algebraMap_integralClosureAt_ne_zero {r : v.toValuationSubring} (hr : r ≠ 0) :
    algebraMap v.toValuationSubring (integralClosureAt F' v) r ≠ 0

theorem

ord_algebraMap_integralClosureAt

L322 ↗

AlgebraicCurve.Place.ord_algebraMap_integralClosureAt

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in
omit [FiniteDimensional F F'] in

Lean source · statement

theorem ord_algebraMap_integralClosureAt (hw : w.restrict F = v) (r : v.toValuationSubring) :
    w.ord (algebraMap (integralClosureAt F' v) F'
        (algebraMap v.toValuationSubring (integralClosureAt F' v) r))
      = w.ramificationIndex F * v.ord (algebraMap v.toValuationSubring F r)

theorem

fiberCenter_liesOver

L329 ↗

AlgebraicCurve.Place.fiberCenter_liesOver

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem fiberCenter_liesOver (hw : w.restrict F = v) :
    (fiberCenter F' v hw).asIdeal.LiesOver
      (IsLocalRing.maximalIdeal v.toValuationSubring)

def

placeOfPrime

L356 ↗

AlgebraicCurve.Place.placeOfPrime

Documentation

The extending place given by a height-one prime of the integral closure.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Bijection
variable {v : Place K F}

Lean source · full declaration

def placeOfPrime (P : HeightOneSpectrum (integralClosureAt F' v)) : Place K F' where
  toValuationSubring := HeightOneSpectrum.valuationSubringAtPrime F' P
  algebraMap_mem' := fun a => by
    rw [HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring,
      Valuation.mem_valuationSubring_iff]
    have h1 : algebraMap K F' a = algebraMap (integralClosureAt F' v) F'
        (algebraMap v.toValuationSubring (integralClosureAt F' v)
          (algebraMap K v.toValuationSubring a)) := by
      rw [← IsScalarTower.algebraMap_apply,
        IsScalarTower.algebraMap_apply v.toValuationSubring F F',
        ← IsScalarTower.algebraMap_apply K v.toValuationSubring F,
        ← IsScalarTower.algebraMap_apply K F F']
    rw [h1]
    exact P.valuation_le_one _
  ne_top' := by
    rw [HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring]
    simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]
    infer_instance
  isPrincipalIdealRing' := by
    rw [HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring]
    exact isPrincipalIdealRing_valuationSubring P

theorem

placeOfPrime_toValuationSubring

L378 ↗

AlgebraicCurve.Place.placeOfPrime_toValuationSubring

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Bijection
variable {v : Place K F}

Lean source · statement

theorem placeOfPrime_toValuationSubring (P : HeightOneSpectrum (integralClosureAt F' v)) :
    (placeOfPrime P).toValuationSubring = HeightOneSpectrum.valuationSubringAtPrime F' P

theorem

restrict_placeOfPrime

L382 ↗

AlgebraicCurve.Place.restrict_placeOfPrime

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Bijection
variable {v : Place K F}

Lean source · statement

theorem restrict_placeOfPrime (P : HeightOneSpectrum (integralClosureAt F' v)) :
    (placeOfPrime P).restrict F = v

theorem

fiberCenter_placeOfPrime

L400 ↗

AlgebraicCurve.Place.fiberCenter_placeOfPrime

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Bijection
variable {v : Place K F}

Lean source · statement

theorem fiberCenter_placeOfPrime (P : HeightOneSpectrum (integralClosureAt F' v)) :
    fiberCenter F' v (restrict_placeOfPrime P) = P

theorem

eq_of_fiberCenter_eq

L412 ↗

AlgebraicCurve.Place.eq_of_fiberCenter_eq

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Bijection
variable {v : Place K F}

Lean source · statement

theorem eq_of_fiberCenter_eq {w w' : Place K F'} (hw : w.restrict F = v)
    (hw' : w'.restrict F = v)
    (h : fiberCenter F' v hw = fiberCenter F' v hw') : w = w'

def

fiberEquiv

L426 ↗

AlgebraicCurve.Place.fiberEquiv

Documentation

The correspondence between places restricting to the base place and integral-closure primes.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in

Lean source · full declaration

def fiberEquiv :
    {w : Place K F' // w.restrict F = v} ≃ HeightOneSpectrum (integralClosureAt F' v) where
  toFun w := fiberCenter F' v w.2
  invFun P := ⟨placeOfPrime P, restrict_placeOfPrime P⟩
  left_inv w := Subtype.ext (eq_of_fiberCenter_eq (restrict_placeOfPrime _) w.2
    (fiberCenter_placeOfPrime (fiberCenter F' v w.2)))
  right_inv P := fiberCenter_placeOfPrime P

theorem

fiberEquiv_apply

L434 ↗

AlgebraicCurve.Place.fiberEquiv_apply

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in

Lean source · statement

theorem fiberEquiv_apply (w : {w : Place K F' // w.restrict F = v}) :
    fiberEquiv F' v w = fiberCenter F' v w.2

theorem

fiberEquiv_symm_apply

L437 ↗

AlgebraicCurve.Place.fiberEquiv_symm_apply

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in

Lean source · statement

theorem fiberEquiv_symm_apply (P : HeightOneSpectrum (integralClosureAt F' v)) :
    ((fiberEquiv F' v).symm P : Place K F') = placeOfPrime P

theorem

finite_setOf_restrict_eq

L440 ↗

AlgebraicCurve.Place.finite_setOf_restrict_eq

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in

Lean source · statement

theorem finite_setOf_restrict_eq : {w : Place K F' | w.restrict F = v}.Finite

def

fiberOver

L455 ↗

AlgebraicCurve.Place.fiberOver

Documentation

The finite set of extending places whose restriction is the given base place.

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

def fiberOver : Finset (Place K F')

theorem

mem_fiberOver

L458 ↗

AlgebraicCurve.Place.mem_fiberOver

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

theorem mem_fiberOver {w : Place K F'} : w ∈ v.fiberOver F' ↔ w.restrict F = v

theorem

restrict_mem_fiberOver

L461 ↗

AlgebraicCurve.Place.restrict_mem_fiberOver

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

theorem restrict_mem_fiberOver (w : Place K F') : w ∈ (w.restrict F).fiberOver F'

theorem

restrict_eq_of_mem_fiberOver

L464 ↗

AlgebraicCurve.Place.restrict_eq_of_mem_fiberOver

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

theorem restrict_eq_of_mem_fiberOver {w : Place K F'} (hw : w ∈ v.fiberOver F') :
    w.restrict F = v

theorem

subset_fiberOver_of_forall_restrict_eq

L468 ↗

AlgebraicCurve.Place.subset_fiberOver_of_forall_restrict_eq

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

theorem subset_fiberOver_of_forall_restrict_eq {S : Finset (Place K F')}
    (hS : ∀ w ∈ S, w.restrict F = v) : S ⊆ v.fiberOver F'

theorem

card_fiberOver_eq

L472 ↗

AlgebraicCurve.Place.card_fiberOver_eq

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

theorem card_fiberOver_eq :
    (v.fiberOver F').card =
      (IsDedekindDomain.primesOverFinset (IsLocalRing.maximalIdeal v.toValuationSubring)
        (integralClosureAt F' v)).card

theorem

fiber_eq_fiberOver

L498 ↗

AlgebraicCurve.Place.fiber_eq_fiberOver

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (F') in
section Fiber
variable (v : Place K F)
variable (F') in
variable (F') in

Lean source · statement

theorem fiber_eq_fiberOver [HasPrincipalDivisors K F'] : v.fiber F' = v.fiberOver F'

Module documentation

OverDVR

Declarations