Adele quotient rank and the index of specialty

This file proves Stichtenoth 1.5.4: the rank of 𝒜_K/(A(D)+diag(K)) equals the specialty index i(D).

@[instance_reducible]

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

The classical decidable equality on coordinate places used for adele surgery.

Equations

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

def MarkoffRiemannRoch.FunctionField.Chart.topAdeleSubmodule (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] : Submodule k ↥(AdeleSpace k K)

The top submodule of the adele space (avoids ↥⊤ notation pitfalls).

Equations

• MarkoffRiemannRoch.FunctionField.Chart.topAdeleSubmodule k K = ⊤

theorem MarkoffRiemannRoch.FunctionField.Chart.exceptionalFinite (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)) : {v : PlaceA k K | ¬(placeValuation k K v) (↑α v) ≤ 1}.Finite

Finite set of finite places where an adele component is not integral.

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.exceptionalPlaces (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)) : Finset (PlaceA k K)

Finset of finite places where an adele component is not integral.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.exceptionalPlaces k K α = ⋯.toFinset

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.divisorOfAdele (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)) : DivisorA k K

Every adele lies in some filtration piece A(D).

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.mem_adeleFilt_divisorOfAdele (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)) : α ∈ adeleFilt k K (divisorOfAdele k K α)

theorem MarkoffRiemannRoch.FunctionField.Chart.exists_adeleFilt_mem (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)) : ∃ (D : DivisorA k K), α ∈ adeleFilt k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.defect_eq_genus_of_ge (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] [IsFullConstantField k K] {D D' : DivisorA k K} (hle : D ≤ D') (hD : defect k K D = ↑(genus k K)) : defect k K D' = ↑(genus k K)

theorem MarkoffRiemannRoch.FunctionField.Chart.sandwichRank_eq_zero_of_defect_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] [IsFullConstantField k K] {D D' : DivisorA k K} (hle : D ≤ D') (hD : defect k K D = ↑(genus k K)) : sandwichRank k K D D' hle = 0

theorem MarkoffRiemannRoch.FunctionField.Chart.adeleFilt_add_diagonal_eq_of_sandwich_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

theorem MarkoffRiemannRoch.FunctionField.Chart.adeleSubmodule_top_eq_adeleFilt_add_diagonal (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] [IsFullConstantField k K] {D : DivisorA k K} (hD : defect k K D = ↑(genus k K)) : topAdeleSubmodule k K = adeleFilt k K D + diagonalSubmodule k K

theorem MarkoffRiemannRoch.FunctionField.Chart.finrankAdeleQuotient_eq_sandwichRank (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') (hfull : topAdeleSubmodule k K = adeleFilt k K D' + diagonalSubmodule k K) : finrankAdeleQuotient k K D = (sandwichRank k K D D' hle).toNat

theorem MarkoffRiemannRoch.FunctionField.Chart.finrank_adele_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] [IsFullConstantField k K] (D : DivisorA k K) : finrankAdeleQuotient k K D = indexOfSpecialty k K D