Documentation

TauCeti.NumberTheory.NumberField.Global.Places.Connected

Connectedness in the unit groups of archimedean completions #

Let w be an infinite place of a number field K. The completion w.Completion is isometric to ℝ when w is real and to ℂ when w is complex. Consequently the unit group w.Completionˣ is connected at a complex place, being homeomorphic to ℂˣ, while at a real place the units of positive real part form a preconnected set, homeomorphic to the positive half-line.

These are the archimedean inputs to the description of the open subgroups of the idele class group: an open subgroup is also closed, so it contains every connected set of ideles through the identity, and in particular the whole unit group at each complex place and the positive units at each real place.

Main results #

source
@[simp]
theorem NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex_apply {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) (x : w.Completion) :
(isometryEquivComplexOfIsComplex hw) x = (extensionEmbedding w) x

The isometry w.Completion ≃ᵢ ℂ of a complex place evaluates to the extension embedding. This records the definition of isometryEquivComplexOfIsComplex, whose underlying equivalence is ringEquivComplexOfIsComplex hw.

source
@[simp]
theorem NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal_apply {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : w.Completion) :
(isometryEquivRealOfIsReal hw) x = (extensionEmbeddingOfIsReal hw) x

The isometry w.Completion ≃ᵢ ℝ of a real place evaluates to the real extension embedding. This records the definition of isometryEquivRealOfIsReal, whose underlying equivalence is ringEquivRealOfIsReal hw.

source
noncomputable def NumberField.InfinitePlace.Completion.continuousMulEquivComplexOfIsComplex {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) :
w.Completion ≃ₜ* ℂ

The continuous multiplicative isomorphism w.Completion ≃ₜ* ℂ of a complex place. Its underlying map is the ring isomorphism ringEquivComplexOfIsComplex hw, which respects open sets because it is the isometry isometryEquivComplexOfIsComplex hw.

Instances For
    source
    @[simp]
    theorem NumberField.InfinitePlace.Completion.continuousMulEquivComplexOfIsComplex_apply {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) (x : w.Completion) :
    (continuousMulEquivComplexOfIsComplex hw) x = (extensionEmbedding w) x

    The continuous multiplicative isomorphism w.Completion ≃ₜ* ℂ of a complex place evaluates to the extension embedding.

    source
    noncomputable def NumberField.InfinitePlace.Completion.continuousMulEquivRealOfIsReal {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) :
    w.Completion ≃ₜ* ℝ

    The continuous multiplicative isomorphism w.Completion ≃ₜ* ℝ of a real place. Its underlying map is the ring isomorphism ringEquivRealOfIsReal hw, which respects open sets because it is the isometry isometryEquivRealOfIsReal hw.

    Instances For
      source
      @[simp]
      theorem NumberField.InfinitePlace.Completion.continuousMulEquivRealOfIsReal_apply {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : w.Completion) :
      (continuousMulEquivRealOfIsReal hw) x = (extensionEmbeddingOfIsReal hw) x

      The continuous multiplicative isomorphism w.Completion ≃ₜ* ℝ of a real place evaluates to the real extension embedding.

      source
      @[simp]
      theorem NumberField.InfinitePlace.Completion.extensionEmbedding_continuousMulEquivComplexOfIsComplex_symm {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) (z : ℂ) :
      (extensionEmbedding w) ((continuousMulEquivComplexOfIsComplex hw).symm z) = z

      The extension embedding inverts the continuous multiplicative isomorphism w.Completion ≃ₜ* ℂ of a complex place.

      source
      @[simp]
      theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_continuousMulEquivRealOfIsReal_symm {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : ℝ) :
      (extensionEmbeddingOfIsReal hw) ((continuousMulEquivRealOfIsReal hw).symm x) = x

      The real extension embedding inverts the continuous multiplicative isomorphism w.Completion ≃ₜ* ℝ of a real place.

      source
      @[simp]
      theorem NumberField.InfinitePlace.Completion.norm_continuousMulEquivComplexOfIsComplex_symm {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) (z : ℂ) :
      ‖(continuousMulEquivComplexOfIsComplex hw).symm z‖ = ‖z‖

      The inverse of the continuous multiplicative isomorphism w.Completion ≃ₜ* ℂ of a complex place preserves norms.

      source
      @[simp]
      theorem NumberField.InfinitePlace.Completion.norm_continuousMulEquivRealOfIsReal_symm {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : ℝ) :
      ‖(continuousMulEquivRealOfIsReal hw).symm x‖ = |x|

      The inverse of the continuous multiplicative isomorphism w.Completion ≃ₜ* ℝ of a real place takes a real number to an element of the same absolute value.

      source
      theorem NumberField.InfinitePlace.Completion.connectedSpace_units_of_isComplex {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) :
      ConnectedSpace w.Completionˣ

      The unit group of a complex completion is connected: it is homeomorphic to ℂˣ through continuousMulEquivComplexOfIsComplex hw.

      source
      theorem NumberField.InfinitePlace.Completion.isPreconnected_setOf_extensionEmbeddingOfIsReal_pos {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) :
      IsPreconnected {u : w.Completionˣ | 0 < (extensionEmbeddingOfIsReal hw) ↑u}

      The positive units of a real completion form a preconnected set: they are homeomorphic to the positive real half-line.