ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology

11 Theorems | 4 Definitions

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.

imports

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

Imported by

Definition CompletedGroupAlgebra.finiteGroupAlgebraTopology

@[reducible]
noncomputable def finiteGroupAlgebraTopology
    (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
    TopologicalSpace (MonoidAlgebra R G) :=
  TopologicalSpace.induced
    ((MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans
      Finsupp.equivFunOnFinite : MonoidAlgebra R G ≃ (G → R))
    inferInstance

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.

Definition CompletedGroupAlgebra.finiteGroupAlgebraHomeomorph

noncomputable 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) := by
  letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  let e : MonoidAlgebra R G ≃ (G → R) :=
    (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
  have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
    Topology.IsInducing.induced e
  exact e.toHomeomorphOfIsInducing he

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

Definition CompletedGroupAlgebra.finiteGroupAlgebraContinuousLinearEquivPi

noncomputable 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) := by
  letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  let e : MonoidAlgebra R G ≃ (G → R) :=
    (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
  have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
    Topology.IsInducing.induced e
  exact ContinuousLinearEquiv.mk
    ((MonoidAlgebra.coeffLinearEquiv R).trans
      (Finsupp.linearEquivFunOnFinite R R G))
    (by
      change Continuous (e : MonoidAlgebra R G → G → R)
      exact he.continuous)
    (by
      change Continuous ((e.toHomeomorphOfIsInducing he).symm : (G → R) → MonoidAlgebra R G)
      exact (e.toHomeomorphOfIsInducing he).symm.continuous)

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

Theorem CompletedGroupAlgebra.finiteGroupAlgebraContinuousLinearEquivPi_apply

@[simp]
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

The continuous equivalence is evaluated by the corresponding comparison formula.

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_coordinate_continuous

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

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_continuousAdd

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_continuousNeg

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_continuousMul

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)

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\).

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_continuousSMul

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_isTopologicalRing

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_compactSpace

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_t2Space

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_totallyDisconnectedSpace

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)

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

Show Lean proof

Definition CompletedGroupAlgebra.finiteGroupAlgebraLift

noncomputable 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 := by
  classical
  letI : Fintype G := Fintype.ofFinite G
  letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  exact
    { toLinearMap :=
        (finiteGroupAlgebraPiLift R G N f).toLinearMap.comp
          ((MonoidAlgebra.coeffLinearEquiv R).trans
            (Finsupp.linearEquivFunOnFinite R R G)).toLinearMap
      cont :=
        by
          have hcont :
              Continuous
                (((MonoidAlgebra.coeffLinearEquiv R).trans
                  (Finsupp.linearEquivFunOnFinite R R G)) :
                  MonoidAlgebra R G → G → R) := by
            let e := finiteGroupAlgebraHomeomorph R G
            change Continuous ((e : MonoidAlgebra R G ≃ₜ (G → R)) :
              MonoidAlgebra R G → G → R)
            exact e.continuous
          exact (finiteGroupAlgebraPiLift R G N f).continuous.comp hcont }

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

Theorem CompletedGroupAlgebra.finiteGroupAlgebraLift_apply_of

@[simp]
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

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

Show Lean proof

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology

Declarations