NumberField.InfinitePlace.Comple… to NumberField.AdeleRing.baseChange…
TheoremNumberField.InfinitePlace.Completion.baseChangeEquiv#
Let \(v\) be an infinite place of \(K\). There is a natural \(L\)-algebra homeomorphism \(L\otimes_K K_v \cong_L \prod_{w\mid v}L_w\), whose restriction to \(1\otimes_K K_v\) corresponds to the map in NumberField.InfinitePlace.Completion.piExtension.
Proof
The map in NumberField.InfinitePlace.Completion.baseChange is an \(L\)-algebra isomorphism by Theorem NumberField.InfinitePlace.Completion.baseChange_surjective and Theorem NumberField.InfinitePlace.Completion.baseChange_injective. Every \(K_v\)-algebra isomorphism between two \(K_v\)-module topological spaces is a homeomorphism. Since the \(L\)-algebra isomorphism of Definition NumberField.InfinitePlace.Completion.baseChange can equivalently be viewed as a \(K_v\)-algebra isomorphism, it is also a homeomorphism.
Lean
Stated as NumberField.InfinitePlace.Completion.baseChangeEquiv; the blueprint marks no proof of it as formalized.
Sources
TheoremNumberField.InfinitePlace.Completion.piEquiv#
Let \(v\) be an infinite place of \(K\). There is a natural \(K_v\)-linear homeomorphism \(K_v^{[L:K]} \cong_{K_v} \prod_{w\mid v}L_w\).
Proof
Compose the \(K_v\)-linear isomorphism \(K_v^{[L:K]} \cong \prod_{w\mid v}L_w\) with the \(K_v\)-linear version of base change NumberField.InfinitePlace.Completion.baseChangeEquiv to get the isomorphism in the statement. Since both sides have the \(K_v\)-module topology, then this is also a homeomorphism.
Lean
Stated as NumberField.InfinitePlace.Completion.piEquiv; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
Base change for the infinite adele ring
First, we induce a \(K_{\infty}\)-algebra on \(L_{\infty}\) from the action of each \(K_v\) on \(\prod_{w\mid v}L_w\). Specifically, this means that for \(x \in K_{\infty}\) and \(y \in L_{\infty}\), we have \((x \cdot y)_w = x_{v_w} \cdot y_w\), where \(v_w\) is the restriction of \(w\) to \(K\). We show that \(L_{\infty}\) has the \(K_{\infty}\)-module topology.
TheoremNumberField.InfiniteAdeleRing.piEquiv#
There is a natural \(K_{\infty}\)-linear homeomorphism \(K_{\infty}^{[L:K]} \cong_{K_{\infty}} L_{\infty}\).
Proof
Using the isomorphisms \(K_v^{[L:K]} \cong_{K_v} \prod_{w\mid v}L_w\) from Theorem NumberField.InfinitePlace.Completion.piEquiv, we clearly have a bijection \(K_{\infty}^{[L:K]} \cong \prod_v\prod_{w \mid v} L_w \cong \prod_w L_w\). The \(K_v\)-linearity of each component isomorphism extends to \(K_{\infty}\)-linearity if the action of \(\prod_v K_v\) on \(\prod_w L_w\) is constant on the fibers of the restriction map on infinite places. In other words, if, for all \(x \in K_{\infty}\) and \(y \in L_{\infty}\), we have \((x \cdot y)_w = x_{v_w} \cdot y_w\), which is true by definition.
Lean
Stated as NumberField.InfiniteAdeleRing.piEquiv; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
TheoremNumberField.InfiniteAdeleRing.instIsModuleTopology_fLT#
\(L_{\infty}\) has the \(K_{\infty}\)-module topology.
Proof
Since \(L_{\infty}\) is homeomorphic to a finite product of \(K_{\infty}\) as a \(K_{\infty}\)-vector space, it has the \(K_{\infty}\)-module topology.
Lean
Stated as NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT; the blueprint marks no proof of it as formalized.
Sources
Uses 1
TheoremNumberField.InfiniteAdeleRing.baseChangeAlgEquiv#
There is a natural \(L\)-algebra isomorphism \(L \otimes_K K_{\infty} \cong_L L_{\infty}\).
Proof
This follows from the following chain of isomorphisms:
The first isomorphism is the standard \(L\)-algebra isomorphism \(L \otimes_K \prod_v K_v \cong_L \prod_v (L \otimes_K K_v)\). The second isomorphism is given by the component \(L\)-algebra isomorphisms \(L \otimes_K K_v \cong_L \prod_{w\mid v}L_w\) from Theorem NumberField.InfinitePlace.Completion.baseChangeEquiv.
Lean
Stated as NumberField.InfiniteAdeleRing.baseChangeAlgEquiv; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
It remains to show that the map in NumberField.InfiniteAdeleRing.baseChangeAlgEquiv is a homeomorphism. Since both sides have the \(K_{\infty}\)-module topology, and since the \(L\)-algebra isomorphism of NumberField.InfiniteAdeleRing.baseChangeAlgEquiv can equivalently be viewed as a \(K_{\infty}\)-linear isomorphism, it is also a homeomorphism.
TheoremNumberField.InfiniteAdeleRing.baseChangeEquiv#
If \(K\to L\) is a ring homomorphism between two number fields then there is a natural isomorphism (both topological and algebraic) \(L\otimes_KK_\infty\cong L_\infty\).
Proof
Since both sides of the \(L\)-algebra isomorphism in NumberField.InfiniteAdeleRing.baseChangeAlgEquiv have the \(K_{\infty}\)-module topology, and since the isomorphism can equivalently be viewed as a \(K_{\infty}\)-linear isomorphism, it is also a homeomorphism.
Lean
Stated as NumberField.InfiniteAdeleRing.baseChangeEquiv, NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
Base change for adeles
From the previous results we deduce immediately that if \(L/K\) is a finite extension of number fields then there's a natural (topological and algebraic) isomorphism \(L\otimes_K\mathbb{A}_K\to \mathbb{A}_L\).
TheoremNumberField.AdeleRing.baseChangeEquiv#
If \(K\to L\) is a ring homomorphism between two number fields then there is a natural isomorphism (both topological and algebraic) \(L\otimes_K\mathbb{A}_K\cong\mathbb{A}_L\).
Proof
Follows from the previous results.
Lean
Formalized as NumberField.AdeleRing.baseChangeEquiv.
Sources
Something else we shall need:
TheoremNumberField.AdeleRing.baseChange_moduleTopology#
If \(K\to L\) is a ring homomorphism between two number fields then the topology on \(\mathbb{A}_L\) is the \(\mathbb{A}_K\)-module topology, where the module structure comes from the natural map \(\mathbb{A}_K\to\mathbb{A}_L\).
Proof
Indeed \(\mathbb{A}_L\cong L\otimes_K\mathbb{A}_K\) is a homeomorphism, and the right hand side has the \(\mathbb{A}_K\)-module topology.
Lean
Formalized as NumberField.AdeleRing.instIsModuleTopology.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.