The degree of the different at infinity

Bound the different at infinity using a primitive element, its discriminant, and the normalized reciprocal polynomial.

theorem BGS.CorvajaZannier.discr_powerBasis_eq_minpoly_discr {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (pb : PowerBasis K L) : Algebra.discr K ⇑pb.basis = (minpoly K pb.gen).discr

theorem BGS.CorvajaZannier.infinityDifferentIntegralClosureModuleFinite (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.infinityDifferentIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityDifferentTopIsTorsionFree (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.IsTorsionFree (↥(RatFuncInfinityIntegers K)) L

theorem BGS.CorvajaZannier.infinityDifferentIntegralClosureIsTorsionFree (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.IsTorsionFree ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityDifferentIntegralClosureIsDedekindDomain (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.infinityDifferentIntegralClosureIsFractionRing (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

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.infinityDifferentPlaceFintype (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] : Fintype ↑((ratFuncInfinityPlace K).asIdeal.primesOver ↥(RatFuncInfinityIntegralClosure K L))

A finite enumeration of ((ratFuncInfinityPlace K).asIdeal.primesOver (RatFuncInfinityIntegralClosure K L)) used in the plane curve infinity different degree construction.

Equations

• BGS.CorvajaZannier.infinityDifferentPlaceFintype K L = ⋯.fintype

noncomputable def BGS.CorvajaZannier.infinityDifferentDegree (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] : ℕ

The residue-degree-weighted multiplicity of the different above the infinity place of K(X).

Equations

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

theorem BGS.CorvajaZannier.ratFuncInfinityIntegralClosureFractionRingEquiv_valuation (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] (q : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncInfinityIntegralClosure K L)) (x : FractionRing ↥(RatFuncInfinityIntegralClosure K L)) : (IsDedekindDomain.HeightOneSpectrum.valuation L q) ((ratFuncInfinityIntegralClosureFractionRingEquiv K L) x) = (IsDedekindDomain.HeightOneSpectrum.valuation (FractionRing ↥(RatFuncInfinityIntegralClosure K L)) q) x

theorem BGS.CorvajaZannier.ratFuncInfinityIntegralClosureFractionRingEquiv_order_eq (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] (q : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncInfinityIntegralClosure K L)) (x : FractionRing ↥(RatFuncInfinityIntegralClosure K L)) (hx : x ≠ 0) : finitePlaceOrder q x = finitePlaceOrder q ((ratFuncInfinityIntegralClosureFractionRingEquiv K L) x)

theorem BGS.CorvajaZannier.infinityDifferentDegree_le_discriminantOrder_of_primitiveElement (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] (G : Polynomial ↥(RatFuncInfinityIntegers K)) (c : ↥(RatFuncInfinityIntegers K)) (u : (↥(RatFuncInfinityIntegers K))ˣ) (v : L) (hu : Polynomial.eval c G = ↑u) (hvc : v ≠ (algebraMap (↥(RatFuncInfinityIntegers K)) L) c) (hv : (Polynomial.aeval v) G = 0) (hprimitive : (RatFunc K)[v] = ⊤) (hdegree : G.natDegree = Module.finrank (RatFunc K) L) (hGdiscr : G.discr ≠ 0) : ↑(infinityDifferentDegree K L) ≤ ratFuncInfinityOrder ((algebraMap (↥(RatFuncInfinityIntegers K)) (RatFunc K)) G.discr)

The different contribution above infinity is bounded by the infinity order of the discriminant of any integral primitive-element equation having a unit value at a center. The inverse translate of the primitive element is integral and realizes the complementary reciprocal-discriminant estimate.

theorem BGS.CorvajaZannier.infinityNormalizedCoefficient_isUnit_of_natDegree_eq (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (P : Polynomial K) (hP : P ≠ 0) (hdegree : P.natDegree = a) : IsUnit (infinityNormalizedCoefficient K a P ⋯)

theorem BGS.CorvajaZannier.infinityNormalizedIntegralPolynomial_isPrimitive (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (F : Polynomial (Polynomial K)) (hcoeff : ∀ (i : ℕ), (F.coeff i).natDegree ≤ a) (i : ℕ) (hFi : F.coeff i ≠ 0) (hi : (F.coeff i).natDegree = a) : (infinityNormalizedIntegralPolynomial K a F hcoeff).IsPrimitive