NYLL
Module

Stage.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Stage
13 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / All Finite / Stage

This module defines the finite group-algebra stages \(R[G/U]\), coefficient-change maps, quotient-transition ring homomorphisms, their compatibility laws, and the topological inverse system used by the all-finite completion.

Imports2
Imported by2

Declarations

abbrev

CompletedGroupAlgebraStage

L35 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraStage
Documentation

The finite-stage group algebra \(R[G/U]\) from Ribes--Zalesskii, Section 5.3.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
abbrev CompletedGroupAlgebraStage (R : Type u) (G : Type v) [CommRing R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    Type (max u v)
def

completedGroupAlgebraStageCoeffMap

L44 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMap
Documentation

For a homomorphism \(f:R\to S\), coefficient change at a fixed finite stage sends \(R[G/U]\) to \(S[G/U]\) by applying \(f\) to each coefficient and leaving the quotient support unchanged.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
def completedGroupAlgebraStageCoeffMap
    (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraStage R G U →+* CompletedGroupAlgebraStage S G U
theorem

completedGroupAlgebraStageCoeffMap_single

L55 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMap_single
Documentation

The coefficient-change map on a finite stage sends the singleton basis function supported at \(q\) with coefficient \(r\) to the singleton supported at the same \(q\) with coefficient \(f(r)\).

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraStageCoeffMap_single
    (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G)
    (q : CompletedGroupAlgebraQuotient G U) (r : R) :
    completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
        (MonoidAlgebra.single q r) =
      MonoidAlgebra.single q (f r)
theorem

completedGroupAlgebraStageCoeffMap_comp

L68 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMap_comp
Documentation

At an all-finite stage \(U\), changing coefficients first along \(f\) and then along \(g\) equals changing coefficients along \(g\circ f\).

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraStageCoeffMap_comp
    (S : Type w) (T : Type*) [CommRing S] [CommRing T]
    (f : R →+* S) (g : S →+* T) (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
        (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) =
      completedGroupAlgebraStageCoeffMap (R := R) (G := G) T (g.comp f) U
theorem

finite_completedGroupAlgebraStage

L78 ↗
CompletedGroupAlgebra.finite_completedGroupAlgebraStage
Documentation

A finite coefficient ring gives finite all-finite completed-group-algebra stages.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem finite_completedGroupAlgebraStage [Finite R] (U : CompletedGroupAlgebraIndex G) :
    Finite (CompletedGroupAlgebraStage R G U)
def

completedGroupAlgebraTransition

L89 ↗
CompletedGroupAlgebra.completedGroupAlgebraTransition
Documentation

The transition map \(R[G/V] \to R[G/U]\) is induced by the quotient map \(G/V \to G/U\).

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
def completedGroupAlgebraTransition (R : Type u) (G : Type v) [CommRing R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) :
    CompletedGroupAlgebraStage R G V →+* CompletedGroupAlgebraStage R G U
theorem

completedGroupAlgebraTransition_of

L100 ↗
CompletedGroupAlgebra.completedGroupAlgebraTransition_of
Documentation

The transition map sends a basis element to the induced basis element.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraTransition_of
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (g : CompletedGroupAlgebraQuotient G V) :
    completedGroupAlgebraTransition R G hUV (MonoidAlgebra.of R _ g) =
      MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1
theorem

completedGroupAlgebraTransition_single

L125 ↗
CompletedGroupAlgebra.completedGroupAlgebraTransition_single
Documentation

The transition map \(R[G/V] \to R[G/U]\) sends a singleton supported at a class of \(G/V\) to the singleton supported at its image in \(G/U\), with the same coefficient.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraTransition_single
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (q : CompletedGroupAlgebraQuotient G V) (r : R) :
    completedGroupAlgebraTransition R G hUV (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r
theorem

completedGroupAlgebraTransition_id

L148 ↗
CompletedGroupAlgebra.completedGroupAlgebraTransition_id
Documentation

The transition map for the reflexive relation is the identity.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraTransition_id (U : CompletedGroupAlgebraIndex G) :
    completedGroupAlgebraTransition R G (le_rfl : U ≤ U) = RingHom.id _
theorem

completedGroupAlgebraTransition_comp

L156 ↗
CompletedGroupAlgebra.completedGroupAlgebraTransition_comp
Documentation

Transition maps compose along refinements of finite quotients.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraTransition_comp
    {U V W : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤ W) :
    (completedGroupAlgebraTransition R G hUV).comp
        (completedGroupAlgebraTransition R G hVW) =
      completedGroupAlgebraTransition R G (hUV.trans hVW)
theorem

completedGroupAlgebraStageCoeffMap_compatible

L181 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMap_compatible
Documentation

Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraStageCoeffMap_compatible
    (S : Type w) [CommRing S] (f : R →+* S)
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U).comp
        (completedGroupAlgebraTransition R G hUV) =
      (completedGroupAlgebraTransition S G hUV).comp
        (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V)
theorem

completedGroupAlgebraStageCoeffMap_transition_comp

L199 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMap_transition_comp
Documentation

Two coefficient changes and two group-quotient transitions compose as the combined change and combined transition.

Source context 10 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
Lean source · statement
theorem completedGroupAlgebraStageCoeffMap_transition_comp
    (S : Type w) (T : Type*) [CommRing S] [CommRing T]
    (f : R →+* S) (g : S →+* T)
    {U V W : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤ W) :
    ((completedGroupAlgebraStageCoeffMap (R := S) (G := G) T g U).comp
        (completedGroupAlgebraTransition S G hUV)).comp
        ((completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V).comp
          (completedGroupAlgebraTransition R G hVW)) =
      (completedGroupAlgebraStageCoeffMap (R := R) (G := G) T (g.comp f) U).comp
        (completedGroupAlgebraTransition R G (hUV.trans hVW))
def

completedGroupAlgebraSystem

L250 ↗
CompletedGroupAlgebra.completedGroupAlgebraSystem
Documentation

The inverse system \(U\mapsto R[G/U]\) with the finite product topology on each stage.

Source context 11 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
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
variable [TopologicalSpace R] [IsTopologicalRing R]
Lean source · full declaration
def completedGroupAlgebraSystem (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    ProCGroups.InverseSystems.InverseSystem (I := CompletedGroupAlgebraIndex G) where
  X := CompletedGroupAlgebraStage R G
  topologicalSpace := fun U => finiteGroupAlgebraTopology R (CompletedGroupAlgebraQuotient G U)
  map := fun {U V} hUV => completedGroupAlgebraTransition R G hUV
  continuous_map := by
    intro U V hUV
    exact finiteGroupAlgebra_mapDomainRingHom_continuous R
      (CompletedGroupAlgebraQuotient G V) (CompletedGroupAlgebraQuotient G U)
      (OpenNormalSubgroupInClass.map
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe (completedGroupAlgebraTransition_id (R := R) (G := G) U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (completedGroupAlgebraTransition_comp (R := R) (G := G) hUV hVW)) x

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