IsDedekindDomain.HeightOneSpectr… to NumberField.InfinitePlace.Comple…
LemmaIsDedekindDomain.HeightOneSpectrum.valuation_comap#
If \(i:K\to L\) denotes the inclusion then for \(k\in K\) we have \(e\times w(i(k))=v(k)\), where \(e\) is the ramification index of \(w/v\) (recall that valuations here are written additively, unlike in mathlib).
Proof
Standard (and formalized).
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.valuation_comap.
Sources
DefinitionIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom#
There's a natural ring map \(K_v\to L_w\) extending the map \(K\to L\). It is defined by completing the inclusion \(K\to L\) at the finite places \(v\) and \(w\) (which can be done because the previous lemma shows that the map is uniformly continuous for the \(v\)-adic and \(w\)-adic topologies).
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom.
Sources
Uses 1 · Used by 4
LemmaIsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom#
If \(i_v:K_v\to L_w\) denotes the map of the previous definition then for \(x\in K_v\) we have \(e\times w(i(k))=v(k)\), where \(e\) is the ramification index of \(w/v\).
Proof
Follows by continuity from lemma IsDedekindDomain.HeightOneSpectrum.valuation_comap.
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom.
Sources
LemmaIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers#
The map \(i_v:K_v\to L_w\) sends the integer ring \(A_v\) into \(B_w\).
Proof
The integer ring is defined by \(v\geq0\) (or \(v\leq 1\) in mathlib, which uses multiplicative valuations) so the result follows from IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom.
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers.
Sources
Uses 1 · Used by 1
TheoremIsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology#
Giving \(L_w\) the \(K_v\)-algebra structure coming from the natural map \(K_v\to L_w\), the \(w\)-adic topology on \(L_w\) is the \(K_v\)-module topology.
Proof
Any basis for \(L\) as a \(K\)-vector space spans \(L_w\) as a \(K_v\)-module, so \(L_w\) is finite-dimensional over \(K_v\) and the module topology is the same as the product topology. So we need to establish that the product topology on \(L_w=K_v^n\) is the \(w\)-adic topology. But the \(w\)-adic topology is induced by the \(w\)-adic norm, which makes \(L_w\) into a normed \(K_v\)-vector space, and (after picking a basis) the product norm on \(L_w=K_v^n\) also makes \(L_w\) into a normed \(K_v\)-vector space. So the result follows from the standard fact (see for example the lemma on p52 of Cassels-Froelich, formalized as ContinuousLinearEquiv.ofFinrankEq in mathlib) that any two norms on a finite-dimensional vector space over a complete field are equivalent (and thus induce the same topology).
Lean
Stated as IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
Because of the commutative diagram
(A commutative diagram in the source is not reproduced here.)
we can view \(L_w\) as an \(L\otimes_KK_v\)-algebra.
Now instead of fixing \(w\) upstairs, we fix \(v\) downstairs and consider all \(w\) lying over it at once. So say \(v\) is in the height one spectrum of \(A\).
LemmaIsDedekindDomain.HeightOneSpectrum.Extension.finite#
There are only finitely many primes \(w\) of \(B\) lying above \(v\).
Proof
This is a standard fact about Dedekind domains. The key input is mathlib's theorem primesOver_finite.
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.Extension.finite.
Sources
Used by 1
We write \(w|v\) to denote the fact that \(w\) is a prime of \(B\) above \(v\) of \(A\).
DefinitionIsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi#
The product of the maps \(K_v\to L_w\) for \(w|v\) is a natural ring map \(K_v\to\prod_{w|v}L_w\) lying over \(K\to L\).
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi.
Sources
Uses 1 · Used by 1
Because \(K_v\to\prod_{w|v}L_w\) lies over \(K\to L\), there's an induced \(L\)-algebra map \(L\otimes_KK_v\to\prod_{w|v}L_w\). We are now able to state one of the key results in this section. The proof is probably the hardest proof in this section to formalize.
TheoremIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv#
The induced \(L\)-algebra homomorphism \(L\otimes_KK_v\to\prod_{w|v}L_w\) is an isomorphism of rings.
Proof
My current proposal to formalize this is as follows. The map is surjective because the image is dense and closed; this has been formalized already. It is also a \(K_v\)-algebra homomorphism if we give \(L_w\) the obvious \(K_v\)-algebra structure. Thus we can conclude the result if we can prove that both spaces are finite-dimensional and have the same dimension. The \(K_v\)-dimension of \(L\otimes_KK_v\) is equal to the \(K\)-dimension of \(L\), which is \(\sum_{w|v}e_wf_w\) using the standard notation that \(e_w\) is the ramification index of \(w\) and \(f_w\) the residue degree (this result is in mathlib). So it suffices to prove that \([L_w:K_v]=e_wf_w\). We already have that \(e_w\) (defined globally) is equal to the local ramification index (defined as the factor by which the valuations differ on \(K\)). So what is left is to prove that (i) the residue field extension induced by \(L_w/K_v\) has degree is equal to the globally-defined \(f_w\), (ii) an extension of local fields has degree \(ef\). Now (i) sounds straightforward given what we have (the map from \(A\) to \(\mathcal{O}_v\) has kernel \(v\) and dense image) and (ii) is true for any complete discretely-valued field; I am not suggesting we formalize the following proof, but at least it represents a rigorous justification: A field complete with respect to a discrete valuation is stable in the sense of the book by Bosch-Güntzer-Remmert (Prop 3.6.2.1), so every finite extension of such a field is cartesian (def 3.6.1.1) and thus \(ef=n\) (Prop 3.6.2.4, (iii) implies (ii)). Note that if you weaken the hypotheses too much then there are counterexamples; it's possible to have \(ef\lt n\) and BGR goes into details.
Lean
Stated as IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv; the blueprint marks no proof of it as formalized.
Sources
TheoremIsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPi#
For \(v\) fixed, the product topology on \(\prod_{w|v}L_w\) is the \(K_v\)-module topology.
Proof
This is a finite product of \(K_v\)-modules each of which has the \(K_v\)-module topology by IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology, and the product topology is the module topology for a finite product of modules each of which has the module topology (this is in mathlib).
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPi.
Sources
Uses 1
We now start thinking about what's going on at the integral level. We write \(A_v\) for the integers of \(K_v\) and \(B_w\) for the integers of \(L_w\).
TheoremIsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_pi#
The isomorphism \(L\otimes_KK_v\to\prod_{w|v}L_w\) induces an isomorphism \(B\otimes_AA_v\to \prod_{w|v}B_w\) for all \(v\) in the height one spectrum of \(A\).
Proof
Certainly the image of the integral elements are integral. The argument in the other direction is more delicate. My original plan was to follow Cassels–Froehlich, Cassels' article “Global fields”, section 12 lemma, p61, which proves it for all but finitely many primes, but a PR by Matthew Jasper gives another approach which works for all primes. Jasper's argument is to show that the closure of \(A\) in \(K_v\) is \(A_v\) for a valuation on a Dedekind domain, and then that the closure of \(A\) in \(\prod_{v\in S}K_v\) is \(\prod_{v\in S}A_v\) for \(S\) a finite set of valuations (using the Chinese remainder theorem). Applying this to \(B\) we get that the closure of \(B\) in \(\prod_{w|v}L_w\) is \(\prod_{w|v}B_w\). He then shows that this closure is the image of \(B\otimes_A\mathcal{O}_v\) (by showing that this image is closed because it's open), giving surjectivity; injectivity follows from the statement that \(L\otimes_KK_v=\prod_{w|v}L_w\).
Lean
Formalized as IsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_pi.
Sources
A summary of what we have so far: for all finite places \(v\) of \(A\) we have shown that the natural map \(L\otimes_KK_v\to\prod_wL_w\) is an isomorphism of \(L\)-algebras, and that if \(L\otimes_KK_v\) has the \(K_v\)-module topology and each \(L_w\) has the valuation topology then this map is also a homeomorphism. Furthermore we have shown that there is an induced algebraic isomorphism \(B\otimes_AA_v\equiv\prod_w B_w\) on the subrings of the left and right hand sides.
Recall that the finite adeles \(\mathbb{A}_{A,K}^\infty\) is defined in mathlib to be the restricted product of the \(K_v\) with respect to the \(A_v\), equipped with a certain restricted product topology (which is not the subspace topology of the product topology, indeed \(\prod_v A_v\) is open in this topology). We have seen in definition IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom that there's a map \(K_v\to L_w\) if \(w|v\), extending \(K\to L\), and we have seen in theorem IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers that this sends \(A_v\) to \(B_w\). We conclude
DefinitionIsDedekindDomain.FiniteAdeleRing.mapSemialgHom#
There's a natural ring homomorphism \(\mathbb{A}_{A,K}^\infty\to\mathbb{A}_{B,L}^\infty\) lying over \(K\to L\).
Hence there's a natural \(L\)-algebra homomorphism \(L\otimes_K\mathbb{A}_{A,K}^\infty\to\mathbb{A}_{B,L}^\infty\).
Our next goal in this section is the following two results. First the algebraic claim:
TheoremIsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv#
This natural map \(L\otimes_K\mathbb{A}_{A,K}^\infty\to\mathbb{A}_{B,L}^\infty\) is an isomorphism.
Proof
Follows immediately from theorem IsDedekindDomain.FiniteAdeleRing.baseChangeIntegralAlgEquiv and theorem IsDedekindDomain.AKLB.tensorProduct_module_algEquiv.
Lean
Stated as IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv; the blueprint marks no proof of it as formalized.
Sources
Uses 2 · Used by 1
Now \(L\otimes_K\mathbb{A}_{A,K}^\infty\) is an \(\mathbb{A}_{A,K}^\infty\)-module and hence can be given the \(\mathbb{A}_{A,K}^\infty\)-module topology. We also claim
TheoremIsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv#
The induced \(L\)-algebra morphism \(L\otimes_K\mathbb{A}_{A,K}^\infty\to\mathbb{A}_{B,L}^\infty\) is a topological isomorphism.
Lean
Stated as IsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv; the blueprint marks no proof of it as formalized.
Sources
Informally, the proofs are simple: componentwise we know that \(L\otimes_KK_v\) is isomorphic both algebraically and topologically to \(\prod_{w|v}L_w\), and that this isomorphism sends the open set \(B\otimes_AA_v\) homeomorphically onto \(\prod_{w|v}B_w\), so now it's “just a case of putting everything together”. Formally, we really need to spell this out, as there is a lot going on. We do this in the next subsection.
Base change for nonarchimedean completions.
As usual we are in the AKLB set-up, so in particular \(K\) is the field of fractions of the Dedekind domain \(A\), \(L/K\) is a finite separable extension, and \(B\) is the integral closure of \(A\) in \(L\). The goal in this subsection is to spell out the following argument: Assume that \(L\otimes_KK_v\cong\prod_{w|v}L_w\) algebraically and topologically for all \(v\), with \(B\otimes_AA_v\) identified with \(\prod_{w|v}B_w\). Then \(L\otimes_K\mathbb{A}_K^\infty\cong\mathbb{A}_L^\infty\), algebraically and topologically. Here the tensor products \(L\otimes_K R\) (for \(R\) a \(K\)-algebra with a topology) are all being given the \(R\)-module topology, which if we choose a basis for \(L/K\) is just the product topology.
We start with the following observation. If \(M\) is a \(K\)-module then there's a canonical map \(B\otimes_AM\to L\otimes_KM\) sending \(b\otimes m\) to \(b\otimes m\) (this follows from the universal property of the tensor product). Our first goal is to show that this map is an isomorphism. Let us establish some lemmas first.
CorollaryIsDedekindDomain.AKLB.tensorProduct_module_algEquiv#
If \(M\) is any \(K\)-module then the canonical map \(B\otimes_A M\to L\otimes_K M\) is an isomorphism.
Proof
We can factor this map as \(B\otimes_AM\cong B\otimes_A(K\otimes_KM)\cong (B\otimes_A K)\cong_KM\to L\otimes_KM\) and we just showed that the latter map was an isomorphism.
Lean
Formalized as IsDedekindDomain.linearEquivTensorProductModule.
Sources
Used by 1
We now need to explain how tensor products sometimes commute with restricted products.
Recall that \(\mathbb{A}_K^\infty\) is the finite adeles of \(K\), defined as the restricted product of the \(K_v\) with respect to the \(A_v\), where \(v\) runs through the nonzero primes of \(A\). Let \(R\) denote the restricted product of the \(B\otimes_A K_v\) with respect to the \(B\otimes_A A_v\).
Recall from earlier in this section that if \(v\) is a finite place of \(A\) then the natural map from \(B\otimes_A K_v\) to \(L\otimes_KK_v\) is an isomorphism, and recall from the previous section that the natural map from \(L\otimes_KK_v\) to \(\prod_{w|v}L_w\) was also an isomorphism. This isomorphism sends \(B\otimes_A A_v\) to \(\prod_{w|v}B_w\) (I thank Matthew Jasper for pointing out to me that this statement was true at all primes, not just at unramified primes). Finally, the set of \(w\) of \(B\) dividing a fixed place \(v\) of \(A\) is finite. Let's now formalize the abstract statement which we need. Rather than following the notation for restricted product in the literature and writing \(\mathbb{A}_K^\infty=\prod'_vK_v\) with the \(\mathcal{O}_v\) implicit, we will write \(\prod'_v(K_v,\mathcal{O}_v)\) in the below.
Because this map factors through the isomorphism \(B\otimes_A\mathbb{A}_K^\infty\to L\otimes_K\mathbb{A}_K^\infty\) we can finally deduce that the natural map \(L\otimes_K\mathbb{A}_K^\infty\to\mathbb{A}_L^\infty\) is an algebraic isomorphism.
The proof of Theorem IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv is shown with its statement.
We still need to talk about topologies though, so let's finish by doing this. Let's start with some trivialities, expressed as definitions rather than theorems because they're constructions.
We now allow a slight change of index set. Unfortunately I don't think that we can deduce the results just stated above from this one, in Lean, because the product of \(Y_w\) over a set of size 1 is not definitionally equal to \(Y_w\).
Recall definition RestrictedProduct.relabelIso, giving us a bijection between two restricted products.
Recall that if
is a commutative ring, and two
-modules both have the
-module topology, then any
-linear morphism between them is automatically continuous. We know that \(\mathbb{A}_L^\infty\) is \(\mathbb{A}_K^\infty\)-linearly isomorphic to \(L\otimes_K\mathbb{A}_K^\infty\) and our claim is that if \(L\otimes_K\mathbb{A}_K^\infty\) is given the \(\mathbb{A}_K^\infty\)-module topology then this isomorphism is also a homeomorphism; to prove this, we thus just need to check that \(\mathbb{A}_L^\infty\) has the \(\mathbb{A}_K^\infty\)-module topology. Equivalently, by the previous result, we need to check that the restricted product topology on the \(\mathbb{A}_K^\infty\)-algebra \(\prod'_v(B\otimes_AK_v,B\otimes_AA_v)\) is the \(\mathbb{A}_K^\infty\)-module topology.
We now need to make restricted products of modules into modules over restricted product of rings. The API, which should be straightforward so we don't give details here, is: if \(R_v\) are rings with subrings \(S_v\) and if \(M_v\) are \(R_v\)-modules with \(S_v\)-stable submodules \(N_v\), then \(\prod'_v(M_v,N_v)\) is naturally a module over \(\prod'_v(R_v,S_v)\), and that \(R_v\)-morphisms \(M_v\to M_v'\) sending \(N_v\) to \(N_v'\) induce \(\prod'_v(R_s,S_v)\)-linear maps \(\prod'_v(M_v,N_v)\to\prod'_v(M'_v,N'_v)\). From this one deduces that isomorphisms on the factors induce isomorphisms on the restricted products.
Now \(A_v\) is a PID, so \(B\otimes_AA_v\) is free (as it is finitely-generated and torsion-free). This means that there is an isomorphism \(B\otimes_AA_v\cong(A_v)^n\), which extends to an isomorphism \(B\otimes_AK_v\cong K_v^n\). These isomorphisms are also homeomorphisms. If we fix such isomorphisms for all \(v\) then we get an induced \(\mathbb{A}_K^\infty\)-module isomorphism + homeomorphism \(\prod'_v(B\otimes_AK_v,B\otimes_AA_v)=\prod'_v(K_n^n,A_v^n)\). So it suffices to prove that the \(\prod'_v(K_v,A_v)\)-module \(\prod'_v(K_v^n,A_v^n)\) has the \(\prod'_v(K_v,A_v)\)-module topology. This follows from the fact that the product topology on two modules with the module topology is the module topology (a fact in mathlib) and the following result.
As a corollary one can prove by induction on \(n\) that the restricted product of \(n\)th powers is homeomorphic to the \(n\)th power of the restricted product and this is the result we require.
Base change for infinite adeles
Recall that if \(K\) is a number field then the infinite adeles of \(K\) are defined to be the product \(\prod_{v\mid\infty} K_v\) of all the completions of \(K\) at the infinite places.
The result we need here is that if \(L/K\) is a finite extension of number fields, then the map \(K\to L\) extends to a continuous \(K\)-algebra map \(K_\infty\to L_\infty\), and thus to a continuous \(L\)-algebra isomorphism \(L\otimes_KK_\infty\to L_\infty\). Perhaps a cheap proof would be to deduce it from the fact that \(K_\infty=K\otimes_{\mathbb{Q}}\mathbb{R}\).
The overall strategy is to first establish, for each infinite place \(v\) of \(K\), homeomorphisms between for the completion \(K_v\) and the product \(\prod_{w\mid v}L_w\) of completions of \(L\) at all infinite places \(w\) of \(L\) lying above \(v\). We then use these homeomorphisms to construct base change for the infinite adele ring.
Weak approximation at infinite places
First, we require a preliminary result that \(K\) is dense inside any product of completions \(\prod_{v\in S} K_v\) of \(K\) at infinite places.
TheoremNumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi#
Let \(S\) be a set of infinite places of \(K\). The image of \(K\) under the embedding \(K\hookrightarrow (K_v)_{v\in S}; k \mapsto (k)_v\) is dense in the product topology.
Proof
Let \((K, v)\) denote \(K\) equipped with the topology induced by the infinite place \(v\). It suffices to show that the image of \(K\) under the embedding \(K\hookrightarrow \prod_{v\mid \infty}(K, v)\) is dense in the product topology. By a standard analytic argument, for each \(v\) it is possible to select a sequence \((x_n^{(v)})_n\) with the property that \(x_n^{(v)} \to 1\) in \(v\)'s topology, while \(x_n^{(v)} \to 0\) in any other infinite place's topology. Let \((z_v)_v \in \prod_{v\mid \infty}(K, v)\). For each \(v\), the sequence \(y_n := \sum_{v\mid\infty} x_n^{(v)}z_v\) in \(K\) converges to \(z_v\) in \(v\)'s topology. So the embedded image of \(y_n\) in \(\prod_{v\mid \infty}(K, v)\) converges to \((z_v)_v\) in the product topology.
Lean
Stated as NumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi; the blueprint marks no proof of it as formalized.
Sources
Used by 1
Base change at infinite places
DefinitionNumberField.InfinitePlace.Completion.piExtension#
Let \(v\) be an infinite place of \(K\). There is a continuous \(K\)-algebra homomorphism \(K_v \to \prod_{w\mid v}L_w\), whose restriction to \(K\) corresponds to the global embedding of \(K\) into \((L_w)_w\).
Used by 1
The map in NumberField.InfinitePlace.Completion.piExtension can be lifted to an \(L\)-algebra homomorphism defined on \(L\otimes_K K_v\).
DefinitionNumberField.InfinitePlace.Completion.baseChange#
Let \(v\) be an infinite place of \(K\). There is a natural \(L\)-algebra homomorphism \(L\otimes_K K_v \to \prod_{w\mid v}L_w\), whose restriction to \(1\otimes_K K_v\) corresponds to the map in NumberField.InfinitePlace.Completion.piExtension.
Uses 1 · Used by 1
TheoremNumberField.InfinitePlace.Completion.baseChange_surjective#
For a fixed infinite place \(v\) of \(K\), the map \(L\otimes_K K_v \to\prod_{w\mid v}L_w\) is surjective.
Proof
Let \((x_i)_i\) be a \(K_v\)-basis of \(\prod_{w\mid v}L_w\). By the density of \(L\) in \(\prod_{w\mid v}L_w\) (Theorem NumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi), we can find \(\alpha_i \in L\) arbitrarily close to \(x_i\prod_{w\mid v}L_w\) with respect to the sup norm when embedded globally in \(\prod_{w\mid v}L_w\). In particular, it is possible to choose such \(\alpha_i\) so that the matrix representing the vector \(((\alpha_i)_{w \mid v})_i\) in the basis \((x_i)_i\) has non-zero determinant. Since \((\alpha_i)_{w \mid v}\) is the image of \(1\otimes \alpha_i\) under base change, we have that \((1 \otimes \alpha_i)_i\) also forms a basis of \(L\otimes_K K_v\), and base change is surjective.
Lean
Stated as NumberField.InfinitePlace.Completion.baseChange_surjective; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
TheoremNumberField.InfinitePlace.Completion.baseChange_injective#
For a fixed infinite place \(v\) of \(K\), the map \(L\otimes_K K_v \to\prod_{w\mid v}L_w\) is injective.
Proof
The \(L\)-algebra map \(L\otimes_K K_v \to\prod_{w\mid v}L_w\) can equivalently be thought of as \(K_v\)-linear, which is injective, because it is surjective by Theorem NumberField.InfinitePlace.Completion.baseChange_surjective, and both side have the same \(K_v\)-dimension by Theorem NumberField.InfinitePlace.Completion.finrank_pi_eq_finrank_tensorProduct.
Lean
Stated as NumberField.InfinitePlace.Completion.baseChange_injective; the blueprint marks no proof of it as formalized.
Sources
Used by 1
We have established that the map of Definition NumberField.InfinitePlace.Completion.baseChange gives an \(L\)-algebra isomorphism between \(L\otimes_K K_v\) and \(\prod_{w\mid v}L_w\). The left-hand side is given the \(K_v\)-module topology, while we show that the right-hand side also has the \(K_v\)-module topology.
TheoremNumberField.InfinitePlace.Completion.instIsModuleTopologyValEqComapAlgebraMap_fLT#
If \(w \mid v\) is an infinite place of \(L\) lying above the infinite place \(v\) of \(K\), then \(L_w\) has the \(K_v\)-module topology.
Proof
Because \(L_w\) is a finite-dimensional normed \(K_v\) vector space, there exists a \(K_v\)-linear linear homeomorphism \(L_w \cong K_v^n\), from which \(L_w\) has the \(K_v\)-module topology.
Lean
Stated as NumberField.InfinitePlace.Completion.instIsModuleTopologyValEqComapAlgebraMap_fLT; the blueprint marks no proof of it as formalized.
Sources
Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.