Exhaustive product formula in a finite extension of K(X)

This file combines the norm/count formula at every finite polynomial place with the corresponding formula at infinity. An element of a finite separable extension is transported to the canonical fraction fields of the two integral closures. Naturality of the field norm shows that both models compute the same norm in K(X).

The final theorem sums the residue-degree-weighted orders at every prime above every finite place, with the finite-place degree factor, and at every prime above infinity. The total is zero.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.polynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension exhaustive product formula construction.

Equations

• BGS.CorvajaZannier.polynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.polynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.RatFuncFiniteIntegralClosure (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Subalgebra (Polynomial K) L

The integral closure of the polynomial ring inside the finite extension.

Equations

• BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L = FunctionField.ringOfIntegers K L

noncomputable def BGS.CorvajaZannier.ratFuncFiniteFractionRingEquiv (K : Type u_1) [Field K] : FractionRing (Polynomial K) ≃ₐ[Polynomial K] RatFunc K

The equivalence between the fraction field of polynomials and rational functions.

Equations

• BGS.CorvajaZannier.ratFuncFiniteFractionRingEquiv K = FractionRing.algEquiv (Polynomial K) (RatFunc K)

theorem BGS.CorvajaZannier.ratFuncFiniteFractionRingEquiv_valuation (K : Type u_1) [Field K] (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) (x : FractionRing (Polynomial K)) : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) v) ((ratFuncFiniteFractionRingEquiv K) x) = (IsDedekindDomain.HeightOneSpectrum.valuation (FractionRing (Polynomial K)) v) x

theorem BGS.CorvajaZannier.ratFuncFiniteFractionRing_order_eq (K : Type u_1) [Field K] (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) (x : FractionRing (Polynomial K)) (hx : x ≠ 0) : finitePlaceOrder v x = ratFuncFiniteOrder v ((ratFuncFiniteFractionRingEquiv K) x)

noncomputable def BGS.CorvajaZannier.ratFuncFiniteIntegralClosureFractionRingEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : FractionRing ↥(RatFuncFiniteIntegralClosure K L) ≃ₐ[↥(RatFuncFiniteIntegralClosure K L)] L

The equivalence between the fraction field of the finite integral closure and the extension field.

Equations

• BGS.CorvajaZannier.ratFuncFiniteIntegralClosureFractionRingEquiv K L = FractionRing.algEquiv (↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)) L

theorem BGS.CorvajaZannier.finiteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.finiteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.polynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.CorvajaZannier.finiteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.finiteBaseFaithfulSMulExtensionFractionRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FaithfulSMul (Polynomial K) (FractionRing ↥(RatFuncFiniteIntegralClosure K L))

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.finiteFractionRingAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (FractionRing (Polynomial K)) (FractionRing ↥(RatFuncFiniteIntegralClosure K L))

The algebra structure from (FractionRing K[X]) to (FractionRing (RatFuncFiniteIntegralClosure K L)) used in the finite extension exhaustive product formula construction.

Equations

• BGS.CorvajaZannier.finiteFractionRingAlgebra K L = FractionRing.liftAlgebra (Polynomial K) (FractionRing ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L))

theorem BGS.CorvajaZannier.finiteFractionRingSeparable (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Algebra.IsSeparable (FractionRing (Polynomial K)) (FractionRing ↥(RatFuncFiniteIntegralClosure K L))

theorem BGS.CorvajaZannier.infinityIntegralClosureModuleFinite' (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityIntegralClosureIsDedekindDomain' (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityIntegralClosureIsFractionRing' (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncInfinityIntegralClosure K L)) L

noncomputable def BGS.CorvajaZannier.ratFuncInfinityIntegralClosureFractionRingEquiv (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : FractionRing ↥(RatFuncInfinityIntegralClosure K L) ≃ₐ[↥(RatFuncInfinityIntegralClosure K L)] L

The equivalence between the fraction field of the infinity integral closure and the extension field.

Equations

• BGS.CorvajaZannier.ratFuncInfinityIntegralClosureFractionRingEquiv K L = FractionRing.algEquiv (↥(BGS.CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

theorem BGS.CorvajaZannier.infinityBaseFaithfulSMulExtensionFractionRing' (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FaithfulSMul (↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.infinityFractionRingAlgebra' (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (FractionRing ↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

The algebra structure from (FractionRing (RatFuncInfinityIntegers K)) to (FractionRing (RatFuncInfinityIntegralClosure K L)) used in the finite extension exhaustive product formula construction.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.CorvajaZannier.infinityFractionRingSeparable' (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Algebra.IsSeparable (FractionRing ↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

theorem BGS.CorvajaZannier.ratFuncFinite_norm_transport (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] (x : L) : (ratFuncFiniteFractionRingEquiv K) ((Algebra.norm (FractionRing (Polynomial K))) ((ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x)) = (Algebra.norm (RatFunc K)) x

theorem BGS.CorvajaZannier.ratFuncInfinity_norm_transport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] (x : L) : (ratFuncInfinityFractionRingEquiv K) ((Algebra.norm (FractionRing ↥(RatFuncInfinityIntegers K))) ((ratFuncInfinityIntegralClosureFractionRingEquiv K L).symm x)) = (Algebra.norm (RatFunc K)) x

theorem BGS.CorvajaZannier.finitePrimesAbove_weightedOrder_eq_normOrder (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) (x : L) (hx : x ≠ 0) : ∑ P : ↑(p.asIdeal.primesOver ↥(RatFuncFiniteIntegralClosure K L)), ↑((↑P).inertiaDeg (Polynomial K)) * finitePlaceOrder (primeOverHeightOne p P) ((ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x) = ratFuncFiniteOrder p ((Algebra.norm (RatFunc K)) x)

theorem BGS.CorvajaZannier.primesAboveInfinity_weightedOrder_eq_normInfinityOrder (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : ∑ P : ↑((ratFuncInfinityPlace K).asIdeal.primesOver ↥(RatFuncInfinityIntegralClosure K L)), ↑((↑P).inertiaDeg ↥(RatFuncInfinityIntegers K)) * finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) ((ratFuncInfinityIntegralClosureFractionRingEquiv K L).symm x) = ratFuncInfinityOrder ((Algebra.norm (RatFunc K)) x)

noncomputable def BGS.CorvajaZannier.finiteExtensionFinitePlaceDegreeSum (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℤ

The exhaustive finite-place contribution in L, grouped by the finite places of K(X) supporting the divisor of the norm.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityOrderSum (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℤ

The contribution of all primes of L above the place at infinity.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceDegreeSum_eq_normFinitePlaceDegreeSum (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionFinitePlaceDegreeSum K L x = ratFuncExhaustiveFinitePlaceDegreeSum ((Algebra.norm (RatFunc K)) x)

theorem BGS.CorvajaZannier.finiteExtensionInfinityOrderSum_eq_normInfinityOrder (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionInfinityOrderSum K L x = ratFuncInfinityOrder ((Algebra.norm (RatFunc K)) x)

theorem BGS.CorvajaZannier.finiteExtension_exhaustivePrincipalDivisor_productFormula (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionFinitePlaceDegreeSum K L x + finiteExtensionInfinityOrderSum K L x = 0

The exhaustive weighted principal-divisor product formula in a finite separable extension L / K(X). Every finite prime is grouped under its base finite place and weighted by residue degree times the degree of that base place; the second sum contains every prime above infinity.