Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Topology
ProCGroups/CompletedGroupAlgebra/Basic/AllFinite/Topology

ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Topology

4 Theorems | 3 Instances

This module transports the finite-stage topological ring and scalar-action structures through the single all-finite inverse limit, and records its compactness and separation properties.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.completedGroupAlgebraStage_isTopologicalRing 
theorem completedGroupAlgebraStage_isTopologicalRing (U : CompletedGroupAlgebraIndex G) :
    IsTopologicalRing ((completedGroupAlgebraSystem R G).X U)

Each finite stage \(R[G/U]\) is a topological ring for its product topology.

Show Lean proof
Instance CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraSystemX 
instance instIsTopologicalRingCompletedGroupAlgebraSystemX
    (U : CompletedGroupAlgebraIndex G) :
    IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) :=
  completedGroupAlgebraStage_isTopologicalRing (R := R) (G := G) U

Each stage of the all-finite system has its finite product topological-ring structure.

Instance CompletedGroupAlgebra.instContinuousSMulCompletedGroupAlgebra 
instance instContinuousSMulCompletedGroupAlgebra :
    ContinuousSMul R (CompletedGroupAlgebraCarrier R G) := by
  letI : ∀ U : CompletedGroupAlgebraIndex G,
      ContinuousSMul R ((completedGroupAlgebraSystem R G).X U) := fun U => by
    dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
    exact finiteGroupAlgebra_continuousSMul R (CompletedGroupAlgebraQuotient G U)
  exact inferInstanceAs
    (ContinuousSMul R (completedGroupAlgebraSystem R G).inverseLimit)

Scalar multiplication is continuous because it is continuous at every finite stage.

Instance CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebra 
instance instIsTopologicalRingCompletedGroupAlgebra :
    IsTopologicalRing (CompletedGroupAlgebraCarrier R G) := by
  exact inferInstanceAs
    (IsTopologicalRing (completedGroupAlgebraSystem R G).inverseLimit)

The completed group algebra inherits its topological-ring structure from the generic ring-valued inverse limit.

Theorem CompletedGroupAlgebra.completedGroupAlgebra_compactSpace 
theorem completedGroupAlgebra_compactSpace [CompactSpace R] [T2Space R] :
    CompactSpace (CompletedGroupAlgebraCarrier R G)

The completed group algebra is compact for compact Hausdorff coefficients.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebra_t2Space 
theorem completedGroupAlgebra_t2Space [T2Space R] :
    T2Space (CompletedGroupAlgebraCarrier R G)

The completed group algebra is Hausdorff for Hausdorff coefficients.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebra_totallyDisconnectedSpace 
theorem completedGroupAlgebra_totallyDisconnectedSpace [TotallyDisconnectedSpace R] :
    TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier R G)

The completed group algebra is totally disconnected for totally disconnected coefficients.

Show Lean proof