The sharp finite different bound for a plane curve

This file bounds the residue-weighted finite different of the plane function field by the discriminant degree of the original second-coordinate equation. The key local step chooses a reciprocal primitive element separately at each base prime; a prime-unit denominator-clearing argument then compares its minimal-polynomial discriminant with the global different.

theorem BGS.CorvajaZannier.adjoin_smul_eq_top_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (r : K) (hr : r ≠ 0) (z : L) (hz : K[z] = ⊤) : K[r • z] = ⊤

theorem BGS.CorvajaZannier.minpoly_discr_ne_zero_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (z : L) (hz : K[z] = ⊤) : (minpoly K z).discr ≠ 0

theorem BGS.CorvajaZannier.powerBasis_discr_smul_eq_diagonal_det_sq_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (r : K) (z : L) (pbz pbx : PowerBasis K L) (hgenZ : pbz.gen = z) (hgenX : pbx.gen = r • z) : Algebra.discr K ⇑pbx.basis = (Matrix.diagonal fun (i : Fin pbx.dim) => r ^ ↑i).det ^ 2 * Algebra.discr K ⇑pbz.basis

theorem BGS.CorvajaZannier.exists_minpoly_discr_smul_eq_pow_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (r : K) (hr : r ≠ 0) (z : L) (hz : K[z] = ⊤) : ∃ (N : ℕ), (minpoly K (r • z)).discr = r ^ N * (minpoly K z).discr

theorem BGS.CorvajaZannier.finitePlaceOrder_mul_of_ne_zero {R : Type u_1} {F : Type u_2} [CommRing R] [IsDedekindDomain R] [Field F] [Algebra R F] [IsFractionRing R F] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : F) (hx : x ≠ 0) (hy : y ≠ 0) : finitePlaceOrder v (x * y) = finitePlaceOrder v x + finitePlaceOrder v y

theorem BGS.CorvajaZannier.finitePlaceOrder_pow_of_ne_zero {R : Type u_1} {F : Type u_2} [CommRing R] [IsDedekindDomain R] [Field F] [Algebra R F] [IsFractionRing R F] (v : IsDedekindDomain.HeightOneSpectrum R) (x : F) (hx : x ≠ 0) (n : ℕ) : finitePlaceOrder v (x ^ n) = n • finitePlaceOrder v x

theorem BGS.CorvajaZannier.finitePlaceOrder_algebraMap_unit_eq_zero {R : Type u_1} {F : Type u_2} [CommRing R] [IsDedekindDomain R] [Field F] [Algebra R F] [IsFractionRing R F] (v : IsDedekindDomain.HeightOneSpectrum R) (u : Rˣ) : finitePlaceOrder v ((algebraMap R F) ↑u) = 0

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_discr_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : (planeCurvePolynomialInSecondCoordinate f).discr ≠ 0

The discriminant of the second-coordinate plane equation is nonzero under the separating-coordinate hypothesis.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.finiteDifferentBoundPolynomialAlgebra (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 plane curve finite different bound construction.

Equations

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

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

theorem BGS.CorvajaZannier.finiteDifferentBoundFiniteIntegralClosureModuleFinite (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.finiteDifferentBoundFiniteIntegralClosureIsIntegral (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.finiteDifferentBoundPolynomialTorsionFreeTop (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.finiteDifferentBoundFiniteIntegralClosureIsTorsionFree (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)

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteDifferentResidueWeightedDivisor (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) : FiniteExtensionFinitePlace K L →₀ ℕ

The finite different, weighted by residue degree but not yet by the degree of the base prime.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentResidueWeightedDivisor_apply (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (q : FiniteExtensionFinitePlace K L) : (finiteExtensionFiniteDifferentResidueWeightedDivisor K L hDifferent) q = multiplicity q.asIdeal (differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)) * q.asIdeal.inertiaDeg (Polynomial K)

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteDifferentDivisorBelow (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum (Polynomial K) →₀ ℕ

Push the residue-weighted finite different down to the finite primes of K[X].

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentDivisorBelow_apply (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : (finiteExtensionFiniteDifferentDivisorBelow K L hDifferent) p = ∑ P : ↑(p.asIdeal.primesOver ↥(RatFuncFiniteIntegralClosure K L)), (↑P).inertiaDeg (Polynomial K) * multiplicity (↑P) (differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L))

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentDegree_eq_belowWeightedDegree (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) : finiteExtensionFiniteDifferentDegree K L hDifferent = (finiteExtensionFiniteDifferentDivisorBelow K L hDifferent).sum fun (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) (e : ℕ) => e * ratFuncFinitePlaceDegree p

Pushing the residue-weighted different down to the base does not change its degree-weighted sum.

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentDegree_le_polynomialDegree_of_localBounds (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (Δ : Polynomial K) (hΔ : Δ ≠ 0) (hlocal : ∀ (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)), ↑((finiteExtensionFiniteDifferentDivisorBelow K L hDifferent) p) ≤ ratFuncFiniteOrder p ((algebraMap (Polynomial K) (RatFunc K)) Δ)) : finiteExtensionFiniteDifferentDegree K L hDifferent ≤ Δ.natDegree

A coefficientwise finite-place discriminant bound sums to the corresponding degree bound.

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentDivisorBelow_apply_le_minpolyDiscr_of_localPrimitive (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) [Algebra (Localization.AtPrime p.asIdeal) L] [IsScalarTower (Polynomial K) (Localization.AtPrime p.asIdeal) L] (z : L) (hzIntegral : IsIntegral (Localization.AtPrime p.asIdeal) z) (hzPrimitive : (RatFunc K)[z] = ⊤) : ↑((finiteExtensionFiniteDifferentDivisorBelow K L hDifferent) p) ≤ ratFuncFiniteOrder p (minpoly (RatFunc K) z).discr

theorem BGS.CorvajaZannier.planeCurve_finiteDifferentDivisorBelow_apply_le_discrOrder {K : Type u_1} [Field K] [Fintype K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : have hx := ⋯; ↑((finiteExtensionFiniteDifferentDivisorBelow K (PlaneCurveFunctionField f) ⋯) p) ≤ ratFuncFiniteOrder p ((algebraMap (Polynomial K) (RatFunc K)) (planeCurvePolynomialInSecondCoordinate f).discr)

At each finite first-coordinate prime, the residue-weighted different is bounded by the order of the discriminant of the original plane equation.

theorem BGS.CorvajaZannier.planeCurve_finiteDifferentDegree_le_discrNatDegree {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) : have hx := ⋯; finiteExtensionFiniteDifferentDegree K (PlaneCurveFunctionField f) ⋯ ≤ (planeCurvePolynomialInSecondCoordinate f).discr.natDegree

The sharp finite different contribution for the plane function field is bounded by the discriminant degree of the original second-coordinate equation.