NYLL
Module

InseparableCounting.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.InseparableCounting
17 declarations indexed from sourceView source ↗

Module documentation

Reducing prime-divisor counts to the separable subextension

The normalization-finiteness theorem used in the separable proofs of Fried--Jarden 6.2.2(b),(d) need only be applied to the maximal separable subextension. A valuation subring of the full field is determined by its restriction to that subextension, because the remaining extension is purely inseparable.

This file first proves the corresponding general counting theorem for FiniteDivisorOver. Unlike the earlier fraction-field theorem, the ambient field may now be a purely inseparable extension of the fraction field of the Dedekind model.

Imports2
Imported by1

Declarations

def

FiniteOn

L41 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.FiniteOn
Documentation

A valuation subring contains the image of the chosen model.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
def FiniteOn (A : ValuationSubring M) : Prop
def

finiteRingHom

L45 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.finiteRingHom
Documentation

The model map factored through a valuation subring.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · full declaration
def finiteRingHom (A : ValuationSubring M)
    (hfinite : FiniteOn (S := S) A) :
    S →+* A where
  toFun s := ⟨algebraMap S M s, hfinite s⟩
  map_zero' := Subtype.ext (map_zero (algebraMap S M))
  map_one' := Subtype.ext (map_one (algebraMap S M))
  map_add' x y := Subtype.ext (map_add (algebraMap S M) x y)
  map_mul' x y := Subtype.ext (map_mul (algebraMap S M) x y)
def

center

L55 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.center
Documentation

The center of a valuation subring on a model it contains.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
def center (A : ValuationSubring M)
    (hfinite : FiniteOn (S := S) A) : Ideal S
theorem

mem_center_iff_mem_nonunits

L60 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.mem_center_iff_mem_nonunits
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
theorem mem_center_iff_mem_nonunits
    (A : ValuationSubring M) (hfinite : FiniteOn (S := S) A) (s : S) :
    s ∈ center (S := S) A hfinite ↔
      algebraMap S M s ∈ A.nonunits
theorem

center_isPrime

L70 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.center_isPrime
Documentation

The center on any contained model is prime.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
theorem center_isPrime
    (A : ValuationSubring M) (hfinite : FiniteOn (S := S) A) :
    (center (S := S) A hfinite).IsPrime
theorem

center_ne_bot

L81 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.center_ne_bot
Documentation

The center of a proper valuation subring on a model with fraction field M is nonzero.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
theorem center_ne_bot
    [IsDomain S] [IsFractionRing S M]
    (A : ValuationSubring M) (hfinite : FiniteOn (S := S) A)
    (hproper : A ≠ ⊤) :
    center (S := S) A hfinite ≠ ⊥
def

centerHeightOneSpectrum

L115 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.centerHeightOneSpectrum
Documentation

The height-one center on a Dedekind model.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
def centerHeightOneSpectrum
    [IsDedekindDomain S] [IsFractionRing S M]
    (A : ValuationSubring M) (hfinite : FiniteOn (S := S) A)
    (hproper : A ≠ ⊤) :
    IsDedekindDomain.HeightOneSpectrum S
theorem

valuationSubringAtCenter_le

L127 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.valuationSubringAtCenter_le
Documentation

The canonical localization at the center is contained in the valuation subring.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
theorem valuationSubringAtCenter_le
    [IsDedekindDomain S] [IsFractionRing S M]
    (A : ValuationSubring M) (hfinite : FiniteOn (S := S) A)
    (hproper : A ≠ ⊤) :
    IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime M
        (centerHeightOneSpectrum A hfinite hproper) ≤ A
theorem

valuationSubringAtCenter_eq

L150 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.valuationSubringAtCenter_eq
Documentation

A proper valuation subring containing a Dedekind model is the canonical localization at its center.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
theorem valuationSubringAtCenter_eq
    [IsDedekindDomain S] [IsFractionRing S M]
    (A : ValuationSubring M) (hfinite : FiniteOn (S := S) A)
    (hproper : A ≠ ⊤) :
    IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime M
        (centerHeightOneSpectrum A hfinite hproper) = A
theorem

eq_of_center_eq

L163 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.ValuationCenter.eq_of_center_eq
Documentation

Proper valuation subrings containing a Dedekind model are determined by their centers, without assuming a DVR structure on the restrictions.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
namespace ValuationCenter
variable {S : Type uS} {M : Type uM}
  [CommRing S] [Field M] [Algebra S M]
Lean source · statement
theorem eq_of_center_eq
    [IsDedekindDomain S] [IsFractionRing S M]
    (A B : ValuationSubring M)
    (hfiniteA : FiniteOn (S := S) A)
    (hfiniteB : FiniteOn (S := S) B)
    (hproperA : A ≠ ⊤) (hproperB : B ≠ ⊤)
    (hcenter :
      center (S := S) A hfiniteA =
        center (S := S) B hfiniteB) :
    A = B
theorem

mem_comap_nonunits_iff

L193 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.mem_comap_nonunits_iff
Documentation

Nonunits are preserved and reflected by restriction to a subfield.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
Lean source · statement
theorem mem_comap_nonunits_iff
    {M : Type uM} {F : Type uF} [Field M] [Field F]
    (A : ValuationSubring F) (ι : M →+* F) (x : M) :
    x ∈ (A.comap ι).nonunits ↔ ι x ∈ A.nonunits
def

restrictedValuationSubring

L214 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.restrictedValuationSubring
Documentation

Restrict the valuation subring underlying a divisor to M.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
section PurelyInseparableFractionField
variable {K : Type uK} {R : Type uR} {S : Type uS}
  {M : Type uM} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field M] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
  [Algebra S M] [Algebra M F] [IsScalarTower S M F]
  [IsDedekindDomain S] [IsFractionRing S M]
  [IsPurelyInseparable M F]
open PrimeDivisorCounting
Lean source · statement
def restrictedValuationSubring
    {p : Ideal R}
    (v : FiniteDivisorOver (K := K) (S := S) (F := F) p) :
    ValuationSubring M
theorem

restrictedValuationSubring_finite

L222 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.restrictedValuationSubring_finite
Documentation

The restricted valuation subring still contains the Dedekind model.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
section PurelyInseparableFractionField
variable {K : Type uK} {R : Type uR} {S : Type uS}
  {M : Type uM} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field M] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
  [Algebra S M] [Algebra M F] [IsScalarTower S M F]
  [IsDedekindDomain S] [IsFractionRing S M]
  [IsPurelyInseparable M F]
open PrimeDivisorCounting
omit [IsDedekindDomain S] [IsFractionRing S M] [IsPurelyInseparable M F] in
Lean source · statement
theorem restrictedValuationSubring_finite
    {p : Ideal R}
    (v : FiniteDivisorOver (K := K) (S := S) (F := F) p) :
    ValuationCenter.FiniteOn (S := S)
      (restrictedValuationSubring (M := M) v)
theorem

restrictedValuationSubring_ne_top

L239 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.restrictedValuationSubring_ne_top
Documentation

The restriction is proper. Otherwise pure-inseparable injectivity would force the original prime-divisor valuation subring to be the whole field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
section PurelyInseparableFractionField
variable {K : Type uK} {R : Type uR} {S : Type uS}
  {M : Type uM} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field M] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
  [Algebra S M] [Algebra M F] [IsScalarTower S M F]
  [IsDedekindDomain S] [IsFractionRing S M]
  [IsPurelyInseparable M F]
open PrimeDivisorCounting
omit [Algebra S M] [IsScalarTower S M F] [IsDedekindDomain S] [IsFractionRing S M] in
Lean source · statement
theorem restrictedValuationSubring_ne_top
    {p : Ideal R}
    (v : FiniteDivisorOver (K := K) (S := S) (F := F) p) :
    restrictedValuationSubring (M := M) v ≠ ⊤
theorem

restrictedValuationSubring_center_eq

L260 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.restrictedValuationSubring_center_eq
Documentation

The center is unchanged after restricting the valuation to M.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
section PurelyInseparableFractionField
variable {K : Type uK} {R : Type uR} {S : Type uS}
  {M : Type uM} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field M] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
  [Algebra S M] [Algebra M F] [IsScalarTower S M F]
  [IsDedekindDomain S] [IsFractionRing S M]
  [IsPurelyInseparable M F]
open PrimeDivisorCounting
omit [IsDedekindDomain S] [IsFractionRing S M] [IsPurelyInseparable M F] in
Lean source · statement
theorem restrictedValuationSubring_center_eq
    {p : Ideal R}
    (v : FiniteDivisorOver (K := K) (S := S) (F := F) p) :
    ValuationCenter.center
        (restrictedValuationSubring (M := M) v)
        (restrictedValuationSubring_finite (M := M) v) =
      v.divisor.centerAlong (IsScalarTower.toAlgHom K S F) v.finite
theorem

centerMap_injective_of_isPurelyInseparable

L282 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.centerMap_injective_of_isPurelyInseparable
Documentation

The existing center map remains injective when the ambient field is a purely inseparable extension of the fraction field of the Dedekind model.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
section PurelyInseparableFractionField
variable {K : Type uK} {R : Type uR} {S : Type uS}
  {M : Type uM} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field M] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
  [Algebra S M] [Algebra M F] [IsScalarTower S M F]
  [IsDedekindDomain S] [IsFractionRing S M]
  [IsPurelyInseparable M F]
open PrimeDivisorCounting
Lean source · statement
theorem centerMap_injective_of_isPurelyInseparable
    (M : Type uM) [Field M] [Algebra S M] [Algebra M F]
    [IsScalarTower S M F] [IsFractionRing S M]
    [IsPurelyInseparable M F] {p : Ideal R} :
    Function.Injective
      (FiniteDivisorOver.centerMap :
        FiniteDivisorOver (K := K) (S := S) (F := F) p →
          p.primesOver S)
theorem

card_finiteDivisorOver_le_finrank_of_isPurelyInseparable

L314 ↗
FieldArithmetic.Chapter06.InseparablePrimeDivisorReduction.card_finiteDivisorOver_le_finrank_of_isPurelyInseparable
Documentation

Prime-divisor counting over a finite Dedekind model is unchanged after a purely inseparable extension of its fraction field.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace InseparablePrimeDivisorReduction
open IsLocalRing
universe uK uR uS uM uF
section PurelyInseparableFractionField
variable {K : Type uK} {R : Type uR} {S : Type uS}
  {M : Type uM} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field M] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
  [Algebra S M] [Algebra M F] [IsScalarTower S M F]
  [IsDedekindDomain S] [IsFractionRing S M]
  [IsPurelyInseparable M F]
open PrimeDivisorCounting
Lean source · statement
theorem card_finiteDivisorOver_le_finrank_of_isPurelyInseparable
    [IsDomain R] [Module.Finite R S] [Module.Flat R S]
    (M : Type uM) [Field M] [Algebra S M] [Algebra M F]
    [IsScalarTower S M F] [IsFractionRing S M]
    [IsPurelyInseparable M F]
    (p : Ideal R) [p.IsPrime] :
    Nat.card (FiniteDivisorOver (K := K) (S := S) (F := F) p) ≤
      Module.finrank R S

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.