Local maximality of the canonical different by cotrace #
This file connects the generic trace-image theorem formalizing Stichtenoth,
Theorem 3.4.6, Step (b1), to the explicit -2∞ base differential and the
extension-place filtration. A one-place witness detects every divisor not
bounded by the trace-different divisor. Applied to the glued cotrace Weil
functional, this proves that the trace-different divisor is its exact maximal
vanishing divisor, without assuming a Riemann--Hurwitz degree identity.
theorem
BGS.HasseWeil.ratFuncCanonicalWeil_exists_singlePlace_witness
(K : Type u_1)
[Field K]
[DecidableEq (RatFunc K)]
(ω : MarkoffRiemannRoch.FunctionField.Chart.WeilDifferential K (RatFunc K))
(hω : ω.IsNonzero)
(hdiv : ω.divOmega hω = ratFuncCanonicalInfinityDivisor K)
(p : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K))
:
∃
a ∈
MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K (RatFunc K)
(ratFuncCanonicalInfinityDivisor K + Finsupp.single p 1),
ω.toFun a ≠ 0 ∧ (∀ (v : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)), v ≠ p → ↑a v = 0) ∧ (MarkoffRiemannRoch.FunctionField.Chart.placeValuation K (RatFunc K) p) (↑a p) = WithZero.exp ((ratFuncCanonicalInfinityDivisor K) p + 1)
At every base chart place, maximality of the canonical -2∞
differential supplies a one-component adele at the first filtration step on
which the differential is nonzero.
@[instance_reducible]
noncomputable def
BGS.HasseWeil.detectionPolynomialAlgebra
(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 local maximality construction.
Equations
- BGS.HasseWeil.detectionPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra
Instances For
theorem
BGS.HasseWeil.detectionPolynomialTower
(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.detectionFiniteClosureModuleFinite
(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]
:
theorem
BGS.HasseWeil.detectionFiniteBaseTorsionFreeTop
(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]
:
theorem
BGS.HasseWeil.detectionFiniteClosureTorsionFree
(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]
:
theorem
BGS.HasseWeil.detectionInfinityClosureModuleFinite
(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]
:
theorem
BGS.HasseWeil.detectionInfinityClosureIsIntegral
(K : Type u_1)
[Field K]
[DecidableEq (RatFunc K)]
(L : Type u_2)
[Field L]
[Algebra (RatFunc K) L]
:
theorem
BGS.HasseWeil.detectionInfinityBaseTorsionFreeTop
(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]
:
theorem
BGS.HasseWeil.detectionInfinityClosureTorsionFree
(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]
:
theorem
BGS.HasseWeil.detectionInfinityClosureIsDedekind
(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]
:
theorem
BGS.HasseWeil.detectionInfinityClosureIsFractionRing
(K : Type u_1)
[Field K]
[DecidableEq (RatFunc K)]
(L : Type u_2)
[Field L]
[Algebra (RatFunc K) L]
[FiniteDimensional (RatFunc K) L]
:
theorem
BGS.HasseWeil.finiteExtensionFiberLift_mem_adeleFilt_of_supported
(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]
(Btop : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L)
(p : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K))
(b : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K (RatFunc K)))
(z : L)
(hbp : ↑b p = 1)
(hbAway : ∀ (v : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)), v ≠ p → ↑b v = 0)
(hz :
∀ (q : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L),
finiteExtensionUnderPlaceChart K L q = p →
(MarkoffRiemannRoch.FunctionField.Chart.placeValuation K L q) z ≤ WithZero.exp (Btop q))
:
A fiber lift supported over one base place lies in an arbitrary divisor filtration once its common nonzero fiber value satisfies the local bounds.
theorem
BGS.HasseWeil.finiteExtensionFiberLift_normalized_trace
(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))
(p : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K))
(a : ↥(MarkoffRiemannRoch.FunctionField.Chart.AdeleSpace K (RatFunc K)))
(haNonzero : ω.toFun a ≠ 0)
(haAway : ∀ (v : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)), v ≠ p → ↑a v = 0)
(x : RatFunc K)
(hx : x = ↑a p)
(hx0 : x ≠ 0)
(z : L)
(hzTrace : (Algebra.trace (RatFunc K) L) z = x)
:
have b := x⁻¹ • a;
↑b p = 1 ∧ (∀ (v : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)), v ≠ p → ↑b v = 0) ∧ ω.toFun ((finiteExtensionFiberTrace K L) (finiteExtensionFiberLift K L z b)) ≠ 0
Normalize a one-component base adele and lift a trace preimage without changing its cotrace.
theorem
BGS.HasseWeil.finiteExtensionFiberCotrace_detects_finite_excess
(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ω : ω.IsNonzero)
(hdiv : ω.divOmega hω = ratFuncCanonicalInfinityDivisor K)
(Btop : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L)
(q₀ : IsDedekindDomain.HeightOneSpectrum ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L))
(hbad :
((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))
((finiteExtensionPlaceEquivChart K L) (Sum.inl q₀)) < Btop ((finiteExtensionPlaceEquivChart K L) (Sum.inl q₀)))
:
∃ (β : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)),
↑β ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L Btop ∧ ω.toFun ((finiteExtensionFiberTrace K L) β) ≠ 0
Step (b1), finite-place branch: any coefficient strictly above the finite different is detected by the cotrace functional on a fiber-constant adele in that divisor filtration.
theorem
BGS.HasseWeil.finiteExtensionFiberCotrace_detects_infinity_excess
(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ω : ω.IsNonzero)
(hdiv : ω.divOmega hω = ratFuncCanonicalInfinityDivisor K)
(Btop : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L)
(P₀ : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L))
(hbad :
((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))
((finiteExtensionPlaceEquivChart K L) (Sum.inr P₀)) < Btop ((finiteExtensionPlaceEquivChart K L) (Sum.inr P₀)))
:
∃ (β : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)),
↑β ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L Btop ∧ ω.toFun ((finiteExtensionFiberTrace K L) β) ≠ 0
Step (b1), infinity-place branch: after compensating the -2e term by
the square of the base infinity uniformizer, any coefficient strictly above
the infinity different is detected by cotrace.
theorem
BGS.HasseWeil.finiteExtensionFiberCotrace_detects_not_le
(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ω : ω.IsNonzero)
(hdiv : ω.divOmega hω = ratFuncCanonicalInfinityDivisor K)
(Btop : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L)
(hB : ¬Btop ≤ (finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))
:
∃ (β : ↥(finiteExtensionFiberConstantAdeleSubmodule K L)),
↑β ∈ MarkoffRiemannRoch.FunctionField.Chart.adeleFilt K L Btop ∧ ω.toFun ((finiteExtensionFiberTrace K L) β) ≠ 0
Stichtenoth, Theorem 3.4.6, Step (b1), in the project chart model: every divisor not bounded by the explicit canonical different is detected by the base canonical functional after cotrace.
@[instance_reducible]
noncomputable def
BGS.HasseWeil.detectionConstantAlgebra
(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
local maximality construction.
Equations
- BGS.HasseWeil.detectionConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra
Instances For
theorem
BGS.HasseWeil.finiteExtensionCanonicalDifferent_isCanonical_of_cotrace
(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.IsFullConstantField K L]
:
The trace-different divisor is exactly the maximal vanishing divisor of the Weil functional obtained by gluing cotrace to zero. This is the direct local-maximality conclusion of Stichtenoth, Theorem 3.4.6, Step (b1), and does not assume a Riemann--Hurwitz degree identity.
theorem
BGS.HasseWeil.finiteExtension_genus_le_canonicalDifferent_finrank_of_cotrace
(K : Type u_1)
[Field K]
[Fintype 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]
[MarkoffRiemannRoch.FunctionField.IsFullConstantField K L]
:
The remaining trace-residue lower bound follows from the direct cotrace canonicality theorem, with no degree premise.
theorem
BGS.HasseWeil.finiteExtension_genus_le_budget_of_cotrace
(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]
[MarkoffRiemannRoch.FunctionField.IsFullConstantField K L]
(budget : ℕ)
(hdegree :
CorvajaZannier.finiteExtensionDivisorDegree K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) ≤ 2 * ↑budget - 2)
:
Any upper bound for the explicit different degree gives the corresponding genus bound directly from cotrace canonicality.