NYLL
Module

ProfiniteCompletion.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletion
25 declarations indexed from sourceView source ↗

Module documentation

Completion by open finite quotients

This module constructs the topological profinite completion of a topological group from its open finite-index normal subgroups. Unlike the abstract completion by all finite quotients, the indexing category records the topology on the source group. This is the completion needed for infinite local reciprocity.

The construction uses Mathlib's category of profinite groups, products, and closed subgroups; it does not depend on a separate copied inverse-system implementation.

Universal property

Functorial action

Imports2
Imported by6

Declarations

theorem

topologicalProfiniteCompletionMap_denseRange

L39 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMap_denseRange
Documentation

The canonical map has dense image in the open-quotient completion.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionMap_denseRange :
    DenseRange (topologicalProfiniteCompletionMap G)
def

topologicalProfiniteCompletionProjection

L68 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionProjection
Documentation

Projection of the completion to one of its defining finite quotients.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def topologicalProfiniteCompletionProjection
    (H : OpenFiniteIndexNormalSubgroup G) :
    TopologicalProfiniteCompletion G →ₜ* openFiniteQuotient G H where
  toFun x := x.1 H
  map_one' := rfl
  map_mul' _ _ := rfl
  continuous_toFun := (continuous_apply H).comp continuous_subtype_val
theorem

topologicalProfiniteCompletionProjection_map

L78 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionProjection_map
Documentation

Projecting the canonical completion image of g gives its quotient class.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionProjection_map
    (H : OpenFiniteIndexNormalSubgroup G) (g : G) :
    topologicalProfiniteCompletionProjection G H
        (topologicalProfiniteCompletionMap G g) =
      QuotientGroup.mk g
theorem

topologicalProfiniteCompletionProjection_surjective

L87 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionProjection_surjective
Documentation

Every defining finite quotient is reached by the canonical projection from the topological profinite completion.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionProjection_surjective
    (H : OpenFiniteIndexNormalSubgroup G) :
    Function.Surjective (topologicalProfiniteCompletionProjection G H)
theorem

topologicalProfiniteCompletionMap_ker

L97 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMap_ker
Documentation

The kernel of the canonical completion map is the intersection of all open finite-index 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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionMap_ker :
    (topologicalProfiniteCompletionMap G).ker =
      ⨅ H : OpenFiniteIndexNormalSubgroup G,
        H.toOpenNormalSubgroup.toSubgroup
theorem

topologicalProfiniteCompletionMap_injective_iff

L119 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMap_injective_iff
Documentation

The canonical completion map is injective exactly when the intersection of all open finite-index normal subgroups is trivial.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionMap_injective_iff :
    Function.Injective (topologicalProfiniteCompletionMap G) ↔
      (⨅ H : OpenFiniteIndexNormalSubgroup G,
        H.toOpenNormalSubgroup.toSubgroup) = ⊥
theorem

topologicalProfiniteCompletionMap_injective_of_iInf_eq_bot

L128 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMap_injective_of_iInf_eq_bot
Documentation

A separated open finite-quotient topology gives an injective canonical completion map.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionMap_injective_of_iInf_eq_bot
    (h :
      (⨅ H : OpenFiniteIndexNormalSubgroup G,
        H.toOpenNormalSubgroup.toSubgroup) = ⊥) :
    Function.Injective (topologicalProfiniteCompletionMap G)
theorem

topologicalProfiniteCompletionProjection_transition

L137 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionProjection_transition
Documentation

The finite quotient projections commute with every transition map in the open finite-quotient diagram.

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 v w
section Completion
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionProjection_transition
    {H K : OpenFiniteIndexNormalSubgroup G} (f : H ⟶ K)
    (x : TopologicalProfiniteCompletion G) :
    (openFiniteQuotientDiagram G).map f
        (topologicalProfiniteCompletionProjection G H x) =
      topologicalProfiniteCompletionProjection G K x
def

topologicalProfiniteCompletionPreimageIndex

L168 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionPreimageIndex
Documentation

The open finite-index normal subgroup obtained by pulling an open normal subgroup of a profinite target back along a continuous homomorphism.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def topologicalProfiniteCompletionPreimageIndex
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) (N : OpenNormalSubgroup P) :
    OpenFiniteIndexNormalSubgroup G
def

topologicalProfiniteCompletionFiniteQuotientMap

L187 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionFiniteQuotientMap
Documentation

The finite-stage map induced by a continuous homomorphism to a profinite group, after quotienting by the pulled-back open 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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def topologicalProfiniteCompletionFiniteQuotientMap
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) (N : OpenNormalSubgroup P) :
    G ⧸ (topologicalProfiniteCompletionPreimageIndex P f N).toOpenNormalSubgroup.toSubgroup →*
      P ⧸ (N : Subgroup P)
def

topologicalProfiniteCompletionFiniteQuotientMorphism

L203 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionFiniteQuotientMorphism
Documentation

The finite-stage map as a continuous homomorphism between the corresponding finite profinite quotients.

This is deliberately a ContinuousMonoidHom, rather than a categorical ProfiniteGrp morphism: the latter forces source and target into the same universe even though the universal property has no such mathematical restriction.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def topologicalProfiniteCompletionFiniteQuotientMorphism
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) (N : OpenNormalSubgroup P) :
    openFiniteQuotient G (topologicalProfiniteCompletionPreimageIndex P f N) →ₜ*
      (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp ProfiniteGrp).obj N where
  toMonoidHom := topologicalProfiniteCompletionFiniteQuotientMap P f N
  continuous_toFun := by
    let : DiscreteTopology
        (openFiniteQuotient G
          (topologicalProfiniteCompletionPreimageIndex P f N)) :=
      ⟨rfl⟩
    exact continuous_of_discreteTopology
def

topologicalProfiniteCompletionFiniteProjection

L217 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionFiniteProjection
Documentation

The continuous projection from the open-quotient completion to an open finite quotient of a profinite target.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def topologicalProfiniteCompletionFiniteProjection
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) (N : OpenNormalSubgroup P) :
    TopologicalProfiniteCompletion G →ₜ*
      (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp ProfiniteGrp).obj N
theorem

topologicalProfiniteCompletionFiniteProjection_map

L227 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionFiniteProjection_map
Documentation

The induced finite projection sends the completion image of g to the class of f g.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionFiniteProjection_map
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) (N : OpenNormalSubgroup P) (g : G) :
    topologicalProfiniteCompletionFiniteProjection P f N
        (topologicalProfiniteCompletionMap G g) =
      QuotientGroup.mk' (N : Subgroup P) (f g)
theorem

topologicalProfiniteCompletionFiniteProjection_transition

L236 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionFiniteProjection_transition
Documentation

The finite projections induced by a map to a profinite group commute with the transition maps between the target's 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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionFiniteProjection_transition
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P)
    {N M : OpenNormalSubgroup P} (i : N ⟶ M)
    (x : TopologicalProfiniteCompletion G) :
    (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp ProfiniteGrp).map i
        (topologicalProfiniteCompletionFiniteProjection P f N x) =
      topologicalProfiniteCompletionFiniteProjection P f M x
def

topologicalProfiniteCompletionToFiniteQuotientLimit

L262 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionToFiniteQuotientLimit
Documentation

The map from the open-quotient completion to the inverse limit of all finite quotients of a profinite target.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def topologicalProfiniteCompletionToFiniteQuotientLimit
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) :
    TopologicalProfiniteCompletion G →ₜ*
      ProfiniteGrp.limit (ProfiniteGrp.diagram P) where
  toFun x :=
    ⟨fun N => topologicalProfiniteCompletionFiniteProjection P f N x,
      by
        intro N M i
        exact topologicalProfiniteCompletionFiniteProjection_transition P f i x⟩
  map_one' := by
    apply Subtype.ext
    funext N
    exact (topologicalProfiniteCompletionFiniteProjection P f N).map_one
  map_mul' x y := by
    apply Subtype.ext
    funext N
    exact (topologicalProfiniteCompletionFiniteProjection P f N).map_mul x y
  continuous_toFun := by
    apply continuous_induced_rng.mpr
    apply continuous_pi
    intro N
    exact (topologicalProfiniteCompletionFiniteProjection P f N).continuous_toFun
def

topologicalProfiniteCompletionLift

L287 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionLift
Documentation

A continuous homomorphism from G to a profinite group extends canonically to the completion of G by its 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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def topologicalProfiniteCompletionLift
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) :
    TopologicalProfiniteCompletion G →ₜ* P
theorem

topologicalProfiniteCompletionLift_map

L296 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionLift_map
Documentation

The canonical lift agrees with the original homomorphism on the dense image of G.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionLift_map
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) (g : G) :
    topologicalProfiniteCompletionLift P f
        (topologicalProfiniteCompletionMap G g) =
      f g
theorem

topologicalProfiniteCompletionLift_comp_map

L313 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionLift_comp_map
Documentation

The canonical lift composed with the completion map is the original continuous homomorphism.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionLift_comp_map
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P) :
    (topologicalProfiniteCompletionLift P f).comp
        (topologicalProfiniteCompletionMap G) = f
theorem

topologicalProfiniteCompletionLift_unique

L322 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionLift_unique
Documentation

The canonical lift is the unique continuous homomorphism extending the given map on the dense image of G.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionLift_unique
    (P : ProfiniteGrp.{v}) (f : G →ₜ* P)
    (h : TopologicalProfiniteCompletion G →ₜ* P)
    (hh : h.comp (topologicalProfiniteCompletionMap G) = f) :
    h = topologicalProfiniteCompletionLift P f
def

topologicalProfiniteCompletionMapHom

L350 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMapHom
Documentation

A continuous homomorphism induces the canonical map between open-quotient completions.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def topologicalProfiniteCompletionMapHom (f : G →ₜ* H) :
    TopologicalProfiniteCompletion G →ₜ* TopologicalProfiniteCompletion H
theorem

topologicalProfiniteCompletionMapHom_map

L357 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMapHom_map
Documentation

The map induced on completions carries canonical images to canonical images.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem topologicalProfiniteCompletionMapHom_map
    (f : G →ₜ* H) (g : G) :
    topologicalProfiniteCompletionMapHom f
        (topologicalProfiniteCompletionMap G g) =
      topologicalProfiniteCompletionMap H (f g)
theorem

topologicalProfiniteCompletionMapHom_id

L368 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMapHom_id
Documentation

The homomorphism induced by the identity is the identity on the completion.

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 v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem topologicalProfiniteCompletionMapHom_id :
    topologicalProfiniteCompletionMapHom
        (ContinuousMonoidHom.id G) =
      ContinuousMonoidHom.id (TopologicalProfiniteCompletion G)
theorem

topologicalProfiniteCompletionMapHom_comp

L398 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionMapHom_comp
Documentation

Passing to topological profinite completions preserves composition.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type w} [Group J] [TopologicalSpace J] [IsTopologicalGroup J]
Lean source · statement
theorem topologicalProfiniteCompletionMapHom_comp
    (f : G →ₜ* H) (g : H →ₜ* J) :
    topologicalProfiniteCompletionMapHom (g.comp f) =
      (topologicalProfiniteCompletionMapHom g).comp
        (topologicalProfiniteCompletionMapHom f)
structure

ProfiniteCompletionUniversalProperty

L434 ↗
LocalClassFieldTheory.ProfiniteCompletionUniversalProperty
Documentation

Bundled universal-arrow formulation of completion by open finite quotients. This is the adjunction data used by clients: maps from G to a profinite group correspond to a unique continuous homomorphism out of its completion. The target universe is independent of the source universe.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type w} [Group J] [TopologicalSpace J] [IsTopologicalGroup J]
Lean source · full declaration
structure ProfiniteCompletionUniversalProperty
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (C : ProfiniteGrp.{u}) (ι : G →ₜ* C) : Prop where
  /-- The image of the canonical map `ι` is dense in the profinite completion candidate `C`. -/
  denseRange : DenseRange ι
  /-- Every continuous homomorphism from `G` to a profinite group factors uniquely through `ι`. -/
  existsUniqueLift :
    ∀ (P : ProfiniteGrp.{v}) (f : G →ₜ* P),
      ∃! lift : C →ₜ* P, lift.comp ι = f
theorem

topologicalProfiniteCompletion_universalProperty

L445 ↗
LocalClassFieldTheory.topologicalProfiniteCompletion_universalProperty
Documentation

The constructed completion satisfies the bundled universal property.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type w} [Group J] [TopologicalSpace J] [IsTopologicalGroup J]
Lean source · full declaration
theorem topologicalProfiniteCompletion_universalProperty :
    ProfiniteCompletionUniversalProperty G
      (TopologicalProfiniteCompletion G)
      (topologicalProfiniteCompletionMap G) where
  denseRange := topologicalProfiniteCompletionMap_denseRange G
  existsUniqueLift := by
    intro P f
    refine ⟨topologicalProfiniteCompletionLift P f,
      topologicalProfiniteCompletionLift_comp_map P f, ?_⟩
    intro lift hlift
    exact topologicalProfiniteCompletionLift_unique P f lift hlift

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