Module

CharacteristicChainsAndIndices.lean

Nyll.ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

49 declarations indexed from sourceView source ↗

Module documentation

Characteristic chains from bounded-index intersections

For a topologically finitely generated profinite group, the intersection of all open subgroups of index at most \(n\) is open and topologically characteristic. These intersections form a descending countable basis at the identity.

Imports2

Imported by7

def

OpenSubgroupsOfIndexLE

L37 ↗

ProCGroups.FiniteGeneration.OpenSubgroupsOfIndexLE

Documentation

The open subgroups of index at most \(n\). This is the bounded-index family whose intersection defines the characteristic core.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def OpenSubgroupsOfIndexLE (G : Type u) [Group G] [TopologicalSpace G]
    (n : ℕ) : Set (Subgroup G)

def

OpenNormalSubgroupsOfIndex

L42 ↗

ProCGroups.FiniteGeneration.OpenNormalSubgroupsOfIndex

Documentation

The family of open normal subgroups of index exactly \(n\).

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def OpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
    (n : ℕ) : Set (Subgroup G)

theorem

mem_openSubgroupsOfIndexLE

L51 ↗

ProCGroups.FiniteGeneration.mem_openSubgroupsOfIndexLE

Documentation

Membership criterion for the finite set of open subgroups of index at most n.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem mem_openSubgroupsOfIndexLE {n : ℕ} {H : Subgroup G} :
    H ∈ OpenSubgroupsOfIndexLE (G := G) n ↔
      IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ n

theorem

mem_openNormalSubgroupsOfIndex

L57 ↗

ProCGroups.FiniteGeneration.mem_openNormalSubgroupsOfIndex

Documentation

Membership criterion for the finite set of open normal subgroups of a fixed index.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem mem_openNormalSubgroupsOfIndex {n : ℕ} {U : Subgroup G} :
    U ∈ OpenNormalSubgroupsOfIndex (G := G) n ↔
      U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n

def

CharacteristicIndexIntersection

L66 ↗

ProCGroups.FiniteGeneration.CharacteristicIndexIntersection

Documentation

The canonical bounded-index intersection Vₙ = ⋂ {H ≤ G | H open and [G : H] ≤ n}.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def CharacteristicIndexIntersection (G : Type u) [Group G] [TopologicalSpace G]
    (n : ℕ) : Subgroup G

theorem

characteristicIndexIntersection_def

L71 ↗

ProCGroups.FiniteGeneration.characteristicIndexIntersection_def

Documentation

The characteristic index intersection is the infimum of all open subgroups of bounded index.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem characteristicIndexIntersection_def (n : ℕ) :
    CharacteristicIndexIntersection (G := G) n =
      sInf (OpenSubgroupsOfIndexLE (G := G) n)

def

HasFiniteOpenSubgroupsOfIndex

L77 ↗

ProCGroups.FiniteGeneration.HasFiniteOpenSubgroupsOfIndex

Documentation

A group has only finitely many open subgroups of each prescribed index.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def HasFiniteOpenSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
    : Prop

def

HasFiniteOpenNormalSubgroupsOfIndex

L83 ↗

ProCGroups.FiniteGeneration.HasFiniteOpenNormalSubgroupsOfIndex

Documentation

Normal-subgroup version of fixed-index finiteness.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def HasFiniteOpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
    : Prop

theorem

toHasFiniteOpenNormalSubgroupsOfIndex

L94 ↗

ProCGroups.FiniteGeneration.HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex

Documentation

Finiteness of open subgroups of each index implies finiteness of open normal subgroups of each index.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex
    (h : HasFiniteOpenSubgroupsOfIndex G) :
    HasFiniteOpenNormalSubgroupsOfIndex G

theorem

continuousMonoidHom_eq_of_eqOn_topologicalGenerators

L103 ↗

ProCGroups.FiniteGeneration.continuousMonoidHom_eq_of_eqOn_topologicalGenerators

Documentation

Continuous homomorphisms are equal when they agree on a topological generating set.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem continuousMonoidHom_eq_of_eqOn_topologicalGenerators
    [IsTopologicalGroup G]
    {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
    {s : Finset G} (hsgen : TopologicallyGenerates (G := G) (↑s : Set G))
    {f g : ContinuousMonoidHom G R}
    (hfg : ∀ x ∈ (↑s : Set G), f x = g x) :
    f = g

theorem

finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated

L141 ↗

ProCGroups.FiniteGeneration.finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated

Documentation

A finitely generated profinite group admits only finitely many continuous homomorphisms into a fixed finite discrete target.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated
    [IsTopologicalGroup G]
    {R : Type v} [Group R] [TopologicalSpace R] [T2Space R] [Finite R]
    (hG : TopologicallyFinitelyGenerated G) :
    Finite (ContinuousMonoidHom G R)

def

openSubgroupIndexEquiv

L157 ↗

ProCGroups.FiniteGeneration.openSubgroupIndexEquiv

Documentation

The chosen identification G ⧸ H ≃ Fin n for an index-n subgroup.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def openSubgroupIndexEquiv
    (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
    (hn : Nat.card (G ⧸ H) = n) :
    (G ⧸ H) ≃ Fin n

def

openSubgroupIndexAction

L166 ↗

ProCGroups.FiniteGeneration.openSubgroupIndexAction

Documentation

The coset action of G on the n cosets of an index-n subgroup, transported to Fin n.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def openSubgroupIndexAction
    (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
    (hn : Nat.card (G ⧸ H) = n) :
    G →* Equiv.Perm (Fin n)

def

openSubgroupIndexBasepoint

L175 ↗

ProCGroups.FiniteGeneration.openSubgroupIndexBasepoint

Documentation

The image of the identity coset under the chosen Fin n identification.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def openSubgroupIndexBasepoint
    (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
    (hn : Nat.card (G ⧸ H) = n) : Fin n

instance

instTopologicalSpaceFinitePerm

L181 ↗

ProCGroups.FiniteGeneration.instTopologicalSpaceFinitePerm

Documentation

The finite permutation type has its canonical topological space structure.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

instance instTopologicalSpaceFinitePerm (n : ℕ) : TopologicalSpace (Equiv.Perm (Fin n))

instance

instDiscreteTopologyFinitePerm

L185 ↗

ProCGroups.FiniteGeneration.instDiscreteTopologyFinitePerm

Documentation

The finite permutation type carries the discrete topology.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

instance instDiscreteTopologyFinitePerm (n : ℕ) : DiscreteTopology (Equiv.Perm (Fin n))

instance

instIsTopologicalGroupFinitePerm

L189 ↗

ProCGroups.FiniteGeneration.instIsTopologicalGroupFinitePerm

Documentation

The finite permutation group is a topological group with the discrete topology.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

instance instIsTopologicalGroupFinitePerm (n : ℕ) : IsTopologicalGroup (Equiv.Perm (Fin n))

instance

instFiniteFinitePerm

L193 ↗

ProCGroups.FiniteGeneration.instFiniteFinitePerm

Documentation

The finite permutation type is finite.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

instance instFiniteFinitePerm (n : ℕ) : Finite (Equiv.Perm (Fin n))

def

openSubgroupIndexContinuousHom

L198 ↗

ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom

Documentation

The finite coset action, viewed as a continuous homomorphism into a discrete permutation group.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def openSubgroupIndexContinuousHom
    [IsTopologicalGroup G] [CompactSpace G]
    (H : Subgroup G) (hH : IsOpen (H : Set G)) {n : ℕ}
    (hHfinite : Finite (G ⧸ H)) (hn : Nat.card (G ⧸ H) = n) :
    G →ₜ* Equiv.Perm (Fin n)

theorem

mem_openSubgroup_iff_indexAction_fix_basepoint

L233 ↗

ProCGroups.FiniteGeneration.mem_openSubgroup_iff_indexAction_fix_basepoint

Documentation

Membership in an open subgroup is equivalent to fixing the basepoint in its coset action.

Source context 10 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]
omit [TopologicalSpace G] in

Lean source · statement

theorem mem_openSubgroup_iff_indexAction_fix_basepoint
    {H : Subgroup G} (hHfinite : Finite (G ⧸ H)) {n : ℕ}
    (hn : Nat.card (G ⧸ H) = n) {g : G} :
    g ∈ H ↔
      openSubgroupIndexAction (G := G) H hHfinite hn g
          (openSubgroupIndexBasepoint (G := G) H hHfinite hn) =
        openSubgroupIndexBasepoint (G := G) H hHfinite hn

theorem

hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated

L255 ↗

ProCGroups.FiniteGeneration.hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated

Documentation

Finitely generated profinite groups have only finitely many open subgroups of each index.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated
    [IsTopologicalGroup G] [CompactSpace G]
    (hG : TopologicallyFinitelyGenerated G) :
    HasFiniteOpenSubgroupsOfIndex G

theorem

finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex

L316 ↗

ProCGroups.FiniteGeneration.finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex

Documentation

Bounding the index by \(n\) still yields only finitely many open subgroups.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex
    (hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :
    Set.Finite (OpenSubgroupsOfIndexLE (G := G) n)

theorem

isOpen_sInf_of_finite

L326 ↗

ProCGroups.FiniteGeneration.Subgroup.isOpen_sInf_of_finite

Documentation

The infimum of a finite family of open subgroups is open.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem Subgroup.isOpen_sInf_of_finite
    {S : Set (Subgroup G)} (hS : S.Finite)
    (hopen : ∀ H ∈ S, IsOpen (H : Set G)) :
    IsOpen ((sInf S : Subgroup G) : Set G)

theorem

characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex

L342 ↗

ProCGroups.FiniteGeneration.characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex

Documentation

The bounded-index characteristic intersection is open once the bounded-index family is finite.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex
    (hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :
    IsOpen ((CharacteristicIndexIntersection (G := G) n : Set G))

theorem

characteristicIndexIntersection_antitone

L351 ↗

ProCGroups.FiniteGeneration.characteristicIndexIntersection_antitone

Documentation

The bounded-index characteristic intersections form a descending chain.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem characteristicIndexIntersection_antitone :
    Antitone (CharacteristicIndexIntersection (G := G))

theorem

characteristicIndexIntersection_isTopologicallyCharacteristic

L359 ↗

ProCGroups.FiniteGeneration.characteristicIndexIntersection_isTopologicallyCharacteristic

Documentation

The finite-index characteristic intersection is characteristic.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem characteristicIndexIntersection_isTopologicallyCharacteristic
    [IsTopologicalGroup G] [CompactSpace G]
    (n : ℕ) :
    IsTopologicallyCharacteristic G (CharacteristicIndexIntersection (G := G) n)

theorem

characteristicIndexIntersection_cofinal_of_openSubgroup

L387 ↗

ProCGroups.FiniteGeneration.characteristicIndexIntersection_cofinal_of_openSubgroup

Documentation

Characteristic index intersections are cofinal among open subgroups.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem characteristicIndexIntersection_cofinal_of_openSubgroup
    [IsTopologicalGroup G] [CompactSpace G]
    (U : Subgroup G) (hU : IsOpen (U : Set G)) :
    ∃ n, CharacteristicIndexIntersection (G := G) n ≤ U

theorem

exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated

L402 ↗

ProCGroups.FiniteGeneration.exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated

Documentation

Topologically finitely generated profinite groups have a countable characteristic open basis at the identity.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated
    [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
    : TopologicallyFinitelyGenerated G →
        ∃ V : ℕ → Subgroup G,
          V 0 = ⊤ ∧
          Antitone V ∧
          (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
          (∀ n, IsTopologicallyCharacteristic G (V n)) ∧
          ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U

theorem

finiteIndexOpenSubgroups_and_charBasis_of_tfg

L456 ↗

ProCGroups.FiniteGeneration.finiteIndexOpenSubgroups_and_charBasis_of_tfg

Documentation

Finitely generated profinite groups have finite fixed-index open-subgroup sets and a countable characteristic open basis at the identity.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section IndexFamilies
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem finiteIndexOpenSubgroups_and_charBasis_of_tfg
    [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : TopologicallyFinitelyGenerated G) :
    HasFiniteOpenSubgroupsOfIndex G ∧
      ∃ V : ℕ → Subgroup G,
        V 0 = ⊤ ∧
        Antitone V ∧
        (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
        (∀ n, IsTopologicallyCharacteristic G (V n)) ∧
        ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U

theorem

surjOn_of_injOn_mapsTo

L479 ↗

ProCGroups.FiniteGeneration.Set.Finite.surjOn_of_injOn_mapsTo

Documentation

An injective self-map of a finite set is automatically surjective on that set.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace Set

Lean source · statement

theorem Finite.surjOn_of_injOn_mapsTo {α : Type*} {s : Set α}
    (hs : s.Finite) {f : α → α}
    (hf : MapsTo f s s) (hinj : InjOn f s) :
    SurjOn f s s

def

OpenNormalSeparatesPoints

L499 ↗

ProCGroups.FiniteGeneration.OpenNormalSeparatesPoints

Documentation

Open normal subgroups separate the identity from every nontrivial element.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def OpenNormalSeparatesPoints (G : Type u) [Group G] [TopologicalSpace G]
    : Prop

theorem

injective_of_ker_le_every_openNormal

L507 ↗

ProCGroups.FiniteGeneration.injective_of_ker_le_every_openNormal

Documentation

If every kernel element lies in every open normal subgroup and open normal subgroups separate points, then the endomorphism is injective.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem injective_of_ker_le_every_openNormal
    {φ : ContinuousMonoidHom G G}
    (hker : ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U)
    (hsep : OpenNormalSeparatesPoints G) :
    Function.Injective φ

def

PreimagePreservesOpenNormalSubgroupsOfIndex

L525 ↗

ProCGroups.FiniteGeneration.PreimagePreservesOpenNormalSubgroupsOfIndex

Documentation

The preimage operator preserves the fixed-index family of open normal subgroups.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def PreimagePreservesOpenNormalSubgroupsOfIndex
    (φ : ContinuousMonoidHom G G) : Prop

theorem

subgroupComap_injective_of_surjective

L534 ↗

ProCGroups.FiniteGeneration.subgroupComap_injective_of_surjective

Documentation

Comap along a surjective homomorphism is injective on subgroups.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]
omit [TopologicalSpace G] in

Lean source · statement

theorem subgroupComap_injective_of_surjective
    {H : Type v} [Group H]
    (f : G →* H) (hf : Function.Surjective f) :
    Function.Injective (Subgroup.comap f)

theorem

preimage_injectiveOn_openNormalSubgroupsOfIndex

L551 ↗

ProCGroups.FiniteGeneration.preimage_injectiveOn_openNormalSubgroupsOfIndex

Documentation

Preimage under a surjective endomorphism is injective on each fixed-index open-normal family.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · full declaration

theorem preimage_injectiveOn_openNormalSubgroupsOfIndex
    {φ : ContinuousMonoidHom G G}
    (hφsurj : Function.Surjective φ) (n : ℕ) :
    Set.InjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
      (OpenNormalSubgroupsOfIndex (G := G) n) := by
  intro U hU V hV hEq
  exact subgroupComap_injective_of_surjective (G := G) φ.toMonoidHom hφsurj hEq

def

PreimageSurjectiveOnOpenNormalSubgroupsOfIndex

L563 ↗

ProCGroups.FiniteGeneration.PreimageSurjectiveOnOpenNormalSubgroupsOfIndex

Documentation

Surjectivity of the preimage operator on each family of open normal subgroups of index \(n\). This is exactly the conclusion obtained from the finiteness of the family \(U_n\).

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def PreimageSurjectiveOnOpenNormalSubgroupsOfIndex
    (φ : ContinuousMonoidHom G G) : Prop

theorem

preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite

L574 ↗

ProCGroups.FiniteGeneration.preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite

Documentation

For finite groups, preimage along a surjective endomorphism is surjective on open normal subgroups of fixed index.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite
    {φ : ContinuousMonoidHom G G}
    (hfin : HasFiniteOpenNormalSubgroupsOfIndex G)
    (hφsurj : Function.Surjective φ)
    (hpres : PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :
    PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ

theorem

ker_le_every_openNormal_of_preimageSurjectiveOn_index

L591 ↗

ProCGroups.FiniteGeneration.ker_le_every_openNormal_of_preimageSurjectiveOn_index

Documentation

If the preimage map is surjective on every fixed-index open-normal family, then \(\ker \varphi \le U\) for every open normal subgroup \(U\).

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem ker_le_every_openNormal_of_preimageSurjectiveOn_index
    [IsTopologicalGroup G] [CompactSpace G]
    {φ : ContinuousMonoidHom G G}
    (hφ : PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ) :
    ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U

theorem

injective_of_preimageSurjectiveOn_openNormalIndex

L613 ↗

ProCGroups.FiniteGeneration.injective_of_preimageSurjectiveOn_openNormalIndex

Documentation

The fixed-index Hopfian kernel-separation hypotheses imply injectivity.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem injective_of_preimageSurjectiveOn_openNormalIndex
    [IsTopologicalGroup G] [CompactSpace G]
    {φ : ContinuousMonoidHom G G}
    (hφ : PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ)
    (hsep : OpenNormalSeparatesPoints G) :
    Function.Injective φ

def

ContinuousHopfian

L627 ↗

ProCGroups.FiniteGeneration.ContinuousHopfian

Documentation

A topological group is continuously Hopfian if every surjective continuous endomorphism is injective.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def ContinuousHopfian (G : Type u) [Group G] [TopologicalSpace G] : Prop

def

SurjectiveContinuousEndomorphismsAreAutomorphisms

L631 ↗

ProCGroups.FiniteGeneration.SurjectiveContinuousEndomorphismsAreAutomorphisms

Documentation

Every surjective continuous endomorphism is induced by a continuous automorphism.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def SurjectiveContinuousEndomorphismsAreAutomorphisms
    (G : Type u) [Group G] [TopologicalSpace G] : Prop

def

toContinuousMulEquivOfBijective

L640 ↗

ProCGroups.FiniteGeneration.ContinuousMonoidHom.toContinuousMulEquivOfBijective

Documentation

Upgrade a continuous bijective endomorphism of a compact Hausdorff topological group to a continuous automorphism.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def ContinuousMonoidHom.toContinuousMulEquivOfBijective
    [CompactSpace G] [T2Space G]
    (φ : ContinuousMonoidHom G G) (hφ : Function.Bijective φ) :
    G ≃ₜ* G

theorem

surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian

L653 ↗

ProCGroups.FiniteGeneration.surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian

Documentation

A continuously Hopfian group has all surjective continuous endomorphisms invertible.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian
    [CompactSpace G] [T2Space G]
    (hhopf : ContinuousHopfian G) :
    SurjectiveContinuousEndomorphismsAreAutomorphisms G

theorem

continuousHopfian_of_preimageSurjectiveOn_openNormalIndex

L668 ↗

ProCGroups.FiniteGeneration.continuousHopfian_of_preimageSurjectiveOn_openNormalIndex

Documentation

Once the preimage-surjectivity statement on fixed-index open normal subgroups is available for all surjective continuous endomorphisms, the Hopfian conclusion follows mathematically.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem continuousHopfian_of_preimageSurjectiveOn_openNormalIndex
    [IsTopologicalGroup G] [CompactSpace G]
    (hsep : OpenNormalSeparatesPoints G)
    (hpre : ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
      PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ) :
    ContinuousHopfian G

theorem

continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex

L678 ↗

ProCGroups.FiniteGeneration.continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex

Documentation

Finiteness of open normal subgroups of each index implies the continuous Hopfian property.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex
    [IsTopologicalGroup G] [CompactSpace G]
    (hsep : OpenNormalSeparatesPoints G)
    (hfin : HasFiniteOpenNormalSubgroupsOfIndex G)
    (hpres :
      ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
        PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :
    ContinuousHopfian G

theorem

surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex

L692 ↗

ProCGroups.FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex

Documentation

Fixed-index finiteness of open normal subgroups implies the profinite Hopfian conclusion.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (hsep : OpenNormalSeparatesPoints G)
    (hfin : HasFiniteOpenNormalSubgroupsOfIndex G)
    (hpres :
      ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
        PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :
    SurjectiveContinuousEndomorphismsAreAutomorphisms G

theorem

openNormalSeparatesPoints_of_profinite

L706 ↗

ProCGroups.FiniteGeneration.openNormalSeparatesPoints_of_profinite

Documentation

In a profinite group, open normal subgroups separate the identity from every nontrivial element.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem openNormalSeparatesPoints_of_profinite
    [IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :
    OpenNormalSeparatesPoints G

theorem

preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective

L724 ↗

ProCGroups.FiniteGeneration.preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective

Documentation

Preimage along a surjective continuous endomorphism preserves open normal subgroups of fixed index.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective
    [IsTopologicalGroup G] [CompactSpace G]
    {φ : ContinuousMonoidHom G G} (hφsurj : Function.Surjective φ) :
    PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ

theorem

surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated

L741 ↗

ProCGroups.FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated

Documentation

A surjective continuous endomorphism of a topologically finitely generated profinite group is automatically a continuous automorphism.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
open ProCGroups.ProC
section HopfianStep
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    : TopologicallyFinitelyGenerated G →
        ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
          ∃ e : G ≃ₜ* G, ∀ x : G, e x = φ x

Module documentation

Characteristic chains from bounded-index intersections

Declarations