NYLL
Module

Index.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Index
18 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / All Finite / Index

This module defines the reverse-ordered finite-quotient indices for the all-finite completion, their quotient groups and quotient projections, and the mutually inverse conversions with \(C\)-indexed quotients when a formation contains all finite quotients of the group.

Imports1
Imported by4

Declarations

abbrev

CompletedGroupAlgebraIndex

L36 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraIndex
Documentation

The index set for the Section 5.3 completed group algebra tower, ordered so that larger indices give finer finite quotients.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev CompletedGroupAlgebraIndex
abbrev

CompletedGroupAlgebraQuotient

L40 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraQuotient
Documentation

The finite quotient \(G/U\) attached to one index of the completed-group-algebra tower.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev CompletedGroupAlgebraQuotient (U : CompletedGroupAlgebraIndex G) : Type v
instance

instFiniteCompletedGroupAlgebraQuotient

L44 ↗
CompletedGroupAlgebra.instFiniteCompletedGroupAlgebraQuotient
Documentation

The finite completed group-algebra quotient is finite.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instFiniteCompletedGroupAlgebraQuotient
    (U : CompletedGroupAlgebraIndex G) :
    Finite (CompletedGroupAlgebraQuotient G U)
def

terminalCompletedGroupAlgebraSubgroup

L50 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraSubgroup
Documentation

The whole group \(G\), as a subgroup, used for the terminal quotient \(G/G\).

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def terminalCompletedGroupAlgebraSubgroup : Subgroup G where
  carrier := Set.univ
  one_mem' := by simp only [Set.mem_univ]
  mul_mem' := by intro a b ha hb; simp only [Set.mem_univ]
  inv_mem' := by intro a ha; simp only [Set.mem_univ]
def

terminalCompletedGroupAlgebraOpenSubgroup

L57 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraOpenSubgroup
Documentation

The whole group \(G\) is an open subgroup.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def terminalCompletedGroupAlgebraOpenSubgroup : OpenSubgroup G
def

terminalCompletedGroupAlgebraOpenNormalSubgroup

L61 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraOpenNormalSubgroup
Documentation

The whole group \(G\) is an open normal subgroup.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def terminalCompletedGroupAlgebraOpenNormalSubgroup : OpenNormalSubgroup G
theorem

terminalCompletedGroupAlgebraOpenNormalSubgroup_coe

L74 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraOpenNormalSubgroup_coe
Documentation

The terminal all-finite open normal subgroup has underlying subgroup equal to the top subgroup.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem terminalCompletedGroupAlgebraOpenNormalSubgroup_coe :
    ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G) =
      ⊤
instance

terminalCompletedGroupAlgebraQuotient_subsingleton

L88 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraQuotient_subsingleton
Documentation

The terminal completed group-algebra quotient is a subsingleton, since it is the quotient by the whole group.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance terminalCompletedGroupAlgebraQuotient_subsingleton :
    Subsingleton
      (G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
        Subgroup G))
def

terminalCompletedGroupAlgebraSubgroupInClass

L100 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraSubgroupInClass
Documentation

The terminal open normal subgroup belongs to the finite-quotient indexing family.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def terminalCompletedGroupAlgebraSubgroupInClass :
    OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G
def

terminalCompletedGroupAlgebraIndex

L110 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex
Documentation

The terminal all-finite index, corresponding to the quotient \(G/G\).

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def terminalCompletedGroupAlgebraIndex : CompletedGroupAlgebraIndex G
instance

instNonemptyCompletedGroupAlgebraIndex

L117 ↗
CompletedGroupAlgebra.instNonemptyCompletedGroupAlgebraIndex
Documentation

The completed group algebra is nonempty, with the terminal quotient or canonical base object as witness.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instNonemptyCompletedGroupAlgebraIndex :
    Nonempty (CompletedGroupAlgebraIndex G)
theorem

terminalCompletedGroupAlgebraIndex_le

L123 ↗
CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le
Documentation

The terminal all-finite index is below every all-finite completed-group-algebra index.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem terminalCompletedGroupAlgebraIndex_le (U : CompletedGroupAlgebraIndex G) :
    terminalCompletedGroupAlgebraIndex G ≤ U
def

completedGroupAlgebraIndexInClassToAllFinite

L132 ↗
CompletedGroupAlgebra.completedGroupAlgebraIndexInClassToAllFinite
Documentation

A quotient indexed by a finite quotient class is also an all-finite quotient.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraIndexInClassToAllFinite
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) : CompletedGroupAlgebraIndex G
theorem

completedGroupAlgebraIndexInClassToAllFinite_le

L140 ↗
CompletedGroupAlgebra.completedGroupAlgebraIndexInClassToAllFinite_le
Documentation

The comparison of all-finite and class-indexed indices is monotone.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraIndexInClassToAllFinite_le
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    completedGroupAlgebraIndexInClassToAllFinite G C U ≤
      completedGroupAlgebraIndexInClassToAllFinite G C V
def

completedGroupAlgebraIndexToInClass

L152 ↗
CompletedGroupAlgebra.completedGroupAlgebraIndexToInClass
Documentation

For a pro-\(C\) group over a formation, every all-finite open-normal quotient is a \(C\)-quotient.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraIndexToInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hG : HasOpenNormalBasisInClass C G)
    (U : CompletedGroupAlgebraIndex G) : CompletedGroupAlgebraIndexInClass G C
theorem

completedGroupAlgebraIndexToInClass_le

L162 ↗
CompletedGroupAlgebra.completedGroupAlgebraIndexToInClass_le
Documentation

The comparison of all-finite and class-indexed indices is monotone.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraIndexToInClass_le
    (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hG : HasOpenNormalBasisInClass C G)
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    completedGroupAlgebraIndexToInClass G C hForm hG U ≤
      completedGroupAlgebraIndexToInClass G C hForm hG V
theorem

completedGroupAlgebraIndexInClassToAllFinite_indexToInClass

L177 ↗
CompletedGroupAlgebra.completedGroupAlgebraIndexInClassToAllFinite_indexToInClass
Documentation

For a pro-\(C\) group, converting an all-finite completed-group-algebra index to the \(C\)-indexed tower and then back to the all-finite tower returns the original index.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraIndexInClassToAllFinite_indexToInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
    (U : CompletedGroupAlgebraIndex G) :
    completedGroupAlgebraIndexInClassToAllFinite G C
        (completedGroupAlgebraIndexToInClass G C hForm hG U) = U
theorem

completedGroupAlgebraIndexToInClass_indexInClassToAllFinite

L195 ↗
CompletedGroupAlgebra.completedGroupAlgebraIndexToInClass_indexInClassToAllFinite
Documentation

For a pro-\(C\) group, converting a \(C\)-indexed completed-group-algebra index to the all-finite tower and then back to the \(C\)-indexed tower returns the original index.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraIndexToInClass_indexInClassToAllFinite
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
    (U : CompletedGroupAlgebraIndexInClass G C) :
    completedGroupAlgebraIndexToInClass G C hForm hG
        (completedGroupAlgebraIndexInClassToAllFinite G C U) = U

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