NYLL
Module

GroupLike.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
8 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / All Finite Functoriality / Group-Like

This module records the action of the all-finite functorial map on canonical group-like elements.

Imports1
Imported by3

Declarations

def

completedGroupAlgebraOf

L33 ↗
CompletedGroupAlgebra.completedGroupAlgebraOf
Documentation

A group element maps to its image in the completed group algebra.

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraOf (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (g : G) : CompletedGroupAlgebraCarrier R G
theorem

completedGroupAlgebraProjection_of

L40 ↗
CompletedGroupAlgebra.completedGroupAlgebraProjection_of
Documentation

Projection of a completed group-like element to a finite quotient 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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraProjection_of
    (U : CompletedGroupAlgebraIndex G) (g : G) :
    completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1
theorem

completedGroupAlgebraOf_one

L50 ↗
CompletedGroupAlgebra.completedGroupAlgebraOf_one
Documentation

The completed group-like element attached to \(1\) is the unit.

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraOf_one :
    completedGroupAlgebraOf R G 1 = (1 : CompletedGroupAlgebraCarrier R G)
theorem

completedGroupAlgebraOf_mul

L62 ↗
CompletedGroupAlgebra.completedGroupAlgebraOf_mul
Documentation

Completed group-like elements multiply according to the group law.

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraOf_mul (g h : G) :
    completedGroupAlgebraOf R G (g * h) =
      completedGroupAlgebraOf R G g * completedGroupAlgebraOf R G h
theorem

continuous_completedGroupAlgebraStageMap_of

L77 ↗
CompletedGroupAlgebra.continuous_completedGroupAlgebraStageMap_of
Documentation

The finite-stage group-like map \(G\to R[G/U]\) is continuous.

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · full declaration
theorem continuous_completedGroupAlgebraStageMap_of
    (U : CompletedGroupAlgebraIndex G) :
    letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
      (completedGroupAlgebraSystem R G).topologicalSpace U
    Continuous fun g : G =>
      completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) := by
  let : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
    (completedGroupAlgebraSystem R G).topologicalSpace U
  let : DiscreteTopology (CompletedGroupAlgebraQuotient G U) :=
    QuotientGroup.discreteTopology
      (ProCGroups.openNormalSubgroup_isOpen
        (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
  have hbasis :
      @Continuous (CompletedGroupAlgebraQuotient G U)
        (CompletedGroupAlgebraStage R G U) inferInstance
        ((completedGroupAlgebraSystem R G).topologicalSpace U)
        (fun q => MonoidAlgebra.single q (1 : R)) :=
    continuous_of_discreteTopology
  have hproj :
      Continuous fun g : G =>
        openNormalSubgroupInClassProj
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g := by
    change Continuous
      (QuotientGroup.mk'
        (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
    exact continuous_quotient_mk'
  have hcont := hbasis.comp hproj
  change @Continuous G (CompletedGroupAlgebraStage R G U) (‹TopologicalSpace G›)
    ((completedGroupAlgebraSystem R G).topologicalSpace U)
    (fun g => MonoidAlgebra.single
      (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) (1 : R)) at hcont
  convert hcont using 1
  funext g
  exact completedGroupAlgebraStageMap_of (R := R) (G := G) U g
theorem

continuous_completedGroupAlgebraOf

L114 ↗
CompletedGroupAlgebra.continuous_completedGroupAlgebraOf
Documentation

The completed group-like map \(G \to \widehat{R[G]}\) is continuous.

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuous_completedGroupAlgebraOf :
    Continuous (completedGroupAlgebraOf R G)
theorem

completedGroupAlgebraMap_of

L140 ↗
CompletedGroupAlgebra.completedGroupAlgebraMap_of
Documentation

The completed functorial map sends the group-like element attached to \(g\) to that of \(\varphi(g)\).

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraMap_of
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMap (G := G) (H := H) R φ hφ (completedGroupAlgebraOf R G g) =
      completedGroupAlgebraOf R H (φ g)
theorem

completedGroupAlgebraMapAlgHom_of

L154 ↗
CompletedGroupAlgebra.completedGroupAlgebraMapAlgHom_of
Documentation

The algebra-hom completed functorial map sends group-like elements to their images.

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 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraMapAlgHom_of
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ
        (completedGroupAlgebraOf R G g) =
      completedGroupAlgebraOf R H (φ g)

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