Module

Comparison.lean

Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison

8 declarations indexed from sourceView source ↗

Module documentation

Comparison maps for in-class completions

This file computes the canonical maps between all-finite and in-class completed group algebras on group-like elements and their differences from one. It also records the corresponding formulas for functorial maps and restricted scalar actions.

Imports2

Imported by3

theorem

completedGroupAlgebraToInClass_of

L39 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_of

Documentation

The all-finite completed group algebra comparison sends group-like elements to the \(C\)-indexed group-like elements.

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
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 completedGroupAlgebraToInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (g : G) :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
        (completedGroupAlgebraOf R G g) =
      completedGroupAlgebraOfInClass C R G g

theorem

completedGroupAlgebraToInClass_of_sub_one

L59 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_of_sub_one

Documentation

The comparison map to a class-indexed completion sends all-finite augmentation generators to class-indexed generators.

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
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 completedGroupAlgebraToInClass_of_sub_one
    (C : ProCGroups.FiniteGroupClass.{v})
    (g : G) :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
        (completedGroupAlgebraOf R G g - 1) =
      completedGroupAlgebraOfInClass C R G g - 1

theorem

completedGroupAlgebraToInClass_restrictScalars_sub_one_smul

L72 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_restrictScalars_sub_one_smul

Documentation

After restricting scalars along \(\widehat{R[G]} \to \widehat{R[G]}_C\), the all-finite augmentation generator acts as the matching \(C\)-indexed generator.

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
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 completedGroupAlgebraToInClass_restrictScalars_sub_one_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraInClass C R G) A]
    (g : G) (a : A) :
    letI : Module (CompletedGroupAlgebraCarrier R G) A :=
      Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
    (completedGroupAlgebraOf R G g - 1) • a =
      (completedGroupAlgebraOfInClass C R G g - 1) • a := by
  exact congrArg (fun z : CompletedGroupAlgebraInClass C R G => z • a)
    (completedGroupAlgebraToInClass_of_sub_one (R := R) (G := G) C g)

theorem

completedGroupAlgebraFromInClass_of

L88 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass_of

Documentation

The comparison map from a class-indexed completion sends class-indexed group-like elements to all-finite group-like elements.

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
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 completedGroupAlgebraFromInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (g : G) :
    completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
        (completedGroupAlgebraOfInClass C R G g) =
      completedGroupAlgebraOf R G g

theorem

completedGroupAlgebraFromInClass_of_sub_one

L108 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass_of_sub_one

Documentation

The comparison map from a class-indexed completion sends class-indexed augmentation generators to all-finite generators.

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
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 completedGroupAlgebraFromInClass_of_sub_one
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (g : G) :
    completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
        (completedGroupAlgebraOfInClass C R G g - 1) =
      completedGroupAlgebraOf R G g - 1

theorem

completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul

L128 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul

Documentation

After restricting scalars along \(\widehat{R[G]}_C \to \widehat{R[G]}\), the \(C\)-indexed augmentation generator acts as the matching all-finite generator.

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
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 completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
    (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraCarrier R G) A]
    (g : G) (a : A) :
    letI : Module (CompletedGroupAlgebraInClass C R G) A :=
      Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
    (completedGroupAlgebraOfInClass C R G g - 1) • a =
      (completedGroupAlgebraOf R G g - 1) • a := by
  exact congrArg (fun z : CompletedGroupAlgebraCarrier R G => z • a)
    (completedGroupAlgebraFromInClass_of_sub_one (R := R) (G := G) C hForm hG g)

theorem

completedGroupAlgebraMapInClass_of

L145 ↗

CompletedGroupAlgebra.completedGroupAlgebraMapInClass_of

Documentation

The class-indexed completed group-algebra map sends the completed group-like element of \(g\) to the completed group-like element of its image.

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
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 completedGroupAlgebraMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (completedGroupAlgebraOfInClass C R G g) =
      completedGroupAlgebraOfInClass C R H (φ g)

theorem

completedGroupAlgebraMapInClass_of_sub_one

L158 ↗

CompletedGroupAlgebra.completedGroupAlgebraMapInClass_of_sub_one

Documentation

The class-indexed functorial map sends group-like augmentation generators to their images.

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
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 completedGroupAlgebraMapInClass_of_sub_one
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (completedGroupAlgebraOfInClass C R G g - 1) =
      completedGroupAlgebraOfInClass C R H (φ g) - 1

Module documentation

Comparison maps for in-class completions

Declarations