K-valued adele space of a function field

Definitions and basic structure for Stichtenoth's adele space.

@[instance_reducible]

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

The classical decidable equality on k(X) used by the coordinate places.

Equations

• FunctionField.Chart.instDecidableEqRatFuncAdele k = Classical.decEq (RatFunc k)

@[instance_reducible]

noncomputable def FunctionField.Chart.instDecidableEqPlaceAAdele (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

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

def FunctionField.Chart.adeleSubmodule (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 (PlaceA k K → K)

The k-submodule of the full product consisting of tuples integral at all but finitely many places.

Equations

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

theorem FunctionField.Chart.eventually_mem_placeValuationSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (f : K) : ∀ᶠ (v : PlaceA k K) in Filter.cofinite, f ∈ placeValuationSubring k K v

Every element of K is integral at all but finitely many coordinate places.

@[reducible, inline]

abbrev FunctionField.Chart.AdeleSpace (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 (PlaceA k K → K)

The K-valued adele space A_K = Πʳ_{v} [K, O_v].

Equations

• FunctionField.Chart.AdeleSpace k K = FunctionField.Chart.adeleSubmodule k K

def FunctionField.Chart.smulAdele (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] (x : K) (a : ↥(AdeleSpace k K)) : ↥(AdeleSpace k K)

Pointwise multiplication of an adele by an element of K.

Equations

• FunctionField.Chart.smulAdele k K x a = ⟨fun (v : FunctionField.Chart.PlaceA k K) => x * ↑a v, ⋯⟩

@[instance_reducible]

instance FunctionField.Chart.instSMulSubtypeForallPlaceAMemSubmoduleAdeleSpace (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] : SMul K ↥(AdeleSpace k K)

Equations

• FunctionField.Chart.instSMulSubtypeForallPlaceAMemSubmoduleAdeleSpace k K = { smul := FunctionField.Chart.smulAdele k K }

@[instance_reducible]

instance FunctionField.Chart.instModuleSubtypeForallPlaceAMemSubmoduleAdeleSpace (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] : Module K ↥(AdeleSpace k K)

Equations

• FunctionField.Chart.instModuleSubtypeForallPlaceAMemSubmoduleAdeleSpace k K = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

def FunctionField.Chart.mulAdeleLinear (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] (x : K) : ↥(AdeleSpace k K) →ₗ[k] ↥(AdeleSpace k K)

Multiplication by x ∈ K as a k-linear endomorphism of the adele space.

Equations

• FunctionField.Chart.mulAdeleLinear k K x = { toFun := fun (a : ↥(FunctionField.Chart.AdeleSpace k K)) => x • a, map_add' := ⋯, map_smul' := ⋯ }

def FunctionField.Chart.memAdeleFilt (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) (α : ↥(AdeleSpace k K)) : Prop

An adele lies in the filtration piece A(D) when its component at every place v has valuation at most WithZero.exp (D v).

Equations

• FunctionField.Chart.memAdeleFilt k K D α = ∀ (v : FunctionField.Chart.PlaceA k K), (FunctionField.Chart.placeValuation k K v) (↑α v) ≤ WithZero.exp (D v)

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

The filtration piece A(D) of the adele space.

Equations

• FunctionField.Chart.adeleFilt k K D = { carrier := {a : ↥(FunctionField.Chart.AdeleSpace k K) | FunctionField.Chart.memAdeleFilt k K D a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def FunctionField.Chart.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] : K →ₗ[k] ↥(AdeleSpace k K)

The diagonal embedding K → A_K of principal adeles.

Equations

• FunctionField.Chart.diagonal k K = { toFun := fun (f : K) => ⟨fun (x : FunctionField.Chart.PlaceA k K) => f, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

def FunctionField.Chart.diagonalSubmodule (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 image diag(K) of the diagonal embedding.

Equations

• FunctionField.Chart.diagonalSubmodule k K = (FunctionField.Chart.diagonal k K).range

theorem FunctionField.Chart.adeleFilt_inf_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] (D : DivisorA k K) : adeleFilt k K D ⊓ diagonalSubmodule k K = Submodule.map (diagonal k K) (RRspace k K D)

theorem FunctionField.Chart.adeleFilt_mono (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'

The adele filtration is monotone in the divisor.

def FunctionField.Chart.adeleFiltWithin (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) : Submodule k ↥(adeleFilt k K D')

A(D) as a submodule of A(D'), for D ≤ D'.

Equations

• FunctionField.Chart.adeleFiltWithin k K D D' = Submodule.comap (FunctionField.Chart.adeleFilt k K D').subtype (FunctionField.Chart.adeleFilt k K D)

noncomputable def FunctionField.Chart.finrankAdeleFiltDiff (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) : ℕ

Finite-rank increment finrank k (A(D') ⧸ A(D)).

Equations

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

noncomputable def FunctionField.Chart.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) : ℤ

Rank of (A(D') + diag(K)) ⧸ (A(D) + diag(K)) from the sandwich bookkeeping.

Equations

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

noncomputable def FunctionField.Chart.adeleUpdate (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) (a : K) : ↥(AdeleSpace k K)

Component update for adele surgery (A(D₁ ⊔ D₂) = A(D₁) + A(D₂)).

Equations

• FunctionField.Chart.adeleUpdate k K α v a = ⟨Function.update (↑α) v a, ⋯⟩

theorem FunctionField.Chart.adeleFilt_sup_eq_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₁ D₂ : DivisorA k K} : adeleFilt k K (D₁ ⊔ D₂) = adeleFilt k K D₁ + adeleFilt k K D₂