Module

Topology.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.InClass.Topology

10 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / Within a Class / Topology

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

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.InClass.Projection

Imported by2

instance

(anonymous instance)

L31 ↗

Source context 9 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U)

instance

(anonymous instance)

L38 ↗

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U)

theorem

completedGroupAlgebraStageInClass_isTopologicalRing

L46 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageInClass_isTopologicalRing

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · full declaration

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) := by
  let : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
    finite_completedGroupAlgebraQuotientInClass G C U
  let : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
    (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
  dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
  exact finiteGroupAlgebra_isTopologicalRing R (CompletedGroupAlgebraQuotientInClass G C U)

instance

instIsTopologicalRingCompletedGroupAlgebraSystemInClassX

L65 ↗

CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraSystemInClassX

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

instance instIsTopologicalRingCompletedGroupAlgebraSystemInClassX
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    IsTopologicalRing ((completedGroupAlgebraSystemInClass C R G).X U)

instance

instIsTopologicalRingCompletedGroupAlgebraInClass

L75 ↗

CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraInClass

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

instance instIsTopologicalRingCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    IsTopologicalRing (CompletedGroupAlgebraInClass C R G)

instance

instContinuousSMulCompletedGroupAlgebraInClass

L82 ↗

CompletedGroupAlgebra.instContinuousSMulCompletedGroupAlgebraInClass

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

instance instContinuousSMulCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    ContinuousSMul R (CompletedGroupAlgebraInClass C R G)

theorem

continuous_completedGroupAlgebraAlgebraMapInClass

L111 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraAlgebraMapInClass

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

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

theorem

completedGroupAlgebraInClass_compactSpace

L135 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClass_compactSpace

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

theorem completedGroupAlgebraInClass_compactSpace
    (C : ProCGroups.FiniteGroupClass.{v})
    [CompactSpace R] [T2Space R] :
    CompactSpace (CompletedGroupAlgebraInClass C R G)

theorem

completedGroupAlgebraInClass_t2Space

L158 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClass_t2Space

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

theorem completedGroupAlgebraInClass_t2Space
    (C : ProCGroups.FiniteGroupClass.{v})
    [T2Space R] :
    T2Space (CompletedGroupAlgebraInClass C R G)

theorem

completedGroupAlgebraInClass_totallyDisconnectedSpace

L176 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClass_totallyDisconnectedSpace

Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance

Lean source · statement

theorem completedGroupAlgebraInClass_totallyDisconnectedSpace
    (C : ProCGroups.FiniteGroupClass.{v})
    [TotallyDisconnectedSpace R] :
    TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C R G)

Module documentation

Completed Group Algebra / Basic / Within a Class / Topology

Declarations