Documentation

TauCeti.Topology.Algebra.Group.Profinite.Completion

The universal property of profinite completion #

This file restates the categorical universal property of Mathlib's profinite completion for unbundled groups and continuous monoid homomorphisms. It also proves that the canonical map from a finite group to its profinite completion is bijective, and exposes the projections of the profinite completion onto the finite quotients it is the limit of.

The correspondence continuousMonoidHomEquiv allows the group and the profinite target to live in independent universes, unlike Mathlib's single-universe adjunction ProfiniteGrp.ProfiniteCompletion.homEquiv; this is what lets a fixed universe-polymorphic completion, such as the profinite integers, map to profinite groups in any universe.

The continuous finite quotients of the completion are exactly the finite quotients of G (isFiniteContinuousQuotient_iff_exists_surjective), and the completion of a finitely generated group is topologically finitely generated (isTopologicallyFinitelyGenerated). Through the finite-quotient determinacy of topologically finitely generated profinite groups this gives the theorem of Dixon, Formanek, Poland and Ribes: two finitely generated groups with the same finite quotients have topologically isomorphic profinite completions (nonempty_continuousMulEquiv_of_forall_exists_surjective_iff); in fact finite generation of one of the two groups suffices.

References #

source
theorem TauCeti.ProfiniteCompletion.continuousMonoidHom_ext (G : Type u) [Group G] {Q : Type v} [Monoid Q] [TopologicalSpace Q] [T2Space Q] {f g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop →ₜ* Q} (h : ∀ (x : G), f (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) x) = g (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) x)) :
f = g

Two continuous homomorphisms from a profinite completion to a Hausdorff topological monoid agree if they agree on the canonical dense image of the original group.

source
theorem TauCeti.ProfiniteCompletion.continuousMonoidHom_ext_iff {G : Type u} [Group G] {Q : Type v} [Monoid Q] [TopologicalSpace Q] [T2Space Q] {f g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop →ₜ* Q} :
f = g ↔ ∀ (x : G), f (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) x) = g (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) x)
source
theorem TauCeti.ProfiniteCompletion.etaFn_bijective_of_finite (G : Type u) [Group G] [Finite G] :
Function.Bijective (ProfiniteGrp.ProfiniteCompletion.etaFn ↧G)

The canonical map from a finite group to its profinite completion is bijective.

source
def TauCeti.ProfiniteCompletion.coordinateHom (G : Type u) [Group G] (H : FiniteIndexNormalSubgroup G) :
↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop →* G ⧸ H.toSubgroup

The projection from the profinite completion of G onto its finite quotient indexed by the finite-index normal subgroup H.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ProfiniteCompletion.coordinateHom_apply (G : Type u) [Group G] (H : FiniteIndexNormalSubgroup G) (x : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) :
    (coordinateHom G H) x = ↑x H

    The projection onto the finite quotient by H evaluates the underlying compatible family of cosets at H.

    source
    @[simp]
    theorem TauCeti.ProfiniteCompletion.coordinateHom_etaFn (G : Type u) [Group G] (H : FiniteIndexNormalSubgroup G) (g : G) :
    (coordinateHom G H) (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) g) = ↑g

    The H-coordinate of the canonical image of g is its coset modulo H.

    source
    theorem TauCeti.ProfiniteCompletion.continuous_coordinateHom (G : Type u) [Group G] (H : FiniteIndexNormalSubgroup G) :
    Continuous ⇑(coordinateHom G H)

    The projection onto a finite quotient is continuous, that quotient carrying the discrete topology.

    source
    noncomputable def TauCeti.ProfiniteCompletion.continuousMonoidHomEquiv (G : Type u) [Group G] (P : Type v) [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] :
    (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop →ₜ* P) ≃ (G →* P)

    Continuous homomorphisms from the profinite completion of G to a profinite group P correspond to abstract homomorphisms from G to P, by restriction along the canonical map. The target P may live in a different universe from G.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.ProfiniteCompletion.continuousMonoidHomEquiv_apply (G : Type u) [Group G] (P : Type v) [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (f : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop →ₜ* P) (g : G) :
      ((continuousMonoidHomEquiv G P) f) g = f (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) g)

      The unbundled profinite-completion correspondence restricts a continuous homomorphism along the canonical map.

      source
      @[simp]
      theorem TauCeti.ProfiniteCompletion.continuousMonoidHomEquiv_symm_apply_etaFn (G : Type u) [Group G] (P : Type v) [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (f : G →* P) (g : G) :
      ((continuousMonoidHomEquiv G P).symm f) (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) g) = f g

      The continuous lift of an abstract homomorphism agrees with it on the original group.

      source
      theorem TauCeti.ProfiniteCompletion.isFiniteContinuousQuotient_iff_exists_surjective {G : Type u} [Group G] {Q : Type u} [Group Q] [Finite Q] :
      IsFiniteContinuousQuotient (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) Q ↔ ∃ (f : G →* Q), Function.Surjective ⇑f

      The continuous finite quotients of the profinite completion are the finite quotients of the group. A finite group Q occurs as a continuous finite quotient of the profinite completion of G exactly when there is a surjective homomorphism G →* Q.

      source
      theorem TauCeti.ProfiniteCompletion.isTopologicallyFinitelyGenerated {G : Type u} [Group G] [Group.FG G] :
      IsTopologicallyFinitelyGenerated ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop

      The profinite completion of a finitely generated group is topologically finitely generated: the canonical image of G is dense.

      source
      theorem TauCeti.ProfiniteCompletion.nonempty_continuousMulEquiv_of_forall_exists_surjective_iff {G : Type u} [Group G] {H : Type u} [Group H] [Group.FG G] (h : ∀ (Q : Type u) [inst : Group Q] [Finite Q], (∃ (f : G →* Q), Function.Surjective ⇑f) ↔ ∃ (f : H →* Q), Function.Surjective ⇑f) :
      Nonempty (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop ≃ₜ* ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧H).toProfinite.toTop)

      Finitely generated groups with the same finite quotients have isomorphic profinite completions (Dixon, Formanek, Poland and Ribes). If G is finitely generated and every finite group is a quotient of G exactly when it is a quotient of H, then the profinite completions of G and H are topologically isomorphic. No finiteness hypothesis is placed on H.