The total effective different divisor

This file packages the finite and above-infinity different multiplicities in one exhaustive effective divisor, and identifies its weighted degree with the sum of the two numerical different degrees already used by Riemann--Hurwitz.

Unlike the canonical divisor attached to dX, this effective divisor records the total different itself: its infinity coefficients do not contain the additional -2e correction coming from the pole of dX.

@[instance_reducible]

noncomputable def BGS.HasseWeil.totalDifferentFintype (K : Type u_1) [Finite K] : Fintype K

A finite enumeration of K used in the finite extension total different effective divisor construction.

Equations

• BGS.HasseWeil.totalDifferentFintype K = Fintype.ofFinite K

@[instance_reducible]

noncomputable def BGS.HasseWeil.totalDifferentPolynomialAlgebra (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 total different effective divisor construction.

Equations

• BGS.HasseWeil.totalDifferentPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

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

theorem BGS.HasseWeil.totalDifferentFiniteIntegralClosureModuleFinite (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) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

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

theorem BGS.HasseWeil.totalDifferentPolynomialTorsionFreeTop (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.HasseWeil.totalDifferentFiniteIntegralClosureIsTorsionFree (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) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

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

theorem BGS.HasseWeil.totalDifferentInfinityIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

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

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

theorem BGS.HasseWeil.totalDifferentInfinityIntegralClosureIsDedekindDomain (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 ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.HasseWeil.totalDifferentInfinityPlaceFintype (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 ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)

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

Equations

• BGS.HasseWeil.totalDifferentInfinityPlaceFintype K L = ⋯.fintype

noncomputable def BGS.HasseWeil.finiteExtensionTotalDifferentEffectiveDivisor (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] : FiniteExtensionEffectiveDivisor K L

The effective divisor whose coefficient at every exhaustive place is the local multiplicity of the trace different.

Equations

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

@[simp]

theorem BGS.HasseWeil.finiteExtensionTotalDifferentEffectiveDivisor_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] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : (finiteExtensionTotalDifferentEffectiveDivisor K L) (Sum.inl P) = multiplicity P.asIdeal (differentIdeal (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L))

@[simp]

theorem BGS.HasseWeil.finiteExtensionTotalDifferentEffectiveDivisor_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] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : (finiteExtensionTotalDifferentEffectiveDivisor K L) (Sum.inr P) = multiplicity (↑P) (differentIdeal ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L))

theorem BGS.HasseWeil.finiteExtensionTotalDifferentEffectiveDivisor_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] : finiteExtensionEffectiveDivisorDegree K L (finiteExtensionTotalDifferentEffectiveDivisor K L) = CorvajaZannier.finiteExtensionFiniteDifferentDegree K L ⋯ + CorvajaZannier.infinityDifferentDegree K L

The exhaustive effective different has degree equal to the finite different degree plus the above-infinity different degree.