The canonical different divisor of a finite function-field extension

For a finite separable extension L / K(X), this module packages the local correction divisor of the differential dX. Its coefficient is the different exponent at a finite place and different exponent - 2 * ramification index above infinity. The weighted degree is therefore the total different degree minus twice the extension degree.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.canonicalDifferentPolynomialAlgebra (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 canonical different divisor construction.

Equations

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

theorem BGS.CorvajaZannier.canonicalDifferentPolynomialScalarTower (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.canonicalDifferentFiniteIntegralClosureModuleFinite (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.canonicalDifferentFiniteIntegralClosureIsIntegral (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.canonicalDifferentPolynomialTorsionFreeTop (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.canonicalDifferentFiniteIntegralClosureIsTorsionFree (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.canonicalDifferentFiniteBaseFaithfulSmulFractionRing (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.canonicalDifferentFiniteFractionRingAlgebra (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 canonical different divisor construction.

Equations

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

theorem BGS.CorvajaZannier.canonicalDifferentFiniteFractionRingSeparable (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.canonicalDifferentInfinityIntegralClosureModuleFinite (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.canonicalDifferentInfinityIntegralClosureIsIntegral (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.canonicalDifferentInfinityTorsionFreeTop (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.canonicalDifferentInfinityIntegralClosureIsTorsionFree (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.canonicalDifferentInfinityIntegralClosureIsDedekindDomain (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.canonicalDifferentInfinityIntegralClosureIsFractionRing (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.canonicalDifferentInfinityPlaceFintype (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 ↑(FiniteExtensionInfinityPlace K L)

A finite enumeration of (FiniteExtensionInfinityPlace K L) used in the finite extension canonical different divisor construction.

Equations

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

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteDifferentDivisor (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-place part of the different divisor, with integer coefficients.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentDivisor_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) : (finiteExtensionFiniteDifferentDivisor K L hDifferent) q = ↑(multiplicity q.asIdeal (differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)))

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityCanonicalDifferentDivisor (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] : ↑(FiniteExtensionInfinityPlace K L) →₀ ℤ

Above infinity, the canonical correction is the different exponent minus twice the ramification index over the parameter X⁻¹.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionInfinityCanonicalDifferentDivisor_apply (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] (P : ↑(FiniteExtensionInfinityPlace K L)) : (finiteExtensionInfinityCanonicalDifferentDivisor K L) P = ↑(multiplicity (↑P) (differentIdeal ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L))) - 2 * ↑((↑P).ramificationIdx ↥(RatFuncInfinityIntegers K))

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

The exhaustive canonical divisor attached to dX: the finite different at finite places and different - 2e above infinity.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionCanonicalDifferentDivisor_inl (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (q : FiniteExtensionFinitePlace K L) : (finiteExtensionCanonicalDifferentDivisor K L hDifferent) (Sum.inl q) = ↑(multiplicity q.asIdeal (differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)))

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionCanonicalDifferentDivisor_inr (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (P : ↑(FiniteExtensionInfinityPlace K L)) : (finiteExtensionCanonicalDifferentDivisor K L hDifferent) (Sum.inr P) = ↑(multiplicity (↑P) (differentIdeal ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L))) - 2 * ↑((↑P).ramificationIdx ↥(RatFuncInfinityIntegers K))

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteDifferentDegree (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) ≠ ⊥) : ℕ

Residue- and base-place-degree weighted finite different degree.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionInfinity_sum_ramification_inertia_eq_finrank (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] : ∑ P : ↑(FiniteExtensionInfinityPlace K L), (↑P).ramificationIdx ↥(RatFuncInfinityIntegers K) * (↑P).inertiaDeg ↥(RatFuncInfinityIntegers K) = Module.finrank (RatFunc K) L

theorem BGS.CorvajaZannier.finiteExtensionFiniteDifferentIdeal_ne_bot (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] : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥

The finite different is nonzero in the separable extension model.

theorem BGS.CorvajaZannier.finiteExtensionCanonicalDifferentDivisor_degree_of_ramification_sum (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] (hDifferent : differentIdeal (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ≠ ⊥) (hRamification : ∑ P : ↑(FiniteExtensionInfinityPlace K L), (↑P).ramificationIdx ↥(RatFuncInfinityIntegers K) * (↑P).inertiaDeg ↥(RatFuncInfinityIntegers K) = Module.finrank (RatFunc K) L) : finiteExtensionDivisorDegree K L (finiteExtensionCanonicalDifferentDivisor K L hDifferent) = ↑(finiteExtensionFiniteDifferentDegree K L hDifferent) + ↑(infinityDifferentDegree K L) - 2 * ↑(Module.finrank (RatFunc K) L)

Degree formula for the canonical different divisor, given the standard ramification-inertia sum above infinity.

theorem BGS.CorvajaZannier.finiteExtensionCanonicalDifferentDivisor_degree (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] : finiteExtensionDivisorDegree K L (finiteExtensionCanonicalDifferentDivisor K L ⋯) = ↑(finiteExtensionFiniteDifferentDegree K L ⋯) + ↑(infinityDifferentDegree K L) - 2 * ↑(Module.finrank (RatFunc K) L)

The canonical different divisor has weighted degree equal to the finite different degree plus the infinity different degree minus twice [L : K(X)].

theorem BGS.CorvajaZannier.finiteExtensionCanonicalDifferentDivisor_degree_le_of_bounds (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] (finiteDiscriminantDegree totalDifferentBudget : ℕ) (hFinite : finiteExtensionFiniteDifferentDegree K L ⋯ ≤ finiteDiscriminantDegree) (hInfinity : ↑(infinityDifferentDegree K L) ≤ ↑totalDifferentBudget - ↑finiteDiscriminantDegree) : finiteExtensionDivisorDegree K L (finiteExtensionCanonicalDifferentDivisor K L ⋯) ≤ ↑totalDifferentBudget - 2 * ↑(Module.finrank (RatFunc K) L)

Separate finite-discriminant and complementary infinity bounds combine into the expected canonical bound totalDifferent - 2 * [L : K(X)].