Adeles of function fields

DefinitionAdèle ring of a field with respect to valuation subrings#✓fully proved

Let \(F\) be a field, \(P\) a type (of places) and, for each \(p \in P\), let \(O_p\) be a valuation subring of \(F\). The adèle ring of \(F\) with respect to \((O_p)_{p \in P}\) is the restricted product of the copies of \(F\) with respect to the subrings \(O_p\): its elements are the families \((a_p)_{p \in P}\) with \(a_p \in F\) for every \(p\) and \(a_p \in O_p\) for all but finitely many \(p\).

def FunctionFieldAdeleRing (F : Type*) [Field F] (P : Type*)
    (O : P → ValuationSubring F) : Type _ :=
  Πʳ p : P, [F, O p]

Used by 2

Used byExtensionality for restricted-product adèles · Adèles are integral at almost all places

TheoremExtensionality for restricted-product adèles#✓fully proved

Let \(F\) be a field, \(P\) a type and, for each \(p \in P\), let \(O_p\) be a valuation subring of \(F\). If two adèles \(a\) and \(b\) of the adèle ring of \(F\) with respect to \((O_p)_{p \in P}\) satisfy \(a_p = b_p\) for every \(p \in P\), then \(a = b\).

@[ext]
theorem ext {a b : FunctionFieldAdeleRing F P O} (h : ∀ p, a p = b p) : a = b

Uses 1

Statement usesAdèle ring of a field with respect to valuation subrings

TheoremAdèles are integral at almost all places#✓fully proved

Let \(F\) be a field, \(P\) a type and, for each \(p \in P\), let \(O_p\) be a valuation subring of \(F\). For every adèle \(a\) of the adèle ring of \(F\) with respect to \((O_p)_{p \in P}\), the component \(a_p\) lies in \(O_p\) for all but finitely many \(p \in P\).

theorem mem_valuationSubring_cofinitely (a : FunctionFieldAdeleRing F P O) :
    ∀ᶠ p in Filter.cofinite, a p ∈ O p

Uses 1

Statement usesAdèle ring of a field with respect to valuation subrings

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.