Embeddings of number fields

This file defines an indirect approach to the completion of a number field with respect to an infinite place. While this suffices for the proof of the local compactness of the adele ring, we have identified deficiencies with this approach, detailed in the implementation notes below. We keep this approach here for reference.

Main definitions

• NumberField.InfinitePlace.completion' is the (indirect) Archimedean completion of a number field as an infinite place, obtained by embedding as a subfield of ℂ and completing this subfield.

Main results

• NumberField.InfinitePlace.Completion.locallyCompactSpace' : the (indirect) 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 the principal approach taken in Embeddings.lean, 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 this file. It leads to an isomorphic field completion to the direct approach, since both define abstract completions. However, the API for the alternative approach in this file 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

def NumberField.InfinitePlace.subfield (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Subfield ℂ

The embedding of K as a subfield in ℂ using the embedding associated to the infinite place v.

Equations

• NumberField.InfinitePlace.subfield K v = { toSubring := RingHom.range (NumberField.InfinitePlace.embedding v), inv_mem' := ⋯ }

def NumberField.InfinitePlace.toSubfield (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : K →+* ↥(NumberField.InfinitePlace.subfield K v)

The embedding sending a number field to its subfield in ℂ.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.InfinitePlace.toSubfield_injective (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Function.Injective ⇑(NumberField.InfinitePlace.toSubfield K v)

theorem NumberField.InfinitePlace.toSubfield_surjective (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Function.Surjective ⇑(NumberField.InfinitePlace.toSubfield K v)

def NumberField.InfinitePlace.subfieldEquiv (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : K ≃+* ↥(NumberField.InfinitePlace.subfield K v)

Equations

• NumberField.InfinitePlace.subfieldEquiv K v = RingEquiv.ofBijective (NumberField.InfinitePlace.toSubfield K v) ⋯

instance NumberField.InfinitePlace.subfield_uniformSpace (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : UniformSpace ↥(NumberField.InfinitePlace.subfield K v)

Equations

• NumberField.InfinitePlace.subfield_uniformSpace K v = inferInstance

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

The completion of a number field at an Archimedean place.

Equations

• NumberField.InfinitePlace.completion' K v = UniformSpace.Completion ↥(NumberField.InfinitePlace.subfield K v)

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 ↥(NumberField.InfinitePlace.subfield K v)

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

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.Completion.instNormedDivisionRingSubtypeComplexMemSubfieldToDivisionRingToNormedDivisionRingInstNormedFieldComplexInstMembershipInstSetLikeSubfieldSubfield (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : NormedDivisionRing ↥(NumberField.InfinitePlace.subfield K v)

Equations

• One or more equations did not get rendered due to their size.

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.instTopologicalRingCompletion'ToTopologicalSpaceInstUniformSpaceCompletion'ToNonUnitalNonAssocRingToNonUnitalNonAssocCommRingToNonUnitalCommRingToCommRingToEuclideanDomainInstFieldCompletion' (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.instT0SpaceCompletion'ToTopologicalSpaceInstUniformSpaceCompletion' (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : T0Space (NumberField.InfinitePlace.completion' K v)

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.Completion.instCoeSubtypeComplexMemSubfieldToDivisionRingToNormedDivisionRingInstNormedFieldComplexInstMembershipInstSetLikeSubfieldSubfieldCompletion' (K : Type u_1) [Field K] (v : NumberField.InfinitePlace K) : Coe (↥(NumberField.InfinitePlace.subfield K v)) (NumberField.InfinitePlace.completion' K v)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• NumberField.InfinitePlace.Completion.instCoeCompletion' K v = { coe := ↑↥(NumberField.InfinitePlace.subfield K v) ∘ ⇑(NumberField.InfinitePlace.toSubfield K v) }

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 = RingHom.comp UniformSpace.Completion.coeRingHom (NumberField.InfinitePlace.toSubfield K v)

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

The embedding v.completion' K → ℂ of a completion of a number field at an Archimedean place into ℂ.

Equations

• NumberField.InfinitePlace.Completion.extensionEmbedding' K v = UniformSpace.Completion.extensionHom (Subfield.subtype (NumberField.InfinitePlace.subfield K 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 → ℂ preserves distances.

theorem NumberField.InfinitePlace.Completion.embedding_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.embedding_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 indirect completion of a number field at an Archimedean place is locally compact.

Equations

• ⋯ = ⋯