Module

Topology.lean

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology

20 declarations indexed from sourceView source ↗

Module documentation

Topology and universal maps for finite group algebras

A finite group algebra over a profinite coefficient ring is identified with a finite product of coefficients and given its profinite ring topology. This file proves continuity of its operations and constructs continuous linear lifts from basis data.

Imports2

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
Mathlib.GroupTheory.FiniteAbelian.Basic

Imported by2

def

finiteGroupAlgebraTopology

L31 ↗

CompletedGroupAlgebra.finiteGroupAlgebraTopology

Documentation

The product topology on the group algebra of a finite group, transported through \(R[G] = G \to_0 R \simeq G \to R\). This is the finite stage used in the construction of the completed group algebra.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · statement

def finiteGroupAlgebraTopology
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
    TopologicalSpace (MonoidAlgebra R G)

def

finiteGroupAlgebraHomeomorphCore

L39 ↗

CompletedGroupAlgebra.finiteGroupAlgebraHomeomorphCore

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · statement

def finiteGroupAlgebraHomeomorphCore
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [topology : TopologicalSpace (MonoidAlgebra R G)]
    (htopology : topology = finiteGroupAlgebraTopology R G) :
    MonoidAlgebra R G ≃ₜ (G → R)

def

finiteGroupAlgebraContinuousLinearEquivPiCore

L50 ↗

CompletedGroupAlgebra.finiteGroupAlgebraContinuousLinearEquivPiCore

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · statement

def finiteGroupAlgebraContinuousLinearEquivPiCore
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [topology : TopologicalSpace (MonoidAlgebra R G)]
    (htopology : topology = finiteGroupAlgebraTopology R G) :
    MonoidAlgebra R G ≃L[R] (G → R)

def

finiteGroupAlgebraHomeomorph

L65 ↗

CompletedGroupAlgebra.finiteGroupAlgebraHomeomorph

Documentation

The finite group algebra with its transported product topology is homeomorphic to the function space \(G \to R\).

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

def finiteGroupAlgebraHomeomorph
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    MonoidAlgebra R G ≃ₜ (G → R) :=
  finiteGroupAlgebraHomeomorphCore R G
    (topology := finiteGroupAlgebraTopology R G) rfl

def

finiteGroupAlgebraContinuousLinearEquivPi

L76 ↗

CompletedGroupAlgebra.finiteGroupAlgebraContinuousLinearEquivPi

Documentation

The finite-stage group algebra is the finite product of copies of the coefficient ring as a topological \(R\)-module.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

def finiteGroupAlgebraContinuousLinearEquivPi
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    MonoidAlgebra R G ≃L[R] (G → R) :=
  finiteGroupAlgebraContinuousLinearEquivPiCore R G
    (topology := finiteGroupAlgebraTopology R G) rfl

theorem

finiteGroupAlgebraContinuousLinearEquivPi_apply

L85 ↗

CompletedGroupAlgebra.finiteGroupAlgebraContinuousLinearEquivPi_apply

Documentation

The continuous equivalence is evaluated by the corresponding comparison formula.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebraContinuousLinearEquivPi_apply
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    (x : MonoidAlgebra R G) :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    finiteGroupAlgebraContinuousLinearEquivPi R G x =
      Finsupp.equivFunOnFinite x.coeff :=
  rfl

theorem

finiteGroupAlgebra_coordinate_continuous

L97 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_coordinate_continuous

Documentation

Coordinate evaluation on a finite group algebra is continuous for the transported product topology.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_coordinate_continuous
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    ∀ g : G, Continuous fun x : MonoidAlgebra R G => x.coeff g := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  intro g
  exact (continuous_apply g).comp (finiteGroupAlgebraHomeomorph R G).continuous

theorem

finiteGroupAlgebra_continuousAdd

L106 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_continuousAdd

Documentation

Addition is continuous for the finite-stage group algebra topology.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_continuousAdd
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [IsTopologicalRing R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    ContinuousAdd (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact continuousAdd_induced
    ((MonoidAlgebra.coeffLinearEquiv R).trans
      (Finsupp.linearEquivFunOnFinite R R G))

theorem

finiteGroupAlgebra_continuousNeg

L117 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_continuousNeg

Documentation

Negation is continuous for the finite-stage group algebra topology.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_continuousNeg
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [IsTopologicalRing R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    ContinuousNeg (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  let e : MonoidAlgebra R G ≃ₗ[R] (G → R) :=
    (MonoidAlgebra.coeffLinearEquiv R).trans (Finsupp.linearEquivFunOnFinite R R G)
  exact (finiteGroupAlgebraHomeomorph R G).isInducing.continuousNeg
    (fun x => map_neg e x)

theorem

finiteGroupAlgebra_continuousMul

L132 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_continuousMul

Documentation

Multiplication is continuous for the finite-stage group algebra topology. The coordinate formula is the finite convolution sum over pairs (g1,g2) with \(g1*g2 = g\).

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_continuousMul
    (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
    [IsTopologicalRing R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    ContinuousMul (MonoidAlgebra R G) := by
  classical
  let : Fintype G := Fintype.ofFinite G
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  have hcoord := finiteGroupAlgebra_coordinate_continuous R G
  refine ⟨?_⟩
  apply (finiteGroupAlgebraHomeomorph R G).isInducing.continuous_iff.mpr
  apply continuous_pi
  intro g
  exact (continuous_finsetSum
    (Finset.univ.filter (fun q : G × G => q.1 * q.2 = g))
    (fun q _hq =>
      ((hcoord q.1).comp continuous_fst).mul ((hcoord q.2).comp continuous_snd))).congr
    (fun p => (MonoidAlgebra.coeff_mul_antidiag p.1 p.2 g
      (Finset.univ.filter (fun q : G × G => q.1 * q.2 = g))
      (by intro q; simp only [Finset.mem_filter, Finset.mem_univ, true_and])).symm)

theorem

finiteGroupAlgebra_continuousSMul

L157 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_continuousSMul

Documentation

Scalar multiplication by the coefficient ring is continuous on the finite-stage group algebra topology.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_continuousSMul
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [IsTopologicalRing R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    ContinuousSMul R (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact continuousSMul_induced
    ((MonoidAlgebra.coeffLinearEquiv R).trans
      (Finsupp.linearEquivFunOnFinite R R G))

theorem

finiteGroupAlgebra_isTopologicalRing

L168 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_isTopologicalRing

Documentation

The finite-stage group algebra topology makes \(R[G]\) a topological ring.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_isTopologicalRing
    (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
    [IsTopologicalRing R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    IsTopologicalRing (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact
    { toIsTopologicalSemiring :=
        { toContinuousAdd := finiteGroupAlgebra_continuousAdd R G
          toContinuousMul := finiteGroupAlgebra_continuousMul R G }
      toContinuousNeg := finiteGroupAlgebra_continuousNeg R G }

theorem

finiteGroupAlgebra_compactSpace

L181 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_compactSpace

Documentation

Compactness of the coefficient ring passes to a finite-stage group algebra.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_compactSpace
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [CompactSpace R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    CompactSpace (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact Homeomorph.compactSpace (finiteGroupAlgebraHomeomorph R G).symm

theorem

finiteGroupAlgebra_t2Space

L190 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_t2Space

Documentation

The Hausdorff property of the coefficient ring passes to a finite-stage group algebra.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_t2Space
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [T2Space R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    T2Space (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact Homeomorph.t2Space (finiteGroupAlgebraHomeomorph R G).symm

theorem

finiteGroupAlgebra_totallyDisconnectedSpace

L199 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_totallyDisconnectedSpace

Documentation

Total disconnectedness of the coefficient ring passes to a finite-stage group algebra.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebra_totallyDisconnectedSpace
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
    [TotallyDisconnectedSpace R] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    TotallyDisconnectedSpace (MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact Homeomorph.totallyDisconnectedSpace (finiteGroupAlgebraHomeomorph R G).symm

def

finiteGroupAlgebraPiLift

L211 ↗

CompletedGroupAlgebra.finiteGroupAlgebraPiLift

Documentation

The finite function-space lift sends a coefficient function to the finite sum of its coefficients acting on the prescribed values.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

def finiteGroupAlgebraPiLift
    (R : Type u) (G : Type v) (N : Type w)
    [Ring R] [TopologicalSpace R] [Fintype G]
    [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousSMul R N]
    (f : G -> N) : (G -> R) →L[R] N where
  toLinearMap :=
    { toFun := fun m => ∑ x : G, m x • f x
      map_add' := by
        intro m n
        simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
      map_smul' := by
        intro lam m
        simp only [Pi.smul_apply, smul_eq_mul, mul_smul, RingHom.id_apply, Finset.smul_sum]}
  cont := by
    apply continuous_finsetSum
    intro x _hx
    exact (continuous_apply x).smul continuous_const

theorem

finiteGroupAlgebraPiLift_apply_basis

L233 ↗

CompletedGroupAlgebra.finiteGroupAlgebraPiLift_apply_basis

Documentation

The finite function-space lift sends the basis function \(\mathrm{Pi.single}\ g\ 1\) to \(f(g)\).

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · statement

theorem finiteGroupAlgebraPiLift_apply_basis
    (R : Type u) (G : Type v) (N : Type w)
    [Ring R] [TopologicalSpace R] [Fintype G] [DecidableEq G]
    [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousSMul R N]
    (f : G -> N) (g : G) :
    finiteGroupAlgebraPiLift R G N f (Pi.single g (1 : R)) = f g

def

finiteGroupAlgebraLiftCore

L243 ↗

CompletedGroupAlgebra.finiteGroupAlgebraLiftCore

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · statement

def finiteGroupAlgebraLiftCore
    (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Finite G]
    [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N]
    [topology : TopologicalSpace (MonoidAlgebra R G)]
    (htopology : topology = finiteGroupAlgebraTopology R G) (f : G → N) :
    MonoidAlgebra R G →L[R] N

def

finiteGroupAlgebraLift

L259 ↗

CompletedGroupAlgebra.finiteGroupAlgebraLift

Documentation

A continuous linear map out of a finite group algebra is determined by its values on group elements.

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

def finiteGroupAlgebraLift
    (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Finite G]
    [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N] (f : G → N) :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    MonoidAlgebra R G →L[R] N :=
  finiteGroupAlgebraLiftCore R G N
    (topology := finiteGroupAlgebraTopology R G) rfl f

theorem

finiteGroupAlgebraLift_apply_of

L270 ↗

CompletedGroupAlgebra.finiteGroupAlgebraLift_apply_of

Documentation

The finite group-algebra lift sends the group-like basis vector at \(g\) to \(f(g)\).

Source context 4 commands

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

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w

Lean source · full declaration

theorem finiteGroupAlgebraLift_apply_of
    (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Group G] [Finite G]
    [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N] (f : G → N) (g : G) :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    finiteGroupAlgebraLift R G N f (MonoidAlgebra.of R G g) = f g := by
  classical
  let : Fintype G := Fintype.ofFinite G
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  rw [show MonoidAlgebra.of R G g =
    (MonoidAlgebra.single g 1 : MonoidAlgebra R G) by rfl]
  unfold finiteGroupAlgebraLift finiteGroupAlgebraLiftCore
  change
    finiteGroupAlgebraPiLift R G N f
        (finiteGroupAlgebraContinuousLinearEquivPi R G
          (MonoidAlgebra.single g 1)) =
      f g
  rw [finiteGroupAlgebraContinuousLinearEquivPi_apply]
  rw [MonoidAlgebra.coeff_single]
  rw [Finsupp.equivFunOnFinite_single]
  exact finiteGroupAlgebraPiLift_apply_basis R G N f g

Module documentation

Topology and universal maps for finite group algebras

Declarations