NYLL
Module

AbstractProfiniteCompletionComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbstractProfiniteCompletionComparison
26 declarations indexed from sourceView source ↗

Module documentation

Comparison with the abstract profinite completion

The abstract profinite completion of a group is the completion formed from all finite-index normal subgroups, without reference to a topology. We realize it by applying the open-quotient construction to a discrete copy of the group.

When every finite-index normal subgroup is open in the given topology, the open-quotient completion and the abstract completion are canonically isomorphic as topological groups.

Imports1
Imported by1

Declarations

structure

AbstractProfiniteSource

L31 ↗
LocalClassFieldTheory.AbstractProfiniteSource
Documentation

A copy of a group equipped with the discrete topology.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · full declaration
structure AbstractProfiniteSource (G : Type u) where
  /-- The underlying group element. -/
  val : G
def

equiv

L40 ↗
LocalClassFieldTheory.AbstractProfiniteSource.equiv
Documentation

The tautological equivalence between the discrete copy and the underlying type.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
namespace AbstractProfiniteSource
variable (G : Type u)
Lean source · full declaration
def equiv : AbstractProfiniteSource G ≃ G where
  toFun := val
  invFun := mk
  left_inv _ := rfl
  right_inv _ := rfl
instance

(anonymous instance)

L47 ↗
Documentation

The discrete source copy inherits the group structure of G.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
namespace AbstractProfiniteSource
variable (G : Type u)
Lean source · statement
instance [Group G] : Group (AbstractProfiniteSource G)
instance

(anonymous instance)

L50 ↗
Documentation

The abstract profinite source carries the discrete topology.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
namespace AbstractProfiniteSource
variable (G : Type u)
Lean source · statement
instance : TopologicalSpace (AbstractProfiniteSource G)
instance

(anonymous instance)

L53 ↗
Documentation

The topology on the abstract profinite source is discrete.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
namespace AbstractProfiniteSource
variable (G : Type u)
Lean source · statement
instance : DiscreteTopology (AbstractProfiniteSource G)
instance

(anonymous instance)

L56 ↗
Documentation

The discrete source copy of a group is a topological group.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
namespace AbstractProfiniteSource
variable (G : Type u)
Lean source · statement
instance [Group G] : IsTopologicalGroup (AbstractProfiniteSource G)
def

mulEquiv

L59 ↗
LocalClassFieldTheory.AbstractProfiniteSource.mulEquiv
Documentation

The tautological multiplicative equivalence from the discrete copy.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
namespace AbstractProfiniteSource
variable (G : Type u)
Lean source · full declaration
def mulEquiv [Group G] : AbstractProfiniteSource G ≃* G where
  toEquiv := equiv G
  map_mul' _ _ := rfl
def

AbstractProfiniteCompletion

L68 ↗
LocalClassFieldTheory.AbstractProfiniteCompletion
Documentation

The abstract profinite completion formed from all finite-index normal subgroups. This is a stable, non-abbrev public object; its inverse-limit realization is available through abstractProfiniteCompletionEquivModel.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
def AbstractProfiniteCompletion
    (G : Type u) [Group G] : ProfiniteGrp
def

abstractProfiniteCompletionEquivModel

L74 ↗
LocalClassFieldTheory.abstractProfiniteCompletionEquivModel
Documentation

Canonical comparison with the concrete open-finite-quotient model used to construct the abstract profinite completion.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
def abstractProfiniteCompletionEquivModel
    (G : Type u) [Group G] :
    AbstractProfiniteCompletion G ≃ₜ*
      TopologicalProfiniteCompletion (AbstractProfiniteSource G)
def

abstractProfiniteCompletionClass

L84 ↗
LocalClassFieldTheory.abstractProfiniteCompletionClass
Documentation

The canonical dense class map from the discrete source into the stable abstract completion.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
def abstractProfiniteCompletionClass
    (G : Type u) [Group G] :
    AbstractProfiniteSource G →ₜ* AbstractProfiniteCompletion G
theorem

abstractProfiniteCompletionEquivModel_class

L92 ↗
LocalClassFieldTheory.abstractProfiniteCompletionEquivModel_class
Documentation

The model equivalence sends an abstract completion class to the canonical topological class.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
theorem abstractProfiniteCompletionEquivModel_class
    (G : Type u) [Group G] (g : AbstractProfiniteSource G) :
    abstractProfiniteCompletionEquivModel G
        (abstractProfiniteCompletionClass G g) =
      topologicalProfiniteCompletionMap (AbstractProfiniteSource G) g
theorem

abstractProfiniteCompletionClass_denseRange

L101 ↗
LocalClassFieldTheory.abstractProfiniteCompletionClass_denseRange
Documentation

The canonical class map has dense range. Clients can use this theorem without knowing which inverse-limit model realizes the abstract completion.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
theorem abstractProfiniteCompletionClass_denseRange
    (G : Type u) [Group G] :
    DenseRange (abstractProfiniteCompletionClass G)
def

abstractProfiniteCompletionLift

L117 ↗
LocalClassFieldTheory.abstractProfiniteCompletionLift
Documentation

Extend a continuous homomorphism from the discrete source across the stable abstract profinite completion. This is the representation-independent universal-property entry point for AbstractProfiniteCompletion.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
def abstractProfiniteCompletionLift
    (G : Type u) [Group G]
    (P : ProfiniteGrp.{v})
    (f : AbstractProfiniteSource G →ₜ* P) :
    AbstractProfiniteCompletion G →ₜ* P
theorem

abstractProfiniteCompletionLift_class

L127 ↗
LocalClassFieldTheory.abstractProfiniteCompletionLift_class
Documentation

The universal lift agrees with the original map on abstract completion classes.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
theorem abstractProfiniteCompletionLift_class
    (G : Type u) [Group G]
    (P : ProfiniteGrp.{v})
    (f : AbstractProfiniteSource G →ₜ* P)
    (g : AbstractProfiniteSource G) :
    abstractProfiniteCompletionLift G P f
        (abstractProfiniteCompletionClass G g) = f g
theorem

abstractProfiniteCompletionLift_comp_class

L142 ↗
LocalClassFieldTheory.abstractProfiniteCompletionLift_comp_class
Documentation

Composing the universal lift with the class map recovers the source homomorphism.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
theorem abstractProfiniteCompletionLift_comp_class
    (G : Type u) [Group G]
    (P : ProfiniteGrp.{v})
    (f : AbstractProfiniteSource G →ₜ* P) :
    (abstractProfiniteCompletionLift G P f).comp
        (abstractProfiniteCompletionClass G) = f
theorem

abstractProfiniteCompletionLift_unique

L153 ↗
LocalClassFieldTheory.abstractProfiniteCompletionLift_unique
Documentation

A continuous homomorphism out of the stable abstract completion is determined by its values on the canonical dense class map.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
Lean source · statement
theorem abstractProfiniteCompletionLift_unique
    (G : Type u) [Group G]
    (P : ProfiniteGrp.{v})
    (f : AbstractProfiniteSource G →ₜ* P)
    (h : AbstractProfiniteCompletion G →ₜ* P)
    (hh : h.comp (abstractProfiniteCompletionClass G) = f) :
    h = abstractProfiniteCompletionLift G P f
def

abstractProfiniteCompletionModelMapMonoidHom

L186 ↗
LocalClassFieldTheory.abstractProfiniteCompletionModelMapMonoidHom
Documentation

The model-valued completion map used internally to establish continuity.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def abstractProfiniteCompletionModelMapMonoidHom :
    G →* TopologicalProfiniteCompletion (AbstractProfiniteSource G)
def

abstractProfiniteCompletionMapMonoidHom

L192 ↗
LocalClassFieldTheory.abstractProfiniteCompletionMapMonoidHom
Documentation

The abstract completion map, viewed as a homomorphism from the original group.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def abstractProfiniteCompletionMapMonoidHom : G →* AbstractProfiniteCompletion G
theorem

abstractProfiniteCompletionMapMonoidHom_apply

L199 ↗
LocalClassFieldTheory.abstractProfiniteCompletionMapMonoidHom_apply
Documentation

The completion map sends g to the class of its discrete source copy.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [TopologicalSpace G] [IsTopologicalGroup G] in
Lean source · statement
theorem abstractProfiniteCompletionMapMonoidHom_apply (g : G) :
    abstractProfiniteCompletionMapMonoidHom G g =
      abstractProfiniteCompletionClass G
        ((AbstractProfiniteSource.mulEquiv G).symm g)
theorem

abstractProfiniteCompletionModelMapMonoidHom_continuous

L214 ↗
LocalClassFieldTheory.abstractProfiniteCompletionModelMapMonoidHom_continuous
Documentation

If every finite-index normal subgroup is open, the abstract completion map is continuous for the original topology.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem abstractProfiniteCompletionModelMapMonoidHom_continuous
    (hOpen : ∀ H : Subgroup G, H.Normal → H.FiniteIndex → IsOpen (H : Set G)) :
    Continuous (abstractProfiniteCompletionModelMapMonoidHom G)
theorem

abstractProfiniteCompletionMapMonoidHom_continuous

L253 ↗
LocalClassFieldTheory.abstractProfiniteCompletionMapMonoidHom_continuous
Documentation

If every finite-index normal subgroup is open, the abstract completion map is continuous for the original topology.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem abstractProfiniteCompletionMapMonoidHom_continuous
    (hOpen : ∀ H : Subgroup G, H.Normal → H.FiniteIndex → IsOpen (H : Set G)) :
    Continuous (abstractProfiniteCompletionMapMonoidHom G)
def

topologicalProfiniteCompletionToAbstract

L261 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionToAbstract
Documentation

The canonical continuous map from the topological completion to the abstract completion.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def topologicalProfiniteCompletionToAbstract
    (hOpen : ∀ H : Subgroup G, H.Normal → H.FiniteIndex → IsOpen (H : Set G)) :
    TopologicalProfiniteCompletion G →ₜ* AbstractProfiniteCompletion G
theorem

topologicalProfiniteCompletionToAbstract_map

L270 ↗
LocalClassFieldTheory.topologicalProfiniteCompletionToAbstract_map
Documentation

The comparison map agrees with the abstract completion map on the source group.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalProfiniteCompletionToAbstract_map
    (hOpen : ∀ H : Subgroup G, H.Normal → H.FiniteIndex → IsOpen (H : Set G))
    (g : G) :
    topologicalProfiniteCompletionToAbstract G hOpen
        (topologicalProfiniteCompletionMap G g) =
      abstractProfiniteCompletionClass G
        ((AbstractProfiniteSource.mulEquiv G).symm g)
def

abstractProfiniteCompletionToTopological

L283 ↗
LocalClassFieldTheory.abstractProfiniteCompletionToTopological
Documentation

The canonical continuous map from the abstract completion to the topological completion.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def abstractProfiniteCompletionToTopological :
    AbstractProfiniteCompletion G →ₜ* TopologicalProfiniteCompletion G
theorem

abstractProfiniteCompletionToTopological_map

L293 ↗
LocalClassFieldTheory.abstractProfiniteCompletionToTopological_map
Documentation

The reverse comparison map agrees with the topological completion map on the discrete source.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem abstractProfiniteCompletionToTopological_map
    (g : AbstractProfiniteSource G) :
    abstractProfiniteCompletionToTopological G
        (abstractProfiniteCompletionClass G g) =
      topologicalProfiniteCompletionMap G (AbstractProfiniteSource.mulEquiv G g)
def

topologicalProfiniteCompletion_compare_abstract

L304 ↗
LocalClassFieldTheory.topologicalProfiniteCompletion_compare_abstract
Documentation

Under the condition that all finite-index normal subgroups are open, the open-quotient completion is canonically the abstract profinite completion.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace LocalClassFieldTheory
universe u v
section Comparison
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def topologicalProfiniteCompletion_compare_abstract
    (hOpen : ∀ H : Subgroup G, H.Normal → H.FiniteIndex → IsOpen (H : Set G)) :
    TopologicalProfiniteCompletion G ≃ₜ* AbstractProfiniteCompletion G

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