Exact dimensions of adele divisor quotients

This file proves the exact rank formula for the adele filtration and the sandwich identity.

@[instance_reducible]

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncAdeleFilter (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

Decidable equality on k(X) for adele filter proofs.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncAdeleFilter k = Classical.decEq (RatFunc k)

@[instance_reducible]

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqPlaceAAdeleFilter (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : DecidableEq (PlaceA k K)

Decidable equality on coordinate places for adele filter proofs.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqPlaceAAdeleFilter k K = Classical.decEq (MarkoffRiemannRoch.FunctionField.Chart.PlaceA k K)

@[instance_reducible]

def MarkoffRiemannRoch.FunctionField.Chart.adeleFiltAddCommGroup (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D' : DivisorA k K) : AddCommGroup ↥(adeleFilt k K D')

Additive group structure on adele filtration pieces.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.adeleFiltAddCommGroup k K D' = (MarkoffRiemannRoch.FunctionField.Chart.adeleFilt k K D').addCommGroup

@[instance_reducible]

def MarkoffRiemannRoch.FunctionField.Chart.adeleFiltModule (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D' : DivisorA k K) : Module k ↥(adeleFilt k K D')

Module structure on adele filtration pieces.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.adeleFiltModule k K D' = (MarkoffRiemannRoch.FunctionField.Chart.adeleFilt k K D').module

def MarkoffRiemannRoch.FunctionField.Chart.zeroAdele (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : ↥(AdeleSpace k K)

The zero adele.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.zeroAdele k K = ⟨0, ⋯⟩

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleLocalResidueToSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) (a : ↥(adeleFilt k K (D + Finsupp.single (Sum.inl v) 1))) : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)

Lift an adele to the valuation subring at a finite place, scaled by a uniformizer power.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleLocalResidueToSubring k K D v a = ⟨Classical.choose ⋯ ^ (D (Sum.inl v) + 1) * ↑↑a (Sum.inl v), ⋯⟩

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleLocalResidueMap (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : ↥(adeleFilt k K (D + Finsupp.single (Sum.inl v) 1)) →ₗ[k] v.asIdeal.ResidueField

One-step local residue map on adeles at a finite coordinate place.

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleLocalResidueMap_ker (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : (finiteAdeleLocalResidueMap k K D v).ker = Submodule.comap (adeleFilt k K (D + Finsupp.single (Sum.inl v) 1)).subtype (adeleFilt k K D)

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleLocalResidueMap_surjective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : Function.Surjective ⇑(finiteAdeleLocalResidueMap k K D v)

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleFiltDiff_single_finite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : finrankAdeleFiltDiff k K D (D + Finsupp.single (Sum.inl v) 1) = placeDegree k K (Sum.inl v)

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.infiniteAdeleLocalResidueToSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) (a : ↥(adeleFilt k K (D + Finsupp.single (Sum.inr v) 1))) : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)

Lift an adele to the valuation subring at an infinite place, scaled by a uniformizer power.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.infiniteAdeleLocalResidueToSubring k K D v a = ⟨Classical.choose ⋯ ^ (D (Sum.inr v) + 1) * ↑↑a (Sum.inr v), ⋯⟩

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.infiniteAdeleLocalResidueMap (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : ↥(adeleFilt k K (D + Finsupp.single (Sum.inr v) 1)) →ₗ[k] v.asIdeal.ResidueField

One-step local residue map on adeles at an infinite coordinate place.

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.infiniteAdeleLocalResidueMap_ker (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : (infiniteAdeleLocalResidueMap k K D v).ker = Submodule.comap (adeleFilt k K (D + Finsupp.single (Sum.inr v) 1)).subtype (adeleFilt k K D)

theorem MarkoffRiemannRoch.FunctionField.Chart.infiniteAdeleLocalResidueMap_surjective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : Function.Surjective ⇑(infiniteAdeleLocalResidueMap k K D v)

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleFiltDiff_single_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : finrankAdeleFiltDiff k K D (D + Finsupp.single (Sum.inr v) 1) = placeDegree k K (Sum.inr v)

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleFiltDiff_single_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) : finrankAdeleFiltDiff k K D (D + Finsupp.single v 1) = placeDegree k K v

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleFiltDiff_quotient_single (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) : Module.Finite k (↥(adeleFilt k K (D + Finsupp.single v 1)) ⧸ Submodule.comap (adeleFilt k K (D + Finsupp.single v 1)).subtype (adeleFilt k K D))

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleFiltDiff_quotient_self (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : Module.Finite k (↥(adeleFilt k K D) ⧸ Submodule.comap (adeleFilt k K D).subtype (adeleFilt k K D))

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleFiltDiff_quotient_mono_add (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D M N : DivisorA k K} (hDM : D ≤ M) (hMN : M ≤ N) [Module.Finite k (↥(adeleFilt k K N) ⧸ Submodule.comap (adeleFilt k K N).subtype (adeleFilt k K M))] [Module.Finite k (↥(adeleFilt k K M) ⧸ Submodule.comap (adeleFilt k K M).subtype (adeleFilt k K D))] : Module.Finite k (↥(adeleFilt k K N) ⧸ Submodule.comap (adeleFilt k K N).subtype (adeleFilt k K D))

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleFiltDiff_quotient_single_nat (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) (n : ℕ) : Module.Finite k (↥(adeleFilt k K (D + Finsupp.single v ↑n)) ⧸ Submodule.comap (adeleFilt k K (D + Finsupp.single v ↑n)).subtype (adeleFilt k K D))

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleFiltDiff_quotient_add_effective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) (hE : IsEffective k K E) : Module.Finite k (↥(adeleFilt k K (D + E)) ⧸ Submodule.comap (adeleFilt k K (D + E)).subtype (adeleFilt k K D))

theorem MarkoffRiemannRoch.FunctionField.Chart.finiteAdeleFiltDiff_quotient_add_eq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {M N : DivisorA k K} (hN : N = M + (N - M)) (hE : IsEffective k K (N - M)) : Module.Finite k (↥(adeleFilt k K N) ⧸ Submodule.comap (adeleFilt k K N).subtype (adeleFilt k K M))

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleFiltDiff_mono_add (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D M N : DivisorA k K} (hDM : D ≤ M) (hMN : M ≤ N) : finrankAdeleFiltDiff k K D N = finrankAdeleFiltDiff k K D M + finrankAdeleFiltDiff k K M N

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleFiltDiff_add_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D M : DivisorA k K} (v : PlaceA k K) (hDM : D ≤ M) : finrankAdeleFiltDiff k K D (M + Finsupp.single v 1) = finrankAdeleFiltDiff k K D M + placeDegree k K v

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleFiltDiff_add_effective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) (hE : IsEffective k K E) : finrankAdeleFiltDiff k K D (D + E) = (deg k K E).toNat

theorem MarkoffRiemannRoch.FunctionField.Chart.finrank_adeleFilt_quotient (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : finrankAdeleFiltDiff k K D D' = (deg k K (D' - D)).toNat

theorem MarkoffRiemannRoch.FunctionField.Chart.finrank_map_comap_mkQ_eq_quotient (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D' : DivisorA k K} {s t : Submodule k ↥(AdeleSpace k K)} (_hs : s ≤ adeleFilt k K D') (ht : t ≤ adeleFilt k K D') (_hst : s ≤ t) : Module.finrank k ↥(Submodule.map (Submodule.comap (adeleFilt k K D').subtype s).mkQ (Submodule.comap (adeleFilt k K D').subtype t)) = Module.finrank k (↥(Submodule.comap (adeleFilt k K D').subtype t) ⧸ Submodule.comap (Submodule.comap (adeleFilt k K D').subtype t).subtype (Submodule.comap (adeleFilt k K D').subtype s))

theorem MarkoffRiemannRoch.FunctionField.Chart.sandwich (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : sandwichRank k K D D' h = deg k K D' - ↑(ell k K D') - (deg k K D - ↑(ell k K D))

theorem MarkoffRiemannRoch.FunctionField.Chart.sandwichDiagonal_inter (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : adeleFilt k K D' ⊓ (adeleFilt k K D + diagonalSubmodule k K) = Submodule.map (diagonal k K) (RRspace k K D') ⊔ adeleFilt k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.sandwichDiagonalSubmodule_eq_of_rank_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (hle : D ≤ D') (h0 : sandwichRank k K D D' hle = 0) : adeleFilt k K D' + diagonalSubmodule k K = adeleFilt k K D + diagonalSubmodule k K