Module

CanonicalData.lean

Nyll.ProCGroups.FreeProC.CanonicalData

4 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Free pro-C / Canonical Data

This module supplies canonical basis maps and proves the rank-one free pro-\(p\) description of the pro-\(p\) integers.

Imports3

Imported by1

Nyll.ProCGroups.FreeProC.All

theorem

familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap

L28 ↗

ProCGroups.FreeProC.familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap

Documentation

The rank-one basis map converges to the identity in the one-point compactification basis space.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u

Lean source · statement

theorem familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap
    {G : Type u} [Group G] [TopologicalSpace G] (g : G) :
    FamilyConvergesToOneAlongOpenSubgroups (G := G) (Function.const PUnit g)

theorem

topologicallyGenerates_rankOneBasisMap

L34 ↗

ProCGroups.FreeProC.topologicallyGenerates_rankOneBasisMap

Documentation

The rank-one basis map topologically generates the target cyclic pro-\(C\) group.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u

Lean source · statement

theorem topologicallyGenerates_rankOneBasisMap
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G}
    (hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
    Generation.TopologicallyGenerates (G := G) (Set.range (Function.const PUnit g))

theorem

profiniteInteger_rankOneGeneratingData

L48 ↗

ProCGroups.FreeProC.profiniteInteger_rankOneGeneratingData

Documentation

The ordinary profinite integers, with their canonical generator, give the expected rank-one profinite generating datum.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u

Lean source · statement

theorem profiniteInteger_rankOneGeneratingData :
    ∃ ι : PUnit →
        Multiplicative
          (Completion.ProCIntegerLimitCarrier
            (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})),
      ProCGroups.ProC.HasOpenNormalBasisInClass
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})
        (Multiplicative
          (Completion.ProCIntegerLimitCarrier
            (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ∧
        FamilyConvergesToOneAlongOpenSubgroups (G :=
          Multiplicative
            (Completion.ProCIntegerLimitCarrier
              (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ι ∧
        Generation.TopologicallyGenerates (G :=
          Multiplicative
            (Completion.ProCIntegerLimitCarrier
              (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})))
          (Set.range ι)

theorem

proPInteger_rankOneGeneratingData

L83 ↗

ProCGroups.FreeProC.proPInteger_rankOneGeneratingData

Documentation

The pro-\(p\) integers, with their canonical generator, give the expected rank-one pro-\(p\) generating datum.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u

Lean source · statement

theorem proPInteger_rankOneGeneratingData (p : ℕ) [Fact (Nat.Prime p)] :
    ∃ ι : PUnit →
        Multiplicative
          (Completion.ProCIntegerLimitCarrier
            (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})),
      ProCGroups.ProC.HasPGroupOpenNormalBasis p
        (Multiplicative
          (Completion.ProCIntegerLimitCarrier
            (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ∧
        FamilyConvergesToOneAlongOpenSubgroups (G :=
          Multiplicative
            (Completion.ProCIntegerLimitCarrier
              (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ι ∧
        Generation.TopologicallyGenerates (G :=
          Multiplicative
            (Completion.ProCIntegerLimitCarrier
              (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})))
          (Set.range ι)

Module documentation

Pro C Groups / Free pro-C / Canonical Data

Declarations

familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap

topologicallyGenerates_rankOneBasisMap

profiniteInteger_rankOneGeneratingData

proPInteger_rankOneGeneratingData