Module

Basic.lean

Nyll.ProCGroups.FreeProC.Basic

81 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Free pro-C / Basic

This module defines the free and pointed free pro-\(C\) universal properties, their converging-set form, and the bundled canonical source data used by later constructions.

Imports8

Mathlib.GroupTheory.SpecificGroups.Cyclic
Mathlib.Topology.Algebra.Nonarchimedean.Basic
Mathlib.Topology.Instances.ZMod
Nyll.ProCGroups.Completion.UniversalProperty
Nyll.ProCGroups.FiniteGroups.StandardClasses
Nyll.ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
Nyll.ProCGroups.ProC.Category.Basic
Nyll.ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation

Imported by18

structure

FamilyConvergesToOneAlongOpenSubgroups

L231 ↗

ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups

Documentation

The weaker condition obtained by testing family convergence only against open subgroups.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

def FamilyConvergesToOneAlongOpenSubgroups
    {X : Type v}
    {G : Type u} [Group G] [TopologicalSpace G]
    (μ : X → G) : Prop

theorem

familyConvergesToOne_iff_alongOpenSubgroups

L357 ↗

ProCGroups.FreeProC.familyConvergesToOne_iff_alongOpenSubgroups

Documentation

For nonarchimedean groups, genuine family convergence is equivalent to the open-subgroup test.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem familyConvergesToOne_iff_alongOpenSubgroups
    {X : Type v} {G : Type u} [Group G] [TopologicalSpace G]
    [NonarchimedeanGroup G] {μ : X → G} :
    FamilyConvergesToOne (G := G) μ ↔
      FamilyConvergesToOneAlongOpenSubgroups (G := G) μ

structure

instCoeFunConvergingGeneratingMap

L386 ↗

ProCGroups.FreeProC.ConvergingGeneratingMap.instCoeFunConvergingGeneratingMap

Documentation

A convergent generating map coerces to its underlying map into the group.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace ConvergingGeneratingMap
variable {X Y : Type v}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instCoeFunConvergingGeneratingMap :
    CoeFun (ConvergingGeneratingMap X G) (fun _ => X → G) where
  coe φ := φ.toFun

theorem

generatesAndConvergesToOneAlongOpenSubgroups

L418 ↗

ProCGroups.FreeProC.ConvergingGeneratingMap.generatesAndConvergesToOneAlongOpenSubgroups

Documentation

The range of a convergent generating map generates the group and converges to one along open subgroups.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace ConvergingGeneratingMap
variable {X Y : Type v}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem generatesAndConvergesToOneAlongOpenSubgroups (φ : ConvergingGeneratingMap X G) :
    Generation.GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) (Set.range (φ : X → G))

structure

IsEpimorphicallyPointedFreeProCGroupOn

L428 ↗

ProCGroups.FreeProC.IsEpimorphicallyPointedFreeProCGroupOn

Documentation

A pointed pro-C group with unique lifts only for pointed maps whose images topologically generate their targets.

This is intentionally not the unrestricted pointed-free universal property.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · full declaration

structure IsEpimorphicallyPointedFreeProCGroupOn
    (X : Type u) [TopologicalSpace X] (x0 : X)
    (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι : X → F) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
  /-- The canonical pointed map into `F` is continuous. -/
  continuous_ι : Continuous ι
  /-- The distinguished source point `x0` is sent to the identity of `F`. -/
  map_base : ι x0 = 1
  /-- The image of the canonical pointed map topologically generates `F`. -/
  generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
  /--
  Every continuous, basepoint-preserving map whose image generates a pro-`C` target extends to
  a unique continuous group homomorphism from `F`.
  -/
  existsUnique_lift :
    ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (G) →
      ∀ (φ : X → G), Continuous φ → φ x0 = 1 →
        Generation.TopologicallyGenerates (G := G) (Set.range φ) →
          ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x

structure

IsEpimorphicallyFreeProCGroupOnConvergingSet

L460 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet

Documentation

A pro-C group with unique lifts only for open-subgroup-convergent families whose images topologically generate their targets. The convergence hypothesis is FamilyConvergesToOneAlongOpenSubgroups, not the unqualified filter predicate.

The Epimorphically qualifier records the missing unrestricted mapping property.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · full declaration

structure IsEpimorphicallyFreeProCGroupOnConvergingSet
    (X : Type v)
    (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι : X → F) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
  /--
  The canonical generator family has only finitely many terms outside each open subgroup of
  `F`.
  -/
  convergesToOneAlongOpenSubgroups : FamilyConvergesToOneAlongOpenSubgroups (G := F) ι
  /-- The canonical converging family topologically generates `F`. -/
  generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
  /--
  Every converging family that topologically generates a pro-`C` target extends to a unique
  continuous group homomorphism from `F`.
  -/
  existsUnique_lift :
    ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (G) →
      ∀ (φ : X → G), FamilyConvergesToOneAlongOpenSubgroups (G := G) φ →
        Generation.TopologicallyGenerates (G := G) (Set.range φ) →
          ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x

theorem

freeProCGroupOn_injective

L490 ↗

ProCGroups.FreeProC.freeProCGroupOn_injective

Documentation

The canonical map of a free pro-C group on a topological space is injective whenever the predicate supplies enough separating pro-C targets.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem freeProCGroupOn_injective
    {X : Type u} [TopologicalSpace X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hι : IsFreeProCGroup (C := C) ι)
    (hsep :
      ∀ ⦃x y : X⦄, x ≠ y →
        ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
          (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
    ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧
            ∃ φ : X → A, Continuous φ ∧
              Generation.TopologicallyGenerates (G := A) (Set.range φ) ∧ φ x ≠ φ y) :
    Function.Injective ι

theorem

one_not_mem_range_of_freeProCGroupOn

L516 ↗

ProCGroups.FreeProC.one_not_mem_range_of_freeProCGroupOn

Documentation

Under an explicit nontrivial cyclic pro-C target hypothesis, the identity does not lie in the image of the topological basis of a free pro-C group.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem one_not_mem_range_of_freeProCGroupOn
    {X : Type u} [TopologicalSpace X] [Nonempty X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hι : IsFreeProCGroup (C := C) ι)
    (hnontrivial :
      ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
        (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
    ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
          Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
    (1 : F) ∉ Set.range ι

theorem

one_not_mem_range_of_epimorphicallyFreeProCGroupOnConvergingSet

L553 ↗

ProCGroups.FreeProC.one_not_mem_range_of_epimorphicallyFreeProCGroupOnConvergingSet

Documentation

Under an explicit nontrivial cyclic pro-C target hypothesis, the identity does not lie in a basis converging to 1.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem one_not_mem_range_of_epimorphicallyFreeProCGroupOnConvergingSet
    {X : Type u}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (hnontrivial :
      ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
        (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
    ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
          Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
    (1 : F) ∉ Set.range ι

theorem

epimorphicallyFreeProCGroupOnConvergingSet_injective

L595 ↗

ProCGroups.FreeProC.epimorphicallyFreeProCGroupOnConvergingSet_injective

Documentation

Under the same nontrivial cyclic-target hypothesis, the basis map for a free pro-C group on a set converging to 1 is injective.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem epimorphicallyFreeProCGroupOnConvergingSet_injective
    {X : Type u}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (hnontrivial :
      ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
        (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
    ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
          Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
    Function.Injective ι

theorem

exists_nontrivial_singleton_topologicalGenerator

L644 ↗

ProCGroups.FreeProC.exists_nontrivial_singleton_topologicalGenerator

Documentation

A nontrivial cyclic topological group has a nontrivial singleton topological generator.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem exists_nontrivial_singleton_topologicalGenerator
    {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [IsCyclic A] [Nontrivial A] :
    ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A)

theorem

exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass

L665 ↗

ProCGroups.FreeProC.exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass

Documentation

A concrete finite-group class containing a nontrivial finite cyclic group admits a nontrivial topologically cyclic pro-C model.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (hquot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    (hcyc :
      ∃ (A : Type u) (_ : Group A) (_ : Finite A),
        C A ∧ IsCyclic A ∧ Nontrivial A) :
    ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
      (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
      ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧
        ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A)

theorem

finite_generatingFamily_is_basis

L688 ↗

ProCGroups.FreeProC.finite_generatingFamily_is_basis

Documentation

For a finite-rank free pro-C group, any generating family with the same finite cardinality is again a converging-set basis.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem finite_generatingFamily_is_basis
    {X : Type u} {Y : Type u}
    [Finite X] [Finite Y]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F} {μ : Y → F}
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (hcard : Cardinal.mk X = Cardinal.mk Y)
    (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
    IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) Y F μ

theorem

finite_generatingFamily_is_basis_of_finiteGroupClass

L817 ↗

ProCGroups.FreeProC.finite_generatingFamily_is_basis_of_finiteGroupClass

Documentation

Concrete finite-group-class specialization of finite_generatingFamily_is_basis.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem finite_generatingFamily_is_basis_of_finiteGroupClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {X : Type u} {Y : Type u}
    [Finite X] [Finite Y]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F} {μ : Y → F}
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (hcard : Cardinal.mk X = Cardinal.mk Y)
    (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
    IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) Y F μ

theorem

finite_generatingFamily_is_basis_of_finiteGroupClass_cyclic

L836 ↗

ProCGroups.FreeProC.finite_generatingFamily_is_basis_of_finiteGroupClass_cyclic

Documentation

Concrete finite-group-class specialization when a nontrivial cyclic target is available.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem finite_generatingFamily_is_basis_of_finiteGroupClass_cyclic
    (C : ProCGroups.FiniteGroupClass.{u})
    (hquot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    (hcyc :
      ∃ (A : Type u) (_ : Group A) (_ : Finite A),
        C A ∧ IsCyclic A ∧ Nontrivial A)
    {X : Type u} {Y : Type u}
    [Finite X] [Finite Y]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F} {μ : Y → F}
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (hcard : Cardinal.mk X = Cardinal.mk Y)
    (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
    IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) Y F μ

theorem

surjective_hom_of_rangeContainsGeneratingSet

L865 ↗

ProCGroups.FreeProC.surjective_hom_of_rangeContainsGeneratingSet

Documentation

If a continuous homomorphism has range containing a topological generating set, then it is surjective between profinite groups.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem surjective_hom_of_rangeContainsGeneratingSet
    {X : Type u}
    {F : Type u} [Group F] [TopologicalSpace F] [CompactSpace F]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
    {ι : X → G}
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range ι))
    {σ : F →* G} (hσ : Continuous σ)
    (hsub : Set.range ι ⊆ (σ.range : Set G)) :
    Function.Surjective σ

theorem

finite_of_topologicallyFinitelyGenerated_epimorphicallyFreeProCGroupOnConvergingSet

L902 ↗

ProCGroups.FreeProC.finite_of_topologicallyFinitelyGenerated_epimorphicallyFreeProCGroupOnConvergingSet

Documentation

A topologically finitely generated free pro-C group on a converging set has finite basis, provided C admits a nontrivial cyclic pro-C target.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem finite_of_topologicallyFinitelyGenerated_epimorphicallyFreeProCGroupOnConvergingSet
    {X : Type u}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hfg : FiniteGeneration.TopologicallyFinitelyGenerated F)
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    (hnontrivial :
      ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
        (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
    ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
          Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
    Finite X

theorem

exists_epimorphicallyFreeProCGroupOnConvergingSet_surjecting

L1016 ↗

ProCGroups.FreeProC.exists_epimorphicallyFreeProCGroupOnConvergingSet_surjecting

Documentation

A fixed free pro-C group on a set converging to 1 admits a continuous epimorphism onto any profinite pro-C target generated by the image of its basis.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem exists_epimorphicallyFreeProCGroupOnConvergingSet_surjecting
    {X : Type u}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (φ : X → G)
    (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
    ∃ ψ : F →* G, Continuous ψ ∧ Function.Surjective ψ ∧ ∀ x, ψ (ι x) = φ x

theorem

proCCompletionOfAbstractFreeGroup_is_free

L1040 ↗

ProCGroups.FreeProC.proCCompletionOfAbstractFreeGroup_is_free

Documentation

The pro-C completion of the abstract free group on a finite basis is free pro-C on that basis.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · full declaration

theorem proCCompletionOfAbstractFreeGroup_is_free
    {X : Type u} [Finite X]
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    {Fhat : Type u} [Group Fhat] [TopologicalSpace Fhat] [IsTopologicalGroup Fhat]
    [CompactSpace Fhat] [T2Space Fhat] [TotallyDisconnectedSpace Fhat]
    {ι : FreeGroup X →ₜ* Fhat}
    (hι : ProCGroups.Completion.IsProCCompletion C (FreeGroup X) Fhat ι) :
    IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X Fhat
      (fun x => ι (FreeGroup.of x)) := by
  refine ⟨hι.hasOpenNormalBasisInClass, ?_, ?_, ?_⟩
  · exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := Fhat)
      (fun x : X => ι (FreeGroup.of x))
  · have himage :
        ι '' Set.range (FreeGroup.of : X → FreeGroup X) =
          Set.range (fun x : X => ι (FreeGroup.of x)) := by
      calc
        ι '' Set.range (FreeGroup.of : X → FreeGroup X) =
            Set.range ((⇑ι) ∘ (FreeGroup.of : X → FreeGroup X)) :=
          (Set.range_comp ι (FreeGroup.of : X → FreeGroup X)).symm
        _ = Set.range (fun x : X => ι (FreeGroup.of x)) := by rfl
    have hclosure :
        Subgroup.closure (Set.range fun x : X => ι (FreeGroup.of x)) =
          ι.toMonoidHom.range := by
      calc
        Subgroup.closure (Set.range fun x : X => ι (FreeGroup.of x))
            = Subgroup.map ι.toMonoidHom
                (Subgroup.closure (Set.range (FreeGroup.of : X → FreeGroup X))) := by
              simpa [himage] using
                (ι.toMonoidHom.map_closure (Set.range (FreeGroup.of : X → FreeGroup X))).symm
        _ = ι.toMonoidHom.range := by
          rw [FreeGroup.closure_range_of X, MonoidHom.range_eq_map]
    rw [Generation.TopologicallyGenerates, hclosure]
    rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
    simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hι.denseRange
  · intro G _ _ _ _ _ _ hG φ _hφ hgen
    let φfree : FreeGroup X →ₜ* G :=
      { toMonoidHom := FreeGroup.lift φ
        continuous_toFun := by
          simpa using (continuous_of_discreteTopology : Continuous (FreeGroup.lift φ)) }
    let φhat : Fhat →ₜ* G := hι.lift hG φfree
    refine ⟨φhat.toMonoidHom, ?_, ?_⟩
    · refine ⟨φhat.continuous_toFun, ?_⟩
      intro x
      have hfac := congrArg (fun ψ : FreeGroup X →ₜ* G => ψ (FreeGroup.of x))
        (hι.lift_spec hG φfree)
      have hfree : φfree (FreeGroup.of x) = φ x := by
        change FreeGroup.lift φ (FreeGroup.of x) = φ x
        simp only [FreeGroup.lift_apply_of]
      exact hfac.trans hfree
    · intro g hg
      let gCont : Fhat →ₜ* G := { toMonoidHom := g, continuous_toFun := hg.1 }
      have hfac' : gCont.comp ι = φfree := by
        apply ContinuousMonoidHom.toMonoidHom_injective
        ext x
        change g (ι (FreeGroup.of x)) = FreeGroup.lift φ (FreeGroup.of x)
        exact (hg.2 x).trans (by simp only [FreeGroup.lift_apply_of])
      exact congrArg ContinuousMonoidHom.toMonoidHom (hι.lift_unique hG φfree hfac')

def

lift

L1109 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.lift

Documentation

The lift supplied by the corresponding free pro-C universal property.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

def lift
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
    (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
    F →* G

theorem

lift_spec

L1120 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.lift_spec

Documentation

The universal-property lift has the prescribed values on the chosen generators.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem lift_spec
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
    (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
    Continuous (hι.lift hG φ hφ hgen) ∧
      ∀ x, hι.lift hG φ hφ hgen (ι x) = φ x

theorem

lift_unique

L1132 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.lift_unique

Documentation

The universal-property lift is unique among continuous maps with the prescribed values.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem lift_unique
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
    (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ))
    {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
    f = hι.lift hG φ hφ hgen

theorem

existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass

L1148 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass

Documentation

For a concrete finite-group class, the generated-target universal property of a free pro-C group on a converging set extends any target map that converges to 1. This formulation supports retractions that collapse all but finitely many basis elements.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)
    (φ : X → G) (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ) :
    ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x

theorem

existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass

L1248 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass

Documentation

Continuous-homomorphism form of existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)
    (φ : X → G) (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ) :
    ∃! f : F →ₜ* G, ∀ x, f (ι x) = φ x

theorem

generator_pow_ne_one_of_sigma

L1272 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.generator_pow_ne_one_of_sigma

Documentation

In a free pro-Σ group with nonempty Σ, a free generator has no positive torsion.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem generator_pow_ne_one_of_sigma
    {σ : Set ℕ} (hσ : ∃ p, p ∈ σ ∧ Nat.Prime p)
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := (ProCGroups.FiniteGroupClass.sigmaGroup σ)) X F ι)
    (i : X) (N : ℕ) (hN : 0 < N) :
    (ι i) ^ N ≠ 1

theorem

generator_zpow_ne_one_of_sigma

L1348 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.generator_zpow_ne_one_of_sigma

Documentation

Integer-power form of generator_pow_ne_one_of_sigma.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem generator_zpow_ne_one_of_sigma
    {σ : Set ℕ} (hσ : ∃ p, p ∈ σ ∧ Nat.Prime p)
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := (ProCGroups.FiniteGroupClass.sigmaGroup σ)) X F ι)
    (i : X) (n : ℤ) (hn : n ≠ 0) :
    (ι i) ^ n ≠ 1

def

liftHom

L1373 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.liftHom

Documentation

The continuous homomorphism supplied by the free pro-C universal property.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · full declaration

def liftHom
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
    (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
    F →ₜ* G where
  toMonoidHom := hι.lift hG φ hφ hgen
  continuous_toFun := (hι.lift_spec hG φ hφ hgen).1

def

liftConvergingGeneratingMap

L1385 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.liftConvergingGeneratingMap

Documentation

Bundled version of liftHom, taking a converging generating map as a single argument.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

def liftConvergingGeneratingMap
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : ConvergingGeneratingMap X G) :
    F →ₜ* G

theorem

liftConvergingGeneratingMap_apply

L1394 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.liftConvergingGeneratingMap_apply

Documentation

The bundled lift has the prescribed value on each generator.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem liftConvergingGeneratingMap_apply
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : ConvergingGeneratingMap X G) (x
        : X) :
    hι.liftConvergingGeneratingMap hG φ (ι x) = φ x

theorem

liftHom_apply

L1405 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.liftHom_apply

Documentation

liftHom has the prescribed value on each generator.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem liftHom_apply
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
    (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
    (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) (x : X) :
    hι.liftHom hG φ hφ hgen (ι x) = φ x

theorem

existsUnique_collapseToFinset_of_finiteGroupClass

L1426 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.existsUnique_collapseToFinset_of_finiteGroupClass

Documentation

The unique continuous endomorphism of a free pro-C group that keeps the finite set S of basis elements and sends the remaining basis elements to 1.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · full declaration

theorem existsUnique_collapseToFinset_of_finiteGroupClass
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    ∃! φ : F →ₜ* F, ∀ x, φ (ι x) = if x ∈ S then ι x else 1 := by
  have hconv :
      FamilyConvergesToOneAlongOpenSubgroups (G := F) (fun x => if x ∈ S then ι x else 1) := by
    intro U
    classical
    refine S.finite_toSet.subset ?_
    intro x hx
    by_cases hxS : x ∈ S
    · exact hxS
    · exfalso
      exact hx (by simp only [hxS, ↓reduceIte, SetLike.mem_coe, one_mem])
  exact
    hι.existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
      C C.isomClosed hVar.out.subgroupClosed
      hι.hasOpenNormalBasisInClass (fun x => if x ∈ S then ι x else 1) hconv

def

collapseToFinset

L1449 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinset

Documentation

The finite-support retraction of a free pro-C group onto the closed subgroup generated by a finite set of basis elements.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

def collapseToFinset
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    F →ₜ* F

theorem

collapseToFinset_apply_mem

L1458 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinset_apply_mem

Documentation

Collapsing to a finite set fixes the selected generators.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem collapseToFinset_apply_mem
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S : Finset X} {x : X} (hx : x ∈ S) :
    hι.collapseToFinset S (ι x) = ι x

theorem

collapseToFinset_apply_not_mem

L1469 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinset_apply_not_mem

Documentation

Collapsing to a finite set sends every unselected generator to the identity.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem collapseToFinset_apply_not_mem
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S : Finset X} {x : X} (hx : x ∉ S) :
    hι.collapseToFinset S (ι x) = 1

theorem

collapseToFinset_idempotent

L1480 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinset_idempotent

Documentation

Collapsing twice to the same finite set is the same as collapsing once.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem collapseToFinset_idempotent
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    (hι.collapseToFinset S).comp (hι.collapseToFinset S) =
      hι.collapseToFinset S

theorem

comp_collapseToFinset_eq_of_eq_one_outside

L1496 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.comp_collapseToFinset_eq_of_eq_one_outside

Documentation

A homomorphism that kills every basis element outside S is unchanged after precomposition with the finite-support retraction.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem comp_collapseToFinset_eq_of_eq_one_outside
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {G : Type w} [Group G] [TopologicalSpace G] [T2Space G]
    (φ : F →ₜ* G) (S : Finset X)
    (hφ : ∀ x, x ∉ S → φ (ι x) = 1) :
    φ.comp (hι.collapseToFinset S) = φ

def

collapseToFinsetRange

L1513 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinsetRange

Documentation

The map from the free pro-C group onto the range of its finite-support retraction.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

def collapseToFinsetRange
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    F →ₜ* ↥((hι.collapseToFinset S : F →* F).range)

def

collapseToFinsetInclusion

L1524 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinsetInclusion

Documentation

The inclusion of the range of a finite-support retraction back into the ambient free group.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

def collapseToFinsetInclusion
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    ↥((hι.collapseToFinset S : F →* F).range) →ₜ* F

abbrev

FinsetSupportRetract

L1534 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.FinsetSupportRetract

Documentation

The range of the finite-support retraction, viewed as the finite-basis retract.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

abbrev FinsetSupportRetract
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) : Type u

def

finsetSupportBasis

L1542 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.finsetSupportBasis

Documentation

The finite basis of the finite-support retract.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

def finsetSupportBasis
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    S → hι.FinsetSupportRetract S

theorem

isClosed_range_collapseToFinset

L1553 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.isClosed_range_collapseToFinset

Documentation

The range of the finite-support retraction is closed.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem isClosed_range_collapseToFinset
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    IsClosed (((hι.collapseToFinset S : F →* F).range : Set F))

instance

instCompactSpaceFinsetSupportRetract

L1577 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.instCompactSpaceFinsetSupportRetract

Documentation

The closed finite-support retract carries its canonical compact topology.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

instance instCompactSpaceFinsetSupportRetract
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    CompactSpace (hι.FinsetSupportRetract S)

theorem

hasOpenNormalBasisInClass_finsetSupportRetract

L1586 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.hasOpenNormalBasisInClass_finsetSupportRetract

Documentation

The finite-support retract again has an open-normal \(C\)-basis.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem hasOpenNormalBasisInClass_finsetSupportRetract
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (hι.FinsetSupportRetract S)

theorem

isFreeProCGroupOnConvergingSet_finsetSupportBasis

L1599 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.isFreeProCGroupOnConvergingSet_finsetSupportBasis

Documentation

The finite-support retract is free pro-C on its retained finite basis.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem isFreeProCGroupOnConvergingSet_finsetSupportBasis
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    (S : Finset X) :
    IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C)
      S (hι.FinsetSupportRetract S) (hι.finsetSupportBasis S)

theorem

collapseToFinset_small_comp_large_of_subset

L1729 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinset_small_comp_large_of_subset

Documentation

If S ⊆ T, then collapsing first to T and then to S is the same as collapsing directly to S. This is the basic compatibility relation for the finite-basis projections.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem collapseToFinset_small_comp_large_of_subset
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S T : Finset X} (hST : S ⊆ T) :
    (hι.collapseToFinset S).comp (hι.collapseToFinset T) =
      hι.collapseToFinset S

theorem

collapseToFinset_large_comp_small_of_subset

L1752 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.collapseToFinset_large_comp_small_of_subset

Documentation

If S ⊆ T, then collapsing to S and then to T is again the collapse to S. Equivalently, the finite-support image for S is fixed by every larger finite-support projection.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem collapseToFinset_large_comp_small_of_subset
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S T : Finset X} (hST : S ⊆ T) :
    (hι.collapseToFinset T).comp (hι.collapseToFinset S) =
      hι.collapseToFinset S

def

finsetSupportTransition

L1770 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.finsetSupportTransition

Documentation

The transition map from the finite-support retract for T to the one for S, for S ⊆ T. It is the projection obtained by including the T-retract into the ambient free pro-C group and then collapsing to S.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

def finsetSupportTransition
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S T : Finset X} :
    hι.FinsetSupportRetract T →ₜ* hι.FinsetSupportRetract S

theorem

finsetSupportTransition_apply_basis

L1784 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.finsetSupportTransition_apply_basis

Documentation

The transition from a larger finite support to a smaller one preserves the basis elements indexed by the smaller support.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem finsetSupportTransition_apply_basis
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S T : Finset X} (hST : S ⊆ T) (x : S) :
    hι.finsetSupportTransition (S := S) (T := T)
        (hι.finsetSupportBasis T ⟨x.1, hST x.2⟩) =
      hι.finsetSupportBasis S x

theorem

finsetSupportTransition_comp_collapseToFinsetRange

L1798 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.finsetSupportTransition_comp_collapseToFinsetRange

Documentation

Compatibility of the ambient projection F → R_T with the transition R_T → R_S.

Source context 22 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}
section FiniteSupportRetracts
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable {X : Type v} [DecidableEq X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}

Lean source · statement

theorem finsetSupportTransition_comp_collapseToFinsetRange
    (hι :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X F ι)
    {S T : Finset X} (hST : S ⊆ T) :
    (hι.finsetSupportTransition (S := S) (T := T)).comp (hι.collapseToFinsetRange T) =
      hι.collapseToFinsetRange S

theorem

hom_ext

L1815 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.hom_ext

Documentation

Continuous homomorphisms out of a free pro-C group on a converging generating set are determined by their values on the chosen generators.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem hom_ext
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
    {G : Type u} [Group G] [TopologicalSpace G] [T2Space G]
    {f g : F →ₜ* G} (hfg : ∀ x, f (ι x) = g (ι x)) :
    f = g

theorem

lift_id

L1827 ↗

ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.lift_id

Documentation

The lift of the canonical generator map to the same free pro-C group is the identity.

Source context 15 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}
namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
variable {X : Type v}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι : X → F}

Lean source · statement

theorem lift_id
    (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι) :
    hι.lift hι.hasOpenNormalBasisInClass ι hι.convergesToOneAlongOpenSubgroups
        hι.generates_range = MonoidHom.id F

structure

EpimorphicallyFreeProCGroupOnConvergingSetData

L1839 ↗

ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData

Documentation

Packaged carrier with the epimorphic convergent-family lifting property.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · full declaration

structure EpimorphicallyFreeProCGroupOnConvergingSetData
    (C : ProCGroups.FiniteGroupClass) where
  /-- The index type of the distinguished converging generating family. -/
  basis : Type u
  /-- The bundled pro-`C` group generated by the distinguished family. -/
  carrier : ProCGrp C
  /-- The distinguished family of elements of the bundled carrier. -/
  inclusion : basis → carrier
  /--
  The inclusion is convergent and generating, and satisfies the epimorphic free pro-`C`
  universal property.
  -/
  isEpimorphicallyFree :
    IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) basis carrier inclusion

theorem

basisCard_eq_topologicalRank_of_finiteBasis

L1858 ↗

ProCGroups.FreeProC.basisCard_eq_topologicalRank_of_finiteBasis

Documentation

The cardinality of a finite converging-set basis is the topological rank of the free pro-\(C\) group, provided the finite class has a nontrivial cyclic quotient witness.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem basisCard_eq_topologicalRank_of_finiteBasis
    (C : ProCGroups.FiniteGroupClass.{u})
    (hquot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    (hcyc :
      ∃ (A : Type u) (_ : Group A) (_ : Finite A),
        C A ∧ IsCyclic A ∧ Nontrivial A)
    (Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData
      (C := C))
    [Finite Fdata.basis] :
    Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier

theorem

freeOnFinitePointedDiscreteSpace_has_convergingSetBasis

L2048 ↗

ProCGroups.FreeProC.freeOnFinitePointedDiscreteSpace_has_convergingSetBasis

Documentation

For a finite discrete pointed space, removing the basepoint from the pointed generating family gives a converging-set basis.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · full declaration

theorem freeOnFinitePointedDiscreteSpace_has_convergingSetBasis
    {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] {x0 : X}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hι : IsEpimorphicallyPointedFreeProCGroupOn (C := C) X x0 F ι) :
    IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) {x : X // x ≠ x0} F (fun x => ι x) := by
  classical
  let μ : {x : X // x ≠ x0} → F := fun x => ι x
  refine ⟨hι.hasOpenNormalBasisInClass, ?_, ?_, ?_⟩
  · exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := F) μ
  · have hrange : Set.range ι = Set.range μ ∪ ({1} : Set F) := by
      ext z
      constructor
      · rintro ⟨x, rfl⟩
        by_cases hx : x = x0
        · right
          simpa [hx] using hι.map_base
        · left
          exact ⟨⟨x, hx⟩, rfl⟩
      · intro hz
        rcases hz with hz | hz
        · rcases hz with ⟨x, rfl⟩
          exact ⟨x, rfl⟩
        · exact ⟨x0, hι.map_base.trans (by simpa using hz.symm)⟩
    have hgen' :
        Generation.TopologicallyGenerates (G := F) (Set.range μ ∪ ({1} : Set F)) := by
      simpa [μ, hrange] using hι.generates_range
    exact (Generation.topologicallyGenerates_union_one_iff (G := F) (X := Set.range μ)).1 hgen'
  · intro G _ _ _ _ _ _ hG φ _hφconv hgenφ
    let φhat : X → G := fun x => if h : x = x0 then 1 else φ ⟨x, h⟩
    have hφhat : Continuous φhat := continuous_of_discreteTopology
    have hφhat0 : φhat x0 = 1 := by
      simp only [ne_eq, ↓reduceDIte, φhat]
    have hrange : Set.range φhat = Set.range φ ∪ ({1} : Set G) := by
      ext z
      constructor
      · rintro ⟨x, rfl⟩
        by_cases hx : x = x0
        · right
          simp only [ne_eq, hx, ↓reduceDIte, mem_singleton_iff, φhat]
        · left
          exact ⟨⟨x, hx⟩, by simp only [ne_eq, hx, ↓reduceDIte, φhat]⟩
      · intro hz
        rcases hz with hz | hz
        · rcases hz with ⟨x, rfl⟩
          exact ⟨x, by simp only [ne_eq, x.2, ↓reduceDIte, Subtype.coe_eta, φhat]⟩
        · exact ⟨x0, by simpa [φhat] using hz.symm⟩
    have hφhatgen :
        Generation.TopologicallyGenerates (G := G) (Set.range φhat) := by
      have hgen' :
          Generation.TopologicallyGenerates (G := G) (Set.range φ ∪ ({1} : Set G)) := by
        exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range φ)).2 hgenφ
      simpa [φhat, hrange] using hgen'
    rcases hι.existsUnique_lift hG φhat hφhat hφhat0 hφhatgen with ⟨f, hf, huniq⟩
    refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
    · intro x
      simpa [μ, φhat, x.2] using hf.2 (x : X)
    · intro g hg
      apply huniq g
      refine ⟨hg.1, ?_⟩
      intro x
      by_cases hx : x = x0
      · calc
          g (ι x) = g (ι x0) := by rw [hx]
          _ = g 1 := by rw [hι.map_base]
          _ = 1 := map_one g
          _ = φhat x := by simp only [ne_eq, hx, ↓reduceDIte, φhat]
      · simpa [μ, φhat, hx] using hg.2 ⟨x, hx⟩

theorem

freeOnFinitePointedDiscreteSpace_has_finiteConvergingSetBasis

L2120 ↗

ProCGroups.FreeProC.freeOnFinitePointedDiscreteSpace_has_finiteConvergingSetBasis

Documentation

For a finite discrete pointed space, the resulting converging-set basis is finite.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
open ProCGroups
open ProCGroups.FiniteGeneration
section
variable {C : ProCGroups.FiniteGroupClass}

Lean source · statement

theorem freeOnFinitePointedDiscreteSpace_has_finiteConvergingSetBasis
    {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] {x0 : X}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hι : IsEpimorphicallyPointedFreeProCGroupOn (C := C) X x0 F ι) :
    ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} (C := C),
      Nonempty (Fdata.carrier ≃ₜ* F) ∧ Finite Fdata.basis

Module documentation

Pro C Groups / Free pro-C / Basic

Declarations