NYLL
Module

ProfiniteIntegerRecognition.lean

Nyll.ProCGroups.Completion.ProfiniteIntegerRecognition
2 declarations indexed from sourceView source ↗

Module documentation

Recognizing the full profinite integers

A profinite group with a topological generator and open normal quotients of every positive order is isomorphic to the actual inverse limit of all finite cyclic groups. Normalizing each coefficient map at the generator proves its uniqueness and hence the compatibility of the independently chosen finite quotients.

Imports6
Imported by2

Declarations

theorem

exists_normalized_cyclic_coefficient

L37 ↗
ProCGroups.Completion.exists_normalized_cyclic_coefficient
Documentation

Normalize an actual finite quotient at a fixed topological generator. The resulting coefficient map detects exactly equality in that quotient.

Source context 6 commands

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

noncomputable section
open scoped Topology
namespace ProCGroups.Completion
open ProCGroups.Generation ProCGroups.ProC
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem exists_normalized_cyclic_coefficient [CompactSpace G]
    (g : G) (hg : TopologicallyGenerates ({g} : Set G))
    (U : OpenNormalSubgroup G) {n : ℕ}
    (hn : Nat.card (G ⧸ (U : Subgroup G)) = n) :
    ∃ f : G →ₜ* Multiplicative (ZMod n),
      f g = Multiplicative.ofAdd 1 ∧
      ∀ x y : G, f x = f y ↔
        OpenNormalSubgroup.quotientProj U x = OpenNormalSubgroup.quotientProj U y
theorem

exists_profiniteInteger_equiv_of_generator_and_quotient_orders

L64 ↗
ProCGroups.Completion.exists_profiniteInteger_equiv_of_generator_and_quotient_orders
Documentation

A topological generator and actual finite quotients of every positive order identify a profinite group with the full inverse limit of finite cyclic groups. The isomorphism sends the specified generator to the compatible residue class of the integer one.

Source context 6 commands

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

noncomputable section
open scoped Topology
namespace ProCGroups.Completion
open ProCGroups.Generation ProCGroups.ProC
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem exists_profiniteInteger_equiv_of_generator_and_quotient_orders
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (g : G) (hg : TopologicallyGenerates ({g} : Set G))
    (horders : ∀ n : ℕ, 0 < n →
      ∃ U : OpenNormalSubgroup G, Nat.card (G ⧸ (U : Subgroup G)) = n) :
    ∃ e : G ≃ₜ* Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})),
      e g = proCIntegerOne (C := FiniteGroupClass.allFinite)

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