Adeles indexed by intrinsic places

This file defines the function-field adele space directly as a restricted product over coordinate-free places. The equivalence adeleEquivChart identifies it with the two-chart construction and transports the filtration and diagonal embedding.

def FunctionField.adeleSubmodule (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Submodule k (Place k K → K)

The k-submodule of tuples over intrinsic places that are integral almost everywhere.

Equations

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

@[reducible, inline]

abbrev FunctionField.AdeleSpace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Submodule k (Place k K → K)

The intrinsic, K-valued adele space.

Equations

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

theorem FunctionField.eventually_mem_place (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] (f : K) : ∀ᶠ (v : Place k K) in Filter.cofinite, f ∈ v.toValuationSubring

Every element of the function field is integral at all but finitely many intrinsic places.

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

Reindex an intrinsic adele along the equivalence between chart and intrinsic places.

Equations

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

@[simp]

theorem FunctionField.adeleEquivChart_apply (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] (a : ↥(AdeleSpace k K)) (w : Chart.PlaceA k K) : ↑((adeleEquivChart k K) a) w = ↑a ((chartToPlace k K) w)

@[simp]

theorem FunctionField.adeleEquivChart_symm_apply (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] (a : ↥(Chart.AdeleSpace k K)) (v : Place k K) : ↑((adeleEquivChart k K).symm a) v = ↑a ((chartToPlace k K).symm v)

def FunctionField.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 intrinsic adele by an element of K.

Equations

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

@[instance_reducible]

instance FunctionField.instSMulSubtypeForallPlaceMemSubmoduleAdeleSpace (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.instSMulSubtypeForallPlaceMemSubmoduleAdeleSpace k K = { smul := FunctionField.smulAdele k K }

@[instance_reducible]

instance FunctionField.instModuleSubtypeForallPlaceMemSubmoduleAdeleSpace (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.instModuleSubtypeForallPlaceMemSubmoduleAdeleSpace k K = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

@[simp]

theorem FunctionField.adeleEquivChart_smul (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)) : (adeleEquivChart k K) (x • a) = x • (adeleEquivChart k K) a

The intrinsic-to-chart adele equivalence commutes with multiplication by K.

def FunctionField.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 an element of K as a k-linear endomorphism of intrinsic adeles.

Equations

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

def FunctionField.memAdeleFilt (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) (a : ↥(AdeleSpace k K)) : Prop

An intrinsic adele satisfies the bound prescribed by a divisor.

Equations

• FunctionField.memAdeleFilt k K D a = ∀ (v : FunctionField.Place k K), v.valuation (↑a v) ≤ WithZero.exp (D v)

def FunctionField.adeleFilt (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : Submodule k ↥(AdeleSpace k K)

The intrinsic adele filtration piece A(D).

Equations

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

theorem FunctionField.mem_adeleFilt_equivChart (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 : Divisor k K) (a : ↥(AdeleSpace k K)) : (adeleEquivChart k K) a ∈ Chart.adeleFilt k K ((divisorEquivChart k K).symm D) ↔ a ∈ adeleFilt k K D

Membership in the intrinsic filtration agrees with chart filtration membership.

theorem FunctionField.adeleFilt_mono (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] {D E : Divisor k K} (h : D ≤ E) : adeleFilt k K D ≤ adeleFilt k K E

The intrinsic adele filtration is monotone in the divisor.

def FunctionField.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 of the function field into intrinsic adeles.

Equations

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

def FunctionField.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 of the intrinsic diagonal embedding.

Equations

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

@[simp]

theorem FunctionField.adeleEquivChart_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] (f : K) : (adeleEquivChart k K) ((diagonal k K) f) = (Chart.diagonal k K) f

theorem FunctionField.map_adeleFilt_equivChart (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 : Divisor k K) : Submodule.map (↑(adeleEquivChart k K)) (adeleFilt k K D) = Chart.adeleFilt k K ((divisorEquivChart k K).symm D)

The chart equivalence maps the intrinsic filtration onto the chart filtration.

theorem FunctionField.map_diagonalSubmodule_equivChart (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.map (↑(adeleEquivChart k K)) (diagonalSubmodule k K) = Chart.diagonalSubmodule k K

The chart equivalence maps the intrinsic diagonal submodule onto the chart diagonal.

theorem FunctionField.map_adeleFilt_add_diagonal_equivChart (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 : Divisor k K) : Submodule.map (↑(adeleEquivChart k K)) (adeleFilt k K D + diagonalSubmodule k K) = Chart.adeleFilt k K ((divisorEquivChart k K).symm D) + Chart.diagonalSubmodule k K

The chart equivalence maps A(D) plus the diagonal onto the corresponding chart submodule.

theorem FunctionField.mem_adeleFilt_add_diagonal_equivChart (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 : Divisor k K) (a : ↥(AdeleSpace k K)) : (adeleEquivChart k K) a ∈ Chart.adeleFilt k K ((divisorEquivChart k K).symm D) + Chart.diagonalSubmodule k K ↔ a ∈ adeleFilt k K D + diagonalSubmodule k K

Membership in A(D) plus the diagonal is preserved by the chart equivalence.