Module

UniversalProperty.lean

Nyll.ProCGroups.Completion.UniversalProperty

12 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Completion / Universal Property

This module defines the universal property of a pro-\(C\) completion and proves the resulting lift, uniqueness, comparison, and canonical-equivalence results.

Imports1

Nyll.ProCGroups.ProC.InverseLimits.Predicates

Imported by4

structure

IsProCCompletion

L25 ↗

ProCGroups.Completion.IsProCCompletion

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}

Lean source · full declaration

structure IsProCCompletion
    (C : ProCGroups.FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (Ghat : Type u) [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
      [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
    (ι : G →ₜ* Ghat) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in the completed
  group.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C Ghat
  /-- The image of the original group under the completion map is dense in `Ghat`. -/
  denseRange : DenseRange ι
  /--
  Every continuous homomorphism from `G` to a pro-`C` target extends uniquely to a continuous
  homomorphism from `Ghat`.
  -/
  existsUnique_lift :
    ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
      [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (H) →
      ∀ (φ : G →ₜ* H), ∃! φbar : Ghat →ₜ* H, φbar.comp ι = φ

def

lift

L59 ↗

ProCGroups.Completion.IsProCCompletion.lift

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}

Lean source · statement

def lift
    (hι : IsProCCompletion C G Ghat ι)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H)) (φ : G →ₜ* H) :
    Ghat →ₜ* H

theorem

lift_spec

L71 ↗

ProCGroups.Completion.IsProCCompletion.lift_spec

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}

Lean source · statement

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

theorem

lift_unique

L80 ↗

ProCGroups.Completion.IsProCCompletion.lift_unique

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}

Lean source · statement

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

theorem

hom_ext

L93 ↗

ProCGroups.Completion.IsProCCompletion.hom_ext

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}

Lean source · statement

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

theorem

lift_self_eq_id

L104 ↗

ProCGroups.Completion.IsProCCompletion.lift_self_eq_id

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}

Lean source · statement

theorem lift_self_eq_id
    (hι : IsProCCompletion C G Ghat ι) :
    hι.lift hι.hasOpenNormalBasisInClass ι = ContinuousMonoidHom.id Ghat

def

comparison

L115 ↗

ProCGroups.Completion.IsProCCompletion.comparison

Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}
variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
variable {ι₂ : G →ₜ* Ghat₂}

Lean source · statement

def comparison
    (h₁ : IsProCCompletion C G Ghat ι)
    (h₂ : IsProCCompletion C G Ghat₂ ι₂) : Ghat →ₜ* Ghat₂

theorem

comparison_spec

L124 ↗

ProCGroups.Completion.IsProCCompletion.comparison_spec

Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}
variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
variable {ι₂ : G →ₜ* Ghat₂}

Lean source · statement

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

theorem

comparison_comp_eq_id

L131 ↗

ProCGroups.Completion.IsProCCompletion.comparison_comp_eq_id

Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}
variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
variable {ι₂ : G →ₜ* Ghat₂}

Lean source · statement

theorem comparison_comp_eq_id
    (h₁ : IsProCCompletion C G Ghat ι)
    (h₂ : IsProCCompletion C G Ghat₂ ι₂) :
    (h₂.comparison h₁).comp (h₁.comparison h₂) = ContinuousMonoidHom.id Ghat

def

continuousMulEquiv

L153 ↗

ProCGroups.Completion.IsProCCompletion.continuousMulEquiv

Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}
variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
variable {ι₂ : G →ₜ* Ghat₂}

Lean source · statement

def continuousMulEquiv
    (h₁ : IsProCCompletion C G Ghat ι)
    (h₂ : IsProCCompletion C G Ghat₂ ι₂) : Ghat ≃ₜ* Ghat₂

theorem

continuousMulEquiv_apply_completionMap

L176 ↗

ProCGroups.Completion.IsProCCompletion.continuousMulEquiv_apply_completionMap

Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}
variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
variable {ι₂ : G →ₜ* Ghat₂}

Lean source · statement

theorem continuousMulEquiv_apply_completionMap
    (h₁ : IsProCCompletion C G Ghat ι)
    (h₂ : IsProCCompletion C G Ghat₂ ι₂) (x : G) :
    h₁.continuousMulEquiv h₂ (ι x) = ι₂ x

theorem

continuousMulEquiv_symm_apply_completionMap

L187 ↗

ProCGroups.Completion.IsProCCompletion.continuousMulEquiv_symm_apply_completionMap

Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Completion
universe u v
variable {C : ProCGroups.FiniteGroupClass}
namespace IsProCCompletion
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
variable {ι : G →ₜ* Ghat}
variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
variable {ι₂ : G →ₜ* Ghat₂}

Lean source · statement

theorem continuousMulEquiv_symm_apply_completionMap
    (h₁ : IsProCCompletion C G Ghat ι)
    (h₂ : IsProCCompletion C G Ghat₂ ι₂) (x : G) :
    (h₁.continuousMulEquiv h₂).symm (ι₂ x) = ι x

Module documentation

Pro C Groups / Completion / Universal Property

Declarations