Module

Topology.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Topology

9 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / All Finite / Topology

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.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Projections

Imported by2

instance

(anonymous instance)

L32 ↗

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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U)

instance

(anonymous instance)

L37 ↗

Source context 11 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U)

theorem

completedGroupAlgebraStage_isTopologicalRing

L43 ↗

CompletedGroupAlgebra.completedGroupAlgebraStage_isTopologicalRing

Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

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

instance

instIsTopologicalRingCompletedGroupAlgebraSystemX

L49 ↗

CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraSystemX

Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

instance instIsTopologicalRingCompletedGroupAlgebraSystemX
    (U : CompletedGroupAlgebraIndex G) :
    IsTopologicalRing ((completedGroupAlgebraSystem R G).X U)

instance

instContinuousSMulCompletedGroupAlgebra

L55 ↗

CompletedGroupAlgebra.instContinuousSMulCompletedGroupAlgebra

Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

instance instContinuousSMulCompletedGroupAlgebra :
    ContinuousSMul R (CompletedGroupAlgebraCarrier R G)

instance

instIsTopologicalRingCompletedGroupAlgebra

L76 ↗

CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebra

Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

instance instIsTopologicalRingCompletedGroupAlgebra :
    IsTopologicalRing (CompletedGroupAlgebraCarrier R G)

theorem

completedGroupAlgebra_compactSpace

L82 ↗

CompletedGroupAlgebra.completedGroupAlgebra_compactSpace

Documentation

The completed group algebra is compact for compact Hausdorff coefficients.

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

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

theorem

completedGroupAlgebra_t2Space

L98 ↗

CompletedGroupAlgebra.completedGroupAlgebra_t2Space

Documentation

The completed group algebra is Hausdorff for Hausdorff coefficients.

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

theorem completedGroupAlgebra_t2Space [T2Space R] :
    T2Space (CompletedGroupAlgebraCarrier R G)

theorem

completedGroupAlgebra_totallyDisconnectedSpace

L108 ↗

CompletedGroupAlgebra.completedGroupAlgebra_totallyDisconnectedSpace

Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance

Lean source · statement

theorem completedGroupAlgebra_totallyDisconnectedSpace [TotallyDisconnectedSpace R] :
    TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier R G)

Module documentation

Completed Group Algebra / Basic / All Finite / Topology

Declarations