Embeddings of number fields

This file defines the main approach to the completion of a number field with respect to an infinite place.

Main definitions

• NumberField.InfinitePlace.completion is the Archimedean completion of a number field as an infinite place, obtained by defining a uniform space structure inherited from ℂ via the embedding associated to an infinite place.

Main results

• NumberField.InfinitePlace.Completion.locallyCompactSpace : the Archimedean completion of a number field is locally compact.

Implementation notes

• We have identified two approaches for formalising the completion of a number field K at an infinite place v. One is to define an appropriate uniform structure on K directly, and apply the UniformSpace.Completion functor to this. To show that the resultant completion is a field requires one to prove that K has a completableTopField instance with this uniform space. This approach is taken in this file, namely we pullback the uniform structure on ℂ via the embedding associated to an infinite place, through UniformSpace.comap. In such a scenario, the completable topological field instance from ℂ transfers to K, which we show in Topology/UniformSpace/UniformEmbedding.lean
• The alternative approach is to use the embedding associated to an infinite place to embed K to a Subfield ℂ term, which already has a CompletableTopField instance. We complete K indirectly by applying the UniformSpace.Completion functor to the Subfield ℂ term. This is the approach taken in EmbeddingsAlt.lean. It leads to an isomorphic field completion to the direct approach, since both define abstract completions. However, the API for the alternative approach is deficient, because we lose any UniformSpace.Completion constructions which transfer properties of the base field K to its completion; for example, UniformSpace.Completion.extension which extends a uniform continuous map on K to one on its completion. These would have to be re-established.

Tags

number field, embeddings, places, infinite places

instance NumberField.InfinitePlace.instInhabitedInfinitePlace (K : Type u_1) [Field K] [NumberField K] : Inhabited (NumberField.InfinitePlace K)

Equations

• NumberField.InfinitePlace.instInhabitedInfinitePlace K = { default := Classical.choice ⋯ }

def NumberField.InfinitePlace.normedDivisionRing {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : NormedDivisionRing K

Equations

• NumberField.InfinitePlace.normedDivisionRing v = NormedDivisionRing.induced K ℂ (NumberField.InfinitePlace.embedding v) ⋯

instance NumberField.InfinitePlace.uniformSpace {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : UniformSpace K

Equations

• NumberField.InfinitePlace.uniformSpace v = UniformSpace.comap (⇑(NumberField.InfinitePlace.embedding v)) inferInstance

instance NumberField.InfinitePlace.uniformAddGroup {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : UniformAddGroup K

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.topologicalSpace {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : TopologicalSpace K

Equations

• NumberField.InfinitePlace.topologicalSpace v = UniformSpace.toTopologicalSpace

instance NumberField.InfinitePlace.topologicalDivisionRing {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : TopologicalDivisionRing K

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.topologicalRing {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : TopologicalRing K

Equations

• ⋯ = ⋯

theorem NumberField.InfinitePlace.uniformEmbedding {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : UniformEmbedding ⇑(NumberField.InfinitePlace.embedding v)

theorem NumberField.InfinitePlace.uniformInducing {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : UniformInducing ⇑(NumberField.InfinitePlace.embedding v)

instance NumberField.InfinitePlace.pseudoMetricSpace {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : PseudoMetricSpace K

Equations

• NumberField.InfinitePlace.pseudoMetricSpace v = UniformInducing.comapPseudoMetricSpace ⇑(NumberField.InfinitePlace.embedding v) ⋯

theorem NumberField.InfinitePlace.isometry {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : Isometry ⇑(NumberField.InfinitePlace.embedding v)

theorem NumberField.InfinitePlace.uniformContinuous {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : UniformContinuous ⇑(NumberField.InfinitePlace.embedding v)

theorem NumberField.InfinitePlace.continuous {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : Continuous ⇑(NumberField.InfinitePlace.embedding v)

instance NumberField.InfinitePlace.t0Space {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : T0Space K

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.completableTopField {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : CompletableTopField K

Equations

• ⋯ = ⋯

def NumberField.InfinitePlace.completion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Type u_1

The completion of a number field at an infinite place.

Equations

• NumberField.InfinitePlace.completion K v = UniformSpace.Completion K

instance NumberField.InfinitePlace.Completion.instUniformSpaceCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : UniformSpace (NumberField.InfinitePlace.completion K v)

Equations

• NumberField.InfinitePlace.Completion.instUniformSpaceCompletion K v = UniformSpace.Completion.uniformSpace K

instance NumberField.InfinitePlace.Completion.instCompleteSpaceCompletionInstUniformSpaceCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : CompleteSpace (NumberField.InfinitePlace.completion K v)

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.Completion.instFieldCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Field (NumberField.InfinitePlace.completion K v)

Equations

• NumberField.InfinitePlace.Completion.instFieldCompletion K v = UniformSpace.Completion.instField

instance NumberField.InfinitePlace.Completion.instInhabitedCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Inhabited (NumberField.InfinitePlace.completion K v)

Equations

• NumberField.InfinitePlace.Completion.instInhabitedCompletion K v = { default := 0 }

instance NumberField.InfinitePlace.Completion.instTopologicalRingCompletionToTopologicalSpaceInstUniformSpaceCompletionToNonUnitalNonAssocRingToNonUnitalNonAssocCommRingToNonUnitalCommRingToCommRingToEuclideanDomainInstFieldCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : TopologicalRing (NumberField.InfinitePlace.completion K v)

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.Completion.instDistCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Dist (NumberField.InfinitePlace.completion K v)

Equations

• NumberField.InfinitePlace.Completion.instDistCompletion K v = UniformSpace.Completion.instDistCompletionToUniformSpace

instance NumberField.InfinitePlace.Completion.instT0SpaceCompletionToTopologicalSpaceInstUniformSpaceCompletion (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : T0Space (NumberField.InfinitePlace.completion K v)

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.Completion.metricSpace (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : MetricSpace (NumberField.InfinitePlace.completion K v)

Equations

• NumberField.InfinitePlace.Completion.metricSpace K v = UniformSpace.Completion.instMetricSpace

def NumberField.InfinitePlace.Completion.coeRingHom (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : K →+* NumberField.InfinitePlace.completion K v

Equations

• NumberField.InfinitePlace.Completion.coeRingHom K v = UniformSpace.Completion.coeRingHom

def NumberField.InfinitePlace.Completion.extensionEmbedding (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : UniformSpace.Completion K →+* ℂ

The embedding associated to an infinite place extended to v.completion K →+* ℂ.

Equations

• NumberField.InfinitePlace.Completion.extensionEmbedding K v = UniformSpace.Completion.extensionHom (NumberField.InfinitePlace.embedding v) ⋯

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_injective (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Function.Injective ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding K v)

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_dist_eq {K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (x : NumberField.InfinitePlace.completion K v) (y : NumberField.InfinitePlace.completion K v) : dist ((NumberField.InfinitePlace.Completion.extensionEmbedding K v) x) ((NumberField.InfinitePlace.Completion.extensionEmbedding K v) y) = dist x y

The embedding v.completion K → ℂ is an isometry.

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_isometry (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Isometry ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding K v)

The embedding v.completion K → ℂ is an isometry.

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_uniformInducing (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : UniformInducing ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding K v)

The embedding v.completion K → ℂ is uniform inducing.

theorem NumberField.InfinitePlace.Completion.closedEmbedding (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : ClosedEmbedding ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding K v)

The embedding v.completion K → ℂ is a closed embedding.

instance NumberField.InfinitePlace.Completion.locallyCompactSpace (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : LocallyCompactSpace (NumberField.InfinitePlace.completion K v)

The completion of a number field at an infinite place is locally compact.

Equations

• ⋯ = ⋯