Module

Topology.lean

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology

8 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit / Topology

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.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System

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 (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K)

theorem

completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing

L38 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing

Documentation

Each two-parameter finite quotient stage is a topological ring for its discrete 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
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · full declaration

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) := by
  let : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  have : DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
  infer_instance

theorem

completedGroupAlgebraOpenFiniteQuotientStage_fintype

L52 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientStage_fintype

Documentation

Each open-finite quotient stage is finite for compact topological 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
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · statement

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))

instance

instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientSystemX

L71 ↗

CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientSystemX

Documentation

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

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 (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · statement

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

instance

instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit

L80 ↗

CompletedGroupAlgebra.instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit

Documentation

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

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 (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · statement

instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
    IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)

theorem

completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace

L87 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace

Documentation

The open-finite quotient limit is compact for compact topological 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
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · statement

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

theorem

completedGroupAlgebraOpenFiniteQuotientLimit_t2Space

L107 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_t2Space

Documentation

The open-finite quotient limit is Hausdorff.

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 (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · statement

theorem completedGroupAlgebraOpenFiniteQuotientLimit_t2Space :
    T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)

theorem

completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace

L117 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace

Documentation

The open-finite quotient limit is totally disconnected.

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 (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance

Lean source · statement

theorem completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace :
    TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)

Module documentation

Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit / Topology

Declarations