NYLL
Module

CanonicalMap.lean

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
9 declarations indexed from sourceView source ↗

Module documentation

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

This module lifts the compatible open-finite quotient maps from the abstract group algebra to the named two-parameter completion, and proves its projection, continuity, and density properties.

Imports1
Imported by2

Declarations

theorem

groupAlgebraOpenFiniteQuotientMap_surjective

L33 ↗
CompletedGroupAlgebra.groupAlgebraOpenFiniteQuotientMap_surjective
Documentation

The abstract group-algebra map onto an open-finite quotient stage is surjective.

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
theorem groupAlgebraOpenFiniteQuotientMap_surjective
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Function.Surjective (groupAlgebraOpenFiniteQuotientMap R G K)
theorem

groupAlgebraOpenFiniteQuotientMap_compatibleMaps

L42 ↗
CompletedGroupAlgebra.groupAlgebraOpenFiniteQuotientMap_compatibleMaps
Documentation

The abstract group-algebra maps to open-finite quotient stages are compatible.

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 · full declaration
theorem groupAlgebraOpenFiniteQuotientMap_compatibleMaps
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    (completedGroupAlgebraOpenFiniteQuotientSystem R G).CompatibleMaps
      (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
        groupAlgebraOpenFiniteQuotientMap R G K) := by
  intro K L hKL
  funext x
  exact congrFun
    (congrArg DFunLike.coe
      (completedGroupAlgebraOpenFiniteQuotientTransition_comp_map R G hKL))
    x
def

toCompletedGroupAlgebraOpenFiniteQuotientLimit

L59 ↗
CompletedGroupAlgebra.toCompletedGroupAlgebraOpenFiniteQuotientLimit
Documentation

The two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\) appearing in Ribes--Zalesskii Section 5.3.

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
def toCompletedGroupAlgebraOpenFiniteQuotientLimit
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (x : MonoidAlgebra R G) :
    CompletedGroupAlgebraOpenFiniteQuotientLimit R G
theorem

completedGroupAlgebraOpenFiniteQuotientLimitProjection_toLimit

L74 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_toLimit
Documentation

Projecting the canonical map to the open-finite quotient limit recovers the stage quotient map.

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
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_toLimit
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : MonoidAlgebra R G) :
    completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
        (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x) =
      groupAlgebraOpenFiniteQuotientMap R G K x
def

toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom

L84 ↗
CompletedGroupAlgebra.toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom
Documentation

The canonical map from \(R[G]\) to the two-parameter limit is bundled as a ring homomorphism.

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 · full declaration
def toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
  toFun := toCompletedGroupAlgebraOpenFiniteQuotientLimit R G
  map_zero' := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
  map_one' := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_one (groupAlgebraOpenFiniteQuotientMap R G K)
  map_add' x y := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_add (groupAlgebraOpenFiniteQuotientMap R G K) x y
  map_mul' x y := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_mul (groupAlgebraOpenFiniteQuotientMap R G K) x y
theorem

toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply

L111 ↗
CompletedGroupAlgebra.toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply
Documentation

The bundled ring homomorphism has the same underlying function as the coordinatewise construction.

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
theorem toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x =
      toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x
theorem

completedGroupAlgebraOpenFiniteQuotientLimitProjection_comp_toLimit

L120 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_comp_toLimit
Documentation

Projection after the canonical ring homomorphism is the corresponding open-finite quotient map.

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
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_comp_toLimit
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K).comp
        (toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G) =
      groupAlgebraOpenFiniteQuotientMap R G K
theorem

continuous_toCompletedGroupAlgebraOpenFiniteQuotientLimit_kernelTopology

L130 ↗
CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraOpenFiniteQuotientLimit_kernelTopology
Documentation

The canonical map to the open-finite quotient limit is continuous for the kernel topology.

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 · full declaration
theorem continuous_toCompletedGroupAlgebraOpenFiniteQuotientLimit_kernelTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    Continuous (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
  let : ∀ K, TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K
  let π : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
      MonoidAlgebra R G → CompletedGroupAlgebraOpenQuotientStage R G K :=
    fun K => groupAlgebraOpenFiniteQuotientMap R G K
  have hπ : ∀ K, Continuous (π K) := by
    intro K
    exact continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology R G K
  have hcompat : S.CompatibleMaps π :=
    groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G
  change Continuous (S.inverseLimitLift π hcompat)
  exact S.continuous_inverseLimitLift π hπ hcompat
theorem

denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit

L156 ↗
CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit
Documentation

The canonical map from R[G] has dense range in the two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\).

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
theorem denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    DenseRange (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.