NYLL
Module

TopologicalProfiniteCompletion.lean

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.TopologicalProfiniteCompletion
16 declarations indexed from sourceView source ↗

Module documentation

Topological profinite completion

This module defines the profinite completion of a topological group using its open finite-index normal subgroups. The construction records the topology on the source group, unlike the abstract profinite completion by all finite quotients.

Imports3
  • Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
  • Mathlib.Topology.Algebra.Group.Quotient
  • Mathlib.Topology.Algebra.OpenSubgroup
Imported by3

Declarations

def

OpenFiniteIndexNormalSubgroup

L32 ↗
LocalClassFieldTheory.OpenFiniteIndexNormalSubgroup
Documentation

An open normal subgroup whose quotient has finite cardinality.

Source context 5 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
Lean source · statement
def OpenFiniteIndexNormalSubgroup (G : Type u) [Group G] [TopologicalSpace G]
def

toOpenNormalSubgroup

L40 ↗
LocalClassFieldTheory.OpenFiniteIndexNormalSubgroup.toOpenNormalSubgroup
Documentation

The underlying open normal subgroup.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def toOpenNormalSubgroup (H : OpenFiniteIndexNormalSubgroup G) :
    OpenNormalSubgroup G
theorem

finiteIndex'

L45 ↗
LocalClassFieldTheory.OpenFiniteIndexNormalSubgroup.finiteIndex'
Documentation

The finite-index witness carried by the subtype.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem finiteIndex' (H : OpenFiniteIndexNormalSubgroup G) :
    H.toOpenNormalSubgroup.toSubgroup.FiniteIndex
theorem

ext

L51 ↗
LocalClassFieldTheory.OpenFiniteIndexNormalSubgroup.ext
Documentation

Finite-index open normal subgroups are determined by their underlying open normal subgroups.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem ext {H K : OpenFiniteIndexNormalSubgroup G}
    (h : H.toOpenNormalSubgroup = K.toOpenNormalSubgroup) : H = K
instance

(anonymous instance)

L56 ↗
Documentation

An indexed open normal subgroup carries its finite-index witness as an instance.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
instance (H : OpenFiniteIndexNormalSubgroup G) :
    H.toOpenNormalSubgroup.toSubgroup.FiniteIndex
instance

(anonymous instance)

L61 ↗
Documentation

Open finite-index normal subgroups are ordered by inclusion.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
instance : PartialOrder (OpenFiniteIndexNormalSubgroup G)
instance

(anonymous instance)

L66 ↗
Documentation

The inclusion preorder makes open finite-index normal subgroups a small thin category.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
instance : SmallCategory (OpenFiniteIndexNormalSubgroup G)
theorem

le_of_hom

L71 ↗
LocalClassFieldTheory.OpenFiniteIndexNormalSubgroup.le_of_hom
Documentation

A morphism of open finite-index normal subgroups induces inclusion of the underlying subgroups.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
namespace OpenFiniteIndexNormalSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem le_of_hom {H K : OpenFiniteIndexNormalSubgroup G} (f : H ⟶ K) :
    H.toOpenNormalSubgroup.toSubgroup ≤ K.toOpenNormalSubgroup.toSubgroup
def

openFiniteQuotientFunctor

L83 ↗
LocalClassFieldTheory.openFiniteQuotientFunctor
Documentation

The functor of finite quotients attached to open finite-index normal subgroups. Inclusion of subgroups induces the corresponding quotient map.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def openFiniteQuotientFunctor :
    OpenFiniteIndexNormalSubgroup G ⥤ FiniteGrp where
  obj H := FiniteGrp.of (G ⧸ H.toOpenNormalSubgroup.toSubgroup)
  map := fun hHK => FiniteGrp.ofHom <|
    QuotientGroup.map _ _ (.id _) (by
      simpa using OpenFiniteIndexNormalSubgroup.le_of_hom hHK)
  map_id _ := ConcreteCategory.ext <| QuotientGroup.map_id _
  map_comp f g := ConcreteCategory.ext <|
    (QuotientGroup.map_comp_map _ _ _ (.id _) (.id _)
      (by simpa using OpenFiniteIndexNormalSubgroup.le_of_hom f)
      (by simpa using OpenFiniteIndexNormalSubgroup.le_of_hom g)).symm
def

openFiniteQuotientDiagram

L97 ↗
LocalClassFieldTheory.openFiniteQuotientDiagram
Documentation

The finite-quotient diagram, regarded in profinite groups with the discrete topology on every finite stage.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def openFiniteQuotientDiagram :
    OpenFiniteIndexNormalSubgroup G ⥤ ProfiniteGrp
def

openFiniteQuotient

L103 ↗
LocalClassFieldTheory.openFiniteQuotient
Documentation

The finite profinite quotient attached to an open finite-index normal subgroup.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def openFiniteQuotient
    (H : OpenFiniteIndexNormalSubgroup G) : ProfiniteGrp
abbrev

openFiniteQuotientProduct

L108 ↗
LocalClassFieldTheory.openFiniteQuotientProduct
Documentation

The product of all open finite quotients used to construct the completion.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev openFiniteQuotientProduct : ProfiniteGrp
def

openFiniteQuotientProductMapMonoidHom

L113 ↗
LocalClassFieldTheory.openFiniteQuotientProductMapMonoidHom
Documentation

The diagonal homomorphism to the product of all open finite quotients.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def openFiniteQuotientProductMapMonoidHom :
    G →* openFiniteQuotientProduct G where
  toFun g H := QuotientGroup.mk g
  map_one' := by
    funext H
    rfl
  map_mul' x y := by
    funext H
    rfl
theorem

openFiniteQuotientProductMapMonoidHom_continuous

L124 ↗
LocalClassFieldTheory.openFiniteQuotientProductMapMonoidHom_continuous
Documentation

The diagonal map into the product of open finite quotients is continuous.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem openFiniteQuotientProductMapMonoidHom_continuous :
    Continuous (openFiniteQuotientProductMapMonoidHom G)
def

TopologicalProfiniteCompletion

L142 ↗
LocalClassFieldTheory.TopologicalProfiniteCompletion
Documentation

The topological profinite completion over open finite quotients, realized as the closure of the diagonal image in their product.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def TopologicalProfiniteCompletion : ProfiniteGrp
def

topologicalProfiniteCompletionMap

L149 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMap
Documentation

The canonical continuous homomorphism into the open-quotient completion.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def topologicalProfiniteCompletionMap :
    G →ₜ* TopologicalProfiniteCompletion G where
  toFun g :=
    ⟨openFiniteQuotientProductMapMonoidHom G g,
      Subgroup.le_topologicalClosure
        (MonoidHom.range (openFiniteQuotientProductMapMonoidHom G)) ⟨g, rfl⟩⟩
  map_one' := by
    apply Subtype.ext
    exact (openFiniteQuotientProductMapMonoidHom G).map_one
  map_mul' x y := by
    apply Subtype.ext
    exact (openFiniteQuotientProductMapMonoidHom G).map_mul x y
  continuous_toFun :=
    (openFiniteQuotientProductMapMonoidHom_continuous G).subtype_mk _

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.