Cotrace construction for the finite-extension canonical different

This file constructs a surjective cotrace on fiber-constant adeles and uses the trace codifferent bounds to build a nonzero Weil differential whose maximal vanishing divisor contains the explicit finite-extension different. Nothing in this file is an assumption.

@[reducible, inline]

abbrev BGS.HasseWeil.RatFuncExhaustivePlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : Type u_1

The exhaustive rational-function places used as the base of the finite extension place map.

Equations

• BGS.HasseWeil.RatFuncExhaustivePlace K = (IsDedekindDomain.HeightOneSpectrum (Polynomial K) ⊕ IsDedekindDomain.HeightOneSpectrum ↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K))

noncomputable def BGS.HasseWeil.ratFuncFiniteBaseRingEquivChart (K : Type u_1) [Field K] : Polynomial K ≃+* ↥(FunctionField.ringOfIntegers K (RatFunc K))

The polynomial ring is the integral closure of itself in its fraction field, so its height-one primes are exactly the finite chart places of K(X).

Equations

• BGS.HasseWeil.ratFuncFiniteBaseRingEquivChart K = (IsIntegralClosure.equiv (Polynomial K) (Polynomial K) (RatFunc K) ↥(FunctionField.ringOfIntegers K (RatFunc K))).toRingEquiv

theorem BGS.HasseWeil.ratFuncFiniteBaseRingEquivChart_algebraMap (K : Type u_1) [Field K] (r : Polynomial K) : (algebraMap (↥(FunctionField.ringOfIntegers K (RatFunc K))) (RatFunc K)) ((ratFuncFiniteBaseRingEquivChart K) r) = (algebraMap (Polynomial K) (RatFunc K)) r

noncomputable def BGS.HasseWeil.ratFuncInfinityBaseRingEquivChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : ↥(CorvajaZannier.RatFuncInfinityIntegers K) ≃+* ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K (RatFunc K))

The BGS infinity valuation ring and the chart infinity integral closure inside K(X) are canonically equivalent.

Equations

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

theorem BGS.HasseWeil.ratFuncInfinityBaseRingEquivChart_algebraMap (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (r : ↥(CorvajaZannier.RatFuncInfinityIntegers K)) : (algebraMap (↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K (RatFunc K))) (RatFunc K)) ((ratFuncInfinityBaseRingEquivChart K) r) = (algebraMap (↥(CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K)) r

noncomputable def BGS.HasseWeil.ratFuncExhaustivePlaceEquivChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : RatFuncExhaustivePlace K ≃ MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)

Reindex the exhaustive BGS rational-function places as chart places.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.cotracePolynomialAlgebra (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 cotrace construction.

Equations

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

theorem BGS.HasseWeil.cotracePolynomialTower (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.cotraceFiniteClosureModuleFinite (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.cotraceFiniteClosureIsIntegral (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.cotraceFiniteBaseTorsionFreeTop (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.cotraceFiniteClosureTorsionFree (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.cotraceInfinityClosureModuleFinite (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.cotraceInfinityClosureIsIntegral (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.cotraceInfinityBaseTorsionFreeTop (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.cotraceInfinityClosureTorsionFree (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.cotraceInfinityClosureIsDedekind (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)

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

theorem BGS.HasseWeil.heightOneValuation_algebraMap_le_one_of_under {R : Type u_3} {S : Type u_4} {F : Type u_5} {E : Type u_6} [CommRing R] [CommRing S] [Field F] [Field E] [Algebra R S] [Algebra R F] [Algebra R E] [Algebra S E] [Algebra F E] [IsScalarTower R S E] [IsScalarTower R F E] [Algebra.IsIntegral R S] [IsFractionRing R F] [IsFractionRing S E] [IsDedekindDomain R] [IsDedekindDomain S] (q : IsDedekindDomain.HeightOneSpectrum S) (p : IsDedekindDomain.HeightOneSpectrum R) (hunder : IsDedekindDomain.HeightOneSpectrum.under R q = p) {x : F} (hx : (IsDedekindDomain.HeightOneSpectrum.valuation F p) x ≤ 1) : (IsDedekindDomain.HeightOneSpectrum.valuation E q) ((algebraMap F E) x) ≤ 1

Integrality at a height-one prime pulls up along a finite extension to every prime above it.

theorem BGS.HasseWeil.zero_le_count_spanSingleton_of_valuation_le_one {R : Type u_3} {F : Type u_4} [CommRing R] [Field F] [Algebra R F] [IsFractionRing R F] [IsDedekindDomain R] (q : IsDedekindDomain.HeightOneSpectrum R) {x : F} (hx : x ≠ 0) (hval : (IsDedekindDomain.HeightOneSpectrum.valuation F q) x ≤ 1) : 0 ≤ FractionalIdeal.count F q ((FractionalIdeal.spanSingleton (nonZeroDivisors R)) x)

Integrality at a height-one place is the nonnegativity of its principal fractional-ideal count.

noncomputable def BGS.HasseWeil.finiteExtensionUnderPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : CorvajaZannier.FiniteExtensionPlace K L → RatFuncExhaustivePlace K

Forget an extension place down to its rational-function place.

Equations

• BGS.HasseWeil.finiteExtensionUnderPlace K L (Sum.inl q) = Sum.inl (IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q)
• BGS.HasseWeil.finiteExtensionUnderPlace K L (Sum.inr val) = Sum.inr (BGS.CorvajaZannier.ratFuncInfinityPlace K)

theorem BGS.HasseWeil.finiteExtensionUnderPlace_surjective (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] : Function.Surjective (finiteExtensionUnderPlace K L)

Every rational-function place has an extension place above it.

theorem BGS.HasseWeil.finiteExtensionUnderPlace_finite_preimage_singleton (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 : RatFuncExhaustivePlace K) : (finiteExtensionUnderPlace K L ⁻¹' {p}).Finite

Every fiber of the exhaustive place map is finite.

theorem BGS.HasseWeil.finiteExtensionUnderPlace_tendstoCofinite (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] : Filter.TendstoCofinite (finiteExtensionUnderPlace K L)

Pullback along the exhaustive place map preserves cofinite eventual properties.

noncomputable def BGS.HasseWeil.finiteExtensionUnderPlaceChart (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 : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L) : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)

The place below a top chart place, expressed in the base chart.

Equations

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

theorem BGS.HasseWeil.finiteExtensionUnderPlaceChart_surjective (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] : Function.Surjective (finiteExtensionUnderPlaceChart K L)

Every rational-function chart place has an upstairs chart place.

theorem BGS.HasseWeil.finiteExtensionUnderPlaceChart_tendstoCofinite (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] : Filter.TendstoCofinite (finiteExtensionUnderPlaceChart K L)

Pullback along the chart place map preserves cofinite eventual properties.

theorem BGS.HasseWeil.finiteExtension_placeValuation_algebraMap_le_one (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 : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L) {x : RatFunc K} (hx : (MarkoffRiemannRoch.FunctionField.Chart.placeValuation K (RatFunc K) (finiteExtensionUnderPlaceChart K L q)) x ≤ 1) : (MarkoffRiemannRoch.FunctionField.Chart.placeValuation K L q) ((algebraMap (RatFunc K) L) x) ≤ 1

A base element integral at a chart place remains integral at every upstairs chart place above it.

noncomputable def BGS.HasseWeil.finiteExtensionPlaceSectionChart (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 : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)) : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L

A chosen place of L above each rational-function chart place.

Equations

• BGS.HasseWeil.finiteExtensionPlaceSectionChart K L p = Classical.choose ⋯

@[simp]

theorem BGS.HasseWeil.finiteExtensionUnderPlaceChart_section (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 : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)) : finiteExtensionUnderPlaceChart K L (finiteExtensionPlaceSectionChart K L p) = p

@[instance_reducible]

noncomputable def BGS.HasseWeil.cotraceConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the finite extension canonical different cotrace construction.

Equations

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

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

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

def BGS.HasseWeil.finiteExtensionFiberConstantAdeleSubmodule (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] : Submodule K ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K L)

Adeles whose components are constant on every fiber over a base place.

Equations

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

theorem BGS.HasseWeil.fiberConstant_component_eq_section (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] (a : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)) (q : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L) : ↑↑a q = ↑↑a (finiteExtensionPlaceSectionChart K L (finiteExtensionUnderPlaceChart K L q))

A fiber-constant adele has the chosen component at the base place of every upstairs place.

noncomputable def BGS.HasseWeil.finiteExtensionFiberTraceRaw (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] : ↥(finiteExtensionFiberConstantAdeleSubmodule K L) →ₗ[K] MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K) → RatFunc K

Componentwise field trace of a fiber-constant adele, before proving that the resulting tuple is a rational-function adele.

Equations

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

def BGS.HasseWeil.finiteExtensionAdeleExceptionalSet (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] (a : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K L)) : Set (MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L)

Top chart places at which a given adele is not integral.

Equations

• BGS.HasseWeil.finiteExtensionAdeleExceptionalSet K L a = {q : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L | ↑a q ∉ MarkoffRiemannRoch.FunctionField.Chart.placeValuationSubring K L q}

theorem BGS.HasseWeil.finiteExtensionAdeleExceptionalSet_finite (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] (a : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K L)) : (finiteExtensionAdeleExceptionalSet K L a).Finite

def BGS.HasseWeil.finiteExtensionDifferentExceptionalSet (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] : Set (MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L)

Finite chart places in the support of the finite different.

Equations

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

theorem BGS.HasseWeil.finiteExtensionDifferentExceptionalSet_finite (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] : (finiteExtensionDifferentExceptionalSet K L).Finite

noncomputable def BGS.HasseWeil.ratFuncInfinityPlaceChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)

The unique base infinity chart place, expressed through the exhaustive place equivalence.

Equations

• BGS.HasseWeil.ratFuncInfinityPlaceChart K = (BGS.HasseWeil.ratFuncExhaustivePlaceEquivChart K) (Sum.inr (BGS.CorvajaZannier.ratFuncInfinityPlace K))

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteExtensionCotraceConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The constant-field algebra on L induced by its rational-function-field algebra.

Equations

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

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

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

def BGS.HasseWeil.finiteExtensionCotraceBadBaseSet (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] (a : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K L)) : Set (MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K))

The finite exceptional set outside which the componentwise trace is integral.

Equations

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

theorem BGS.HasseWeil.finiteExtensionCotraceBadBaseSet_finite (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] (a : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K L)) : (finiteExtensionCotraceBadBaseSet K L a).Finite

theorem BGS.HasseWeil.ratFunc_infinite_chart_place_eq (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (p : IsDedekindDomain.HeightOneSpectrum ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K (RatFunc K))) : Sum.inr p = ratFuncInfinityPlaceChart K

The infinity component of the rational-function chart contains only the place transported from the BGS infinity valuation ring.

theorem BGS.HasseWeil.finiteExtensionFiberTraceRaw_mem_placeValuationSubring_of_not_bad (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] (a : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)) (p : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)) (hp : p ∉ finiteExtensionCotraceBadBaseSet K L ↑a) : (finiteExtensionFiberTraceRaw K L) a p ∈ MarkoffRiemannRoch.FunctionField.Chart.placeValuationSubring K (RatFunc K) p

Outside the explicit finite exceptional set, the raw componentwise trace is integral at the base chart place.

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteExtensionFiberTraceConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The constant-field algebra on the extension field used for the fiber trace construction.

Equations

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

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

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

noncomputable def BGS.HasseWeil.finiteExtensionFiberTrace (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] : ↥(finiteExtensionFiberConstantAdeleSubmodule K L) →ₗ[K] ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K (RatFunc K))

Componentwise field trace as an actual rational-function adele.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionFiberLift (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] (z : L) (b : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K (RatFunc K))) : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)

Lift a base adele to a fiber-constant upstairs adele after multiplying by a fixed extension-field element.

Equations

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

theorem BGS.HasseWeil.finiteExtensionFiberTrace_lift (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] (z : L) (b : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K (RatFunc K))) : (finiteExtensionFiberTrace K L) (finiteExtensionFiberLift K L z b) = (Algebra.trace (RatFunc K) L) z • b

Cotrace of the lifted adele is scalar multiplication by Tr(z).

theorem BGS.HasseWeil.finiteExtensionFiberTrace_surjective (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] : Function.Surjective ⇑(finiteExtensionFiberTrace K L)

Componentwise cotrace is onto the base adele space.

theorem BGS.HasseWeil.finiteExtensionFiberTrace_finite_valuation_le_one (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] (a : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)) (ha : ↑a ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))) (p : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers K (RatFunc K))) : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) p) (↑((finiteExtensionFiberTrace K L) a) (Sum.inl p)) ≤ 1

At a finite base place, the componentwise trace of a fiber-constant adele in the explicit different filtration is integral.

theorem BGS.HasseWeil.finiteExtensionFiberTrace_infinite_valuation_le_exp_neg_two (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] (a : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)) (ha : ↑a ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))) (p : IsDedekindDomain.HeightOneSpectrum ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K (RatFunc K))) : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) p) (↑((finiteExtensionFiberTrace K L) a) (Sum.inr p)) ≤ WithZero.exp (-2)

At the infinite base place, the componentwise trace of a fiber-constant adele in the explicit different filtration has order at least two.

theorem BGS.HasseWeil.ratFuncInfinityChartPlace_eq_baseChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : ratFuncInfinityChartPlace K = ratFuncInfinityPlaceChart K

The infinity place selected for the identity extension is the unique infinity place in the base chart.

theorem BGS.HasseWeil.finiteExtensionFiberTrace_mem_ratFuncCanonicalInfinityAdeleFilt (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] (a : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)) (ha : ↑a ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))) : (finiteExtensionFiberTrace K L) a ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K (RatFunc K) (ratFuncCanonicalInfinityDivisor K)

The cotrace sends the explicit different filtration into the canonical -2∞ filtration on the rational function field.

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteExtensionLocalCotraceConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The constant-field algebra on the extension field used for the local cotrace comparison.

Equations

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

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

theorem BGS.HasseWeil.finiteExtension_diagonal_mem_fiberConstant (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) : (MarkoffRiemannRoch.FunctionField.Chart.diagonal K L) x ∈ finiteExtensionFiberConstantAdeleSubmodule K L

Principal adeles are fiber-constant.

theorem BGS.HasseWeil.finiteExtensionFiberTrace_diagonal (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) : (finiteExtensionFiberTrace K L) ⟨(MarkoffRiemannRoch.FunctionField.Chart.diagonal K L) x, ⋯⟩ = (MarkoffRiemannRoch.FunctionField.Chart.diagonal K (RatFunc K)) ((Algebra.trace (RatFunc K) L) x)

Cotrace carries a principal adele to the principal adele of the field trace.

theorem BGS.HasseWeil.finiteExtensionFiberCotrace_vanishes_on_intersection (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] (ω : MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential K (RatFunc K)) (hωvan : ratFuncCanonicalInfinityDivisor K ∈ ω.vanishingDivisors) (x : ↥(finiteExtensionFiberConstantAdeleSubmodule K L ⊓ (MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯)) + MarkoffRiemannRoch.FunctionField.Chart.diagonalSubmodule K L))) : (ω.toFun ∘ₗ finiteExtensionFiberTrace K L) ⟨↑x, ⋯⟩ = 0

The base canonical functional composed with cotrace vanishes on the intersection of fiber-constant adeles with the explicit different filtration plus principal adeles.

theorem BGS.HasseWeil.finiteExtensionFiberCotrace_ne_zero (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] (ω : MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential K (RatFunc K)) (hω : ω.toFun ≠ 0) : ω.toFun ∘ₗ finiteExtensionFiberTrace K L ≠ 0

A nonzero base Weil functional stays nonzero after composition with the surjective fiber cotrace.

theorem BGS.HasseWeil.finiteExtensionCanonicalDifferent_le_divOmega (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] [hFull : MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] : ∃ (ωTop : MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential K L) (hωTop : ωTop.IsNonzero), (finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) ≤ ωTop.divOmega hωTop

The explicit finite-extension different divisor is a vanishing divisor of a nonzero Weil differential. Consequently it is bounded above by the maximal divisor of that differential.