Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
ProCGroups/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/CanonicalMap

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap

7 Theorems | 2 Definitions

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.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.groupAlgebraOpenFiniteQuotientMap_surjective 
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)

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

Show Lean proof
Theorem CompletedGroupAlgebra.groupAlgebraOpenFiniteQuotientMap_compatibleMaps 
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)

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

Show Lean proof
Definition CompletedGroupAlgebra.toCompletedGroupAlgebraOpenFiniteQuotientLimit 
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 :=
  (completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv
    (R := R) (G := G)).symm
    ((completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimitLift
      (fun K => groupAlgebraOpenFiniteQuotientMap R G K)
      (groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G) x)

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

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_toLimit 
@[simp]
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

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

Show Lean proof
Definition CompletedGroupAlgebra.toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom 
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

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

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply 
@[simp]
theorem toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x =
      toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x

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

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_comp_toLimit 
@[simp]
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_comp_toLimit
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K).comp
        (toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G) =
      groupAlgebraOpenFiniteQuotientMap R G K

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

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraOpenFiniteQuotientLimit_kernelTopology 
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)

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

Show Lean proof
Theorem CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit 
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)

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

Show Lean proof