Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.FiniteExtensionProductFormula

Finite-extension norm and place-count formula #

For a finite torsion-free extension of Dedekind domains, this file identifies the exponent of the relative norm of an integral ideal at a height-one prime with the inertia-degree-weighted sum of the ideal's exponents at all primes above it. The principal-integral specialization gives the corresponding formula for Algebra.intNorm.

This is the finite-place norm bridge needed to pass from the rational-function field product formula to a finite function-field extension. The final theorem clears a denominator to extend the identity to arbitrary elements of the fraction field. Places at infinity are treated separately.

source
def BGS.CorvajaZannier.primeOverHeightOne {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] [Algebra R S] [Module.IsTorsionFree R S] (p : IsDedekindDomain.HeightOneSpectrum R) (P : ↑(p.asIdeal.primesOver S)) :
IsDedekindDomain.HeightOneSpectrum S

A prime of S over a height-one prime of R, regarded as a height-one prime of S.

Equations
Instances For
    source
    @[simp]
    theorem BGS.CorvajaZannier.primeOverHeightOne_asIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] [Algebra R S] [Module.IsTorsionFree R S] (p : IsDedekindDomain.HeightOneSpectrum R) (P : ↑(p.asIdeal.primesOver S)) :
    (primeOverHeightOne p P).asIdeal = ↑P
    source
    theorem BGS.CorvajaZannier.relativeNormFractionRingFiniteDimensional {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] :
    FiniteDimensional (FractionRing R) (FractionRing S)
    source
    theorem BGS.CorvajaZannier.count_relNorm_eq_sum_inertiaDeg_mul_count {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (p : IsDedekindDomain.HeightOneSpectrum R) [Fintype ↑(p.asIdeal.primesOver S)] (I : Ideal S) :
    FractionalIdeal.count (FractionRing R) p ↑((Ideal.relNorm R) I) = ∑ P : ↑(p.asIdeal.primesOver S), ↑((↑P).inertiaDeg R) * FractionalIdeal.count (FractionRing S) (primeOverHeightOne p P) ↑I

    The finite-prime exponent of the relative norm of an integral ideal is the residue-degree-weighted sum of its exponents at primes above it.

    source
    theorem BGS.CorvajaZannier.count_spanSingleton_intNorm_eq_sum_inertiaDeg_mul_count {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (p : IsDedekindDomain.HeightOneSpectrum R) [Fintype ↑(p.asIdeal.primesOver S)] (x : S) :
    FractionalIdeal.count (FractionRing R) p ((FractionalIdeal.spanSingleton (nonZeroDivisors R)) ((algebraMap R (FractionRing R)) ((Algebra.intNorm R S) x))) = ∑ P : ↑(p.asIdeal.primesOver S), ↑((↑P).inertiaDeg R) * FractionalIdeal.count (FractionRing S) (primeOverHeightOne p P) ((FractionalIdeal.spanSingleton (nonZeroDivisors S)) ((algebraMap S (FractionRing S)) x))

    For an integral element, the finite-place order of its integral norm is the residue-degree-weighted sum of the principal orders above the place.

    source
    theorem BGS.CorvajaZannier.count_spanSingleton_norm_algebraMap_eq_sum_inertiaDeg_mul_count {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (p : IsDedekindDomain.HeightOneSpectrum R) [Fintype ↑(p.asIdeal.primesOver S)] (x : S) :
    FractionalIdeal.count (FractionRing R) p ((FractionalIdeal.spanSingleton (nonZeroDivisors R)) ((Algebra.norm (FractionRing R)) ((algebraMap S (FractionRing S)) x))) = ∑ P : ↑(p.asIdeal.primesOver S), ↑((↑P).inertiaDeg R) * FractionalIdeal.count (FractionRing S) (primeOverHeightOne p P) ((FractionalIdeal.spanSingleton (nonZeroDivisors S)) ((algebraMap S (FractionRing S)) x))

    The same principal-integral identity with the field norm written explicitly in the fraction fields.

    source
    theorem BGS.CorvajaZannier.count_spanSingleton_norm_eq_sum_inertiaDeg_mul_count {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (p : IsDedekindDomain.HeightOneSpectrum R) [Fintype ↑(p.asIdeal.primesOver S)] (x : FractionRing S) :
    FractionalIdeal.count (FractionRing R) p ((FractionalIdeal.spanSingleton (nonZeroDivisors R)) ((Algebra.norm (FractionRing R)) x)) = ∑ P : ↑(p.asIdeal.primesOver S), ↑((↑P).inertiaDeg R) * FractionalIdeal.count (FractionRing S) (primeOverHeightOne p P) ((FractionalIdeal.spanSingleton (nonZeroDivisors S)) x)

    For an arbitrary fraction-field element, the finite-place order of its field norm is the residue-degree-weighted sum of its principal orders at the places above the given base place.