ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology

5 Theorems | 2 Instances

This module transports the discrete topological-ring structures of the open-finite quotient stages through the single two-parameter inverse limit, and records compactness and separation results.

import

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System

Imported by

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing

theorem completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    IsTopologicalRing (CompletedGroupAlgebraOpenQuotientStage R G K)

Each two-parameter finite quotient stage is a topological ring for its discrete topology.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientStage_fintype

theorem completedGroupAlgebraOpenFiniteQuotientStage_fintype
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] [CompactSpace R]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Nonempty (Fintype (CompletedGroupAlgebraOpenQuotientStage R G K))

Each open-finite quotient stage is finite for compact topological coefficients.

Show Lean proof

Instance CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientSystemX

instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientSystemX
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    IsTopologicalRing
      ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
  completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing
    (R := R) (G := G) K

Each open-finite quotient stage has its discrete topological-ring structure.

Instance CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit

instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
    IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
  exact inferInstanceAs
    (IsTopologicalRing
      (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit)

The open-finite quotient limit inherits its topological-ring structure from the generic ring-valued inverse limit.

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace

theorem completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace
    [IsTopologicalRing R] [CompactSpace R] :
    CompactSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)

The open-finite quotient limit is compact for compact topological coefficients.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_t2Space

theorem completedGroupAlgebraOpenFiniteQuotientLimit_t2Space :
    T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)

The open-finite quotient limit is Hausdorff.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace

theorem completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace :
    TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)

The open-finite quotient limit is totally disconnected.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology

Declarations