Module

Counting.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Counting

6 declarations indexed from sourceView source ↗

Module documentation

Counting prime divisors over a base prime

A prime divisor finite on a Dedekind model has a nonzero prime center, and that center determines the divisor. Thus prime divisors whose centers lie over a fixed base prime inject into the set of primes over that base prime. The ramification--inertia count then bounds their number by the module rank.

Imports2

Imported by3

structure

FiniteDivisorOver

L39 ↗

FieldArithmetic.Chapter06.PrimeDivisorCounting.FiniteDivisorOver

Documentation

A prime divisor finite on the model S whose center contracts to p.

The equality stored in center_liesOver is the defining property of the collection being counted, rather than an auxiliary theorem used to force a later proof.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorCounting
universe uK uR uS uF
variable {K : Type uK} {R : Type uR} {S : Type uS} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]

Lean source · full declaration

structure FiniteDivisorOver (p : Ideal R) where
  /-- The underlying prime divisor of the function field. -/
  divisor : FunctionFieldPrimeDivisor K F
  /-- The prime divisor is finite along the chosen map from the model S. -/
  finite :
    divisor.FiniteAlong (IsScalarTower.toAlgHom K S F)
  /-- The center on S contracts to the ideal p of R. -/
  center_liesOver :
    p =
      (divisor.centerAlong (IsScalarTower.toAlgHom K S F) finite).under R

theorem

ext

L56 ↗

FieldArithmetic.Chapter06.PrimeDivisorCounting.FiniteDivisorOver.ext

Documentation

Equality of the underlying prime divisors determines bundled elements.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorCounting
universe uK uR uS uF
variable {K : Type uK} {R : Type uR} {S : Type uS} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
namespace FiniteDivisorOver
variable {p : Ideal R}

Lean source · statement

theorem ext
    {v₁ v₂ : FiniteDivisorOver (K := K) (S := S) (F := F) p}
    (h : v₁.divisor = v₂.divisor) :
    v₁ = v₂

def

centerMap

L67 ↗

FieldArithmetic.Chapter06.PrimeDivisorCounting.FiniteDivisorOver.centerMap

Documentation

The center as an element of the set of primes of S above p.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorCounting
universe uK uR uS uF
variable {K : Type uK} {R : Type uR} {S : Type uS} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
namespace FiniteDivisorOver
variable {p : Ideal R}

Lean source · statement

def centerMap
    (v : FiniteDivisorOver (K := K) (S := S) (F := F) p) :
    p.primesOver S

theorem

centerMap_val

L76 ↗

FieldArithmetic.Chapter06.PrimeDivisorCounting.FiniteDivisorOver.centerMap_val

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorCounting
universe uK uR uS uF
variable {K : Type uK} {R : Type uR} {S : Type uS} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
namespace FiniteDivisorOver
variable {p : Ideal R}

Lean source · statement

theorem centerMap_val
    (v : FiniteDivisorOver (K := K) (S := S) (F := F) p) :
    (v.centerMap : Ideal S) =
      v.divisor.centerAlong (IsScalarTower.toAlgHom K S F) v.finite

theorem

centerMap_injective

L85 ↗

FieldArithmetic.Chapter06.PrimeDivisorCounting.FiniteDivisorOver.centerMap_injective

Documentation

For a Dedekind model inside its fraction field, the center map is injective.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorCounting
universe uK uR uS uF
variable {K : Type uK} {R : Type uR} {S : Type uS} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]
namespace FiniteDivisorOver
variable {p : Ideal R}

Lean source · statement

theorem centerMap_injective
    [IsDedekindDomain S] [IsFractionRing S F] :
    Function.Injective
      (centerMap :
        FiniteDivisorOver (K := K) (S := S) (F := F) p →
          p.primesOver S)

theorem

card_finiteDivisorOver_le_finrank

L103 ↗

FieldArithmetic.Chapter06.PrimeDivisorCounting.card_finiteDivisorOver_le_finrank

Documentation

The number of prime divisors finite on S and centered over p is at most the rank of the finite flat extension S / R.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorCounting
universe uK uR uS uF
variable {K : Type uK} {R : Type uR} {S : Type uS} {F : Type uF}
  [Field K] [CommRing R] [CommRing S] [Field F]
  [Algebra R S] [Algebra K S] [Algebra K F] [Algebra S F]
  [IsScalarTower K S F]

Lean source · statement

theorem card_finiteDivisorOver_le_finrank
    [IsDomain R] [IsDedekindDomain S] [IsFractionRing S F]
    [Module.Finite R S] [Module.Flat R S]
    (p : Ideal R) [p.IsPrime] :
    Nat.card (FiniteDivisorOver (K := K) (S := S) (F := F) p) ≤
      Module.finrank R S

Module documentation

Counting prime divisors over a base prime

Declarations

FiniteDivisorOver

ext

centerMap

centerMap_val

centerMap_injective

card_finiteDivisorOver_le_finrank