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

ProCGroups.CompletedGroupAlgebra.Basic.InClass.Topology

5 Theorems | 3 Instances

This module transports finite-stage topological structures through the named \(C\)-indexed inverse-limit carrier and records its compactness and separation properties.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageInClass_isTopologicalRing 
theorem completedGroupAlgebraStageInClass_isTopologicalRing
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
      finite_completedGroupAlgebraQuotientInClass G C U
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
      (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
    IsTopologicalRing (CompletedGroupAlgebraStageInClass C R G U)

Each \(C\)-indexed finite stage is a topological ring.

Show Lean proof
Instance CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraSystemInClassX 
instance instIsTopologicalRingCompletedGroupAlgebraSystemInClassX
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    IsTopologicalRing ((completedGroupAlgebraSystemInClass C R G).X U) :=
  completedGroupAlgebraStageInClass_isTopologicalRing (R := R) (G := G) C U

The inverse system of finite-stage group algebras inherits a ring structure from the compatible finite-stage rings.

Instance CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraInClass 
instance instIsTopologicalRingCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    IsTopologicalRing (CompletedGroupAlgebraInClass C R G) := by
  change IsTopologicalRing (completedGroupAlgebraSystemInClass C R G).inverseLimit
  infer_instance

The \(C\)-indexed completed group algebra inherits a ring structure from the compatible finite-stage rings.

Instance CompletedGroupAlgebra.instContinuousSMulCompletedGroupAlgebraInClass 
instance instContinuousSMulCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    ContinuousSMul R (CompletedGroupAlgebraInClass C R G) := by
  letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      ContinuousSMul R ((completedGroupAlgebraSystemInClass C R G).X U) :=
    fun U => by
      letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
        finite_completedGroupAlgebraQuotientInClass G C U
      dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
      exact finiteGroupAlgebra_continuousSMul R
        (CompletedGroupAlgebraQuotientInClass G C U)
  exact inferInstanceAs
    (ContinuousSMul R (completedGroupAlgebraSystemInClass C R G).inverseLimit)

Scalar multiplication is continuous for the relevant inverse-limit topology.

Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraAlgebraMapInClass 
theorem continuous_completedGroupAlgebraAlgebraMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Continuous (algebraMap R (CompletedGroupAlgebraInClass C R G))

The coefficient-ring map into the \(C\)-indexed completed group algebra is continuous.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraInClass_compactSpace 
theorem completedGroupAlgebraInClass_compactSpace
    (C : ProCGroups.FiniteGroupClass.{v})
    [CompactSpace R] [T2Space R] :
    CompactSpace (CompletedGroupAlgebraInClass C R G)

The \(C\)-indexed completed group algebra is compact for compact Hausdorff coefficients.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraInClass_t2Space 
theorem completedGroupAlgebraInClass_t2Space
    (C : ProCGroups.FiniteGroupClass.{v})
    [T2Space R] :
    T2Space (CompletedGroupAlgebraInClass C R G)

The \(C\)-indexed completed group algebra is Hausdorff for Hausdorff coefficients.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraInClass_totallyDisconnectedSpace 
theorem completedGroupAlgebraInClass_totallyDisconnectedSpace
    (C : ProCGroups.FiniteGroupClass.{v})
    [TotallyDisconnectedSpace R] :
    TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C R G)

The \(C\)-indexed completed group algebra is totally disconnected for totally disconnected coefficients.

Show Lean proof