ProCGroups.Completion.UniversalProperty

8 Theorem | 3 Definition | 1 Structure

This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.

Open this file on GitHub

import

ProCGroups.ProC.GroupPredicate

Imported by

Structure ProCGroups.Completion.IsProCCompletion GitHub

structure IsProCCompletion
    (ProC : ProCGroups.ProC.ProCGroupPredicate)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (Ghat : Type u) [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
    (ι : G →ₜ* Ghat) : Prop where
  isProC : ProC (G := Ghat)
  denseRange : DenseRange ι
  existsUnique_lift :
    ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H],
      ProC (G := H) →
      ∀ (φ : G →ₜ* H), ∃! φbar : Ghat →ₜ* H, φbar.comp ι = φ

An abstract pro-\(C\) completion of a topological group.

Definition ProCGroups.Completion.IsProCCompletion.lift GitHub

noncomputable def lift
    (hι : IsProCCompletion ProC G Ghat ι)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (hH : ProC (G := H)) (φ : G →ₜ* H) :
    Ghat →ₜ* H :=
  Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hH φ))

A continuous homomorphism from the source group to a pro-\(C\) target factors uniquely through the pro-\(C\) completion.

Theorem ProCGroups.Completion.IsProCCompletion.lift_spec GitHub

theorem lift_spec
    (hι : IsProCCompletion ProC G Ghat ι)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (hH : ProC (G := H)) (φ : G →ₜ* H) :
    (hι.lift hH φ).comp ι = φ

The universal-property lift is continuous and extends the given homomorphism along the completion map.

Show proof

Theorem ProCGroups.Completion.IsProCCompletion.lift_unique GitHub

theorem lift_unique
    (hι : IsProCCompletion ProC G Ghat ι)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (hH : ProC (G := H)) (φ : G →ₜ* H)
    {f : Ghat →ₜ* H} (hfac : f.comp ι = φ) :
    f = hι.lift hH φ

The universal-property lift is the unique continuous map extending the given homomorphism.

Show proof

Theorem ProCGroups.Completion.IsProCCompletion.hom_ext GitHub

theorem hom_ext
    (hι : IsProCCompletion ProC G Ghat ι)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (hH : ProC (G := H))
    {f g : Ghat →ₜ* H}
    (hfg : f.comp ι = g.comp ι) :
    f = g

Continuous homomorphisms out of a pro-\(C\) completion are determined by their composites with the dense source map.

Show proof

Theorem ProCGroups.Completion.IsProCCompletion.lift_self_eq_id GitHub

@[simp] theorem lift_self_eq_id
    (hι : IsProCCompletion ProC G Ghat ι) :
    hι.lift hι.isProC ι = ContinuousMonoidHom.id Ghat

The lift of the completion map to the completion itself is the identity.

Show proof

Definition ProCGroups.Completion.IsProCCompletion.comparison GitHub

noncomputable def comparison
    (h₁ : IsProCCompletion ProC G Ghat ι)
    (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) : Ghat →ₜ* Ghat₂ :=
  h₁.lift h₂.isProC ι₂

The canonical comparison map between two pro-\(C\) completions of the same group.

Theorem ProCGroups.Completion.IsProCCompletion.comparison_spec GitHub

theorem comparison_spec
    (h₁ : IsProCCompletion ProC G Ghat ι)
    (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) :
    (h₁.comparison h₂).comp ι = ι₂

The comparison map between two pro-\(C\) completions agrees with the second completion map on the source.

Show proof

Theorem ProCGroups.Completion.IsProCCompletion.comparison_comp_eq_id GitHub

@[simp 900] theorem comparison_comp_eq_id
    (h₁ : IsProCCompletion ProC G Ghat ι)
    (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) :
    (h₂.comparison h₁).comp (h₁.comparison h₂) = ContinuousMonoidHom.id Ghat

The two comparison maps between pro-\(C\) completions compose to the identity.

Show proof

Definition ProCGroups.Completion.IsProCCompletion.continuousMulEquiv GitHub

noncomputable def continuousMulEquiv
    (h₁ : IsProCCompletion ProC G Ghat ι)
    (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) : Ghat ≃ₜ* Ghat₂ :=
  let f : Ghat →ₜ* Ghat₂ := h₁.comparison h₂
  let g : Ghat₂ →ₜ* Ghat := h₂.comparison h₁
  { toMulEquiv :=
      { toFun := f
        invFun := g
        left_inv := by
          intro x
          have hgf : g.comp f = ContinuousMonoidHom.id Ghat := h₁.comparison_comp_eq_id h₂
          exact congrArg (fun h : Ghat →ₜ* Ghat => h x) hgf
        right_inv := by
          intro x
          have hfg : f.comp g = ContinuousMonoidHom.id Ghat₂ := h₂.comparison_comp_eq_id h₁
          exact congrArg (fun h : Ghat₂ →ₜ* Ghat₂ => h x) hfg
        map_mul' := f.map_mul }
    continuous_toFun := f.continuous_toFun
    continuous_invFun := g.continuous_toFun }

The canonical multiplicative homeomorphism between two pro-\(C\) completions of the same topological group.

Theorem ProCGroups.Completion.IsProCCompletion.continuousMulEquiv_apply_completionMap GitHub

@[simp] theorem continuousMulEquiv_apply_completionMap
    (h₁ : IsProCCompletion ProC G Ghat ι)
    (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) (x : G) :
    h₁.continuousMulEquiv h₂ (ι x) = ι₂ x

The canonical equivalence between pro-\(C\) completions sends one completion map to the other.

Show proof

Theorem ProCGroups.Completion.IsProCCompletion.continuousMulEquiv_symm_apply_completionMap GitHub

@[simp] theorem continuousMulEquiv_symm_apply_completionMap
    (h₁ : IsProCCompletion ProC G Ghat ι)
    (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) (x : G) :
    (h₁.continuousMulEquiv h₂).symm (ι₂ x) = ι x

The inverse canonical equivalence between pro-\(C\) completions sends the second completion map back to the first.

Show proof

ProCGroups.Completion.UniversalProperty

Declarations