Discreteness and compactness

We need that if \(K\) is a number field then \(K\subseteq\mathbb{A}_K\) is discrete, and the quotient (with the quotient topology) is compact. Here is a proposed proof.

TheoremRat.AdeleRing.zero_discrete#

There's an open subset of \(\mathbb{A}_{\mathbb{Q}}\) whose intersection with \(\mathbb{Q}\) is \(\{0\}\).

Proof

Use \(\prod_p{\mathbb{Z}_p}\times(-1,1)\). Any rational \(q\) in this set is a \(p\)-adic integer for all primes \(p\) and hence (writing it in lowest terms as \(q=n/d\)) satisfies \(p\nmid d\), meaning that \(d=\pm1\) and thus \(q\in\mathbb{Z}\). The fact that \(q\in(-1,1)\) implies \(q=0\).

Lean

Stated as Rat.AdeleRing.zero_discrete; the blueprint marks no proof of it as formalized.

Sources
LeanRat.AdeleRing.zero_discrete
Used by 1
Used byNumberField.AdeleRing.zero_discrete

TheoremNumberField.AdeleRing.zero_discrete#

There's an open subset of \(\mathbb{A}_{K}\) whose intersection with \(K\) is \(\{0\}\).

Proof

By a previous result, we have \(\mathbb{A}_K=K\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}\). Choose a basis of \(K/\mathbb{Q}\); then \(K\) can be identified with \(\mathbb{Q}^n\subseteq(\mathbb{A}_{\mathbb{Q}})^n\) and the result follows from the previous theorem.

Lean

Stated as NumberField.AdeleRing.zero_discrete; the blueprint marks no proof of it as formalized.

Sources
LeanNumberField.AdeleRing.zero_discrete
Uses 2 · Used by 1
Statement usesRat.AdeleRing.zero_discrete · NumberField.AdeleRing.baseChangeEquiv
Used byNumberField.AdeleRing.discrete

TheoremNumberField.AdeleRing.discrete#

The additive subgroup \(K\) of \(\mathbb{A}_K\) is discrete.

Proof

If \(x\in K\) and \(U\) is the open subset in the previous lemma, then it's easily checked that \(K\cap U=\{0\}\) implies \(K\cap (U+x)=\{x\}\), and \(U+x\) is open.

Lean

Stated as NumberField.AdeleRing.discrete; the blueprint marks no proof of it as formalized.

Sources
LeanNumberField.AdeleRing.discrete
Uses 1
Statement usesNumberField.AdeleRing.zero_discrete

For compactness we follow the same approach.

TheoremRat.AdeleRing.cocompact#

The quotient \(\mathbb{A}_{\mathbb{Q}}/\mathbb{Q}\) is compact.

Proof

The space \(\prod_p\mathbb{Z}_p\times[0,1]\subseteq\mathbb{A}_{\mathbb{Q}}\) is a product of compact spaces and is hence compact. I claim that it surjects onto \(\mathbb{A}_{\mathbb{Q}}/\mathbb{Q}\). Indeed, if \(a\in\mathbb{A}_{\mathbb{Q}}\) then for the finitely many prime numbers \(p\in S\) such that \(a_p\not\in\mathbb{Z}_p\) we have \(a_p\in\frac{r_p}{p^{n_p}}+\mathbb{Z}_p\) with \(r_p/p^{n_p}\in\mathbb{Q}\), and if \(q=\sum_{p\in S}\frac{r_p}{p^{n_p}}\in\mathbb{Q}\) then \(a-q\in \prod_p\mathbb{Z}_p\times\mathbb{R}\). Now just subtract \(\lfloor a_{\infty}-q\rfloor\) to move into \(\prod_p\mathbb{Z}_p\times[0,1)\) and we are done.

Lean

Stated as Rat.AdeleRing.cocompact; the blueprint marks no proof of it as formalized.

Sources
LeanRat.AdeleRing.cocompact
Used by 1
Used byNumberField.AdeleRing.cocompact

TheoremNumberField.AdeleRing.cocompact#

The quotient \(\mathbb{A}_K/K\) is compact.

Proof

We proceed as in the discreteness proof above, by reducing to \(\mathbb{Q}\). As before, choosing a \(\mathbb{Q}\)-basis of \(K\) gives us \(\mathbb{A}_K/K\cong(\mathbb{A}_{\mathbb{Q}}/\mathbb{Q})^n\) so the result follows from the previous theorem.

Lean

Stated as NumberField.AdeleRing.cocompact; the blueprint marks no proof of it as formalized.

Sources
LeanNumberField.AdeleRing.cocompact
Uses 2
Statement usesRat.AdeleRing.cocompact · NumberField.AdeleRing.baseChangeEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.