ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

27 Theorems | 21 Definitions | 2 Structures | 4 Instances

This module compares the named fixed-coefficient completion with the named two-parameter open-finite quotient completion and studies the induced topology, injectivity, density, and coefficient-quotient kernels.

imports

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
Mathlib.Algebra.Ring.TransferInstance
Mathlib.Topology.Homeomorph.TransferInstance

Imported by

Definition CompletedGroupAlgebra.completedGroupAlgebraToOpenFiniteQuotientLimit

def completedGroupAlgebraToOpenFiniteQuotientLimit
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (x : CompletedGroupAlgebraCarrier R G) :
    CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
  (completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv
    (R := R) (G := G)).symm
    ((completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimitLift
      (fun K => completedGroupAlgebraOpenFiniteQuotientProjection R G K)
      (by
        intro K L hKL
        funext x
        exact congrFun
          (congrArg DFunLike.coe
            (completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection
              R G hKL))
          x) x)

The canonical map from the fixed-coefficient completed group algebra \(\widehat{R[G]}\) to the two-parameter limit \(\varprojlim_{I,U} (R/I)[G/U]\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_fromCompleted

@[simp]
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_fromCompleted
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
        (completedGroupAlgebraToOpenFiniteQuotientLimit R G x) =
      completedGroupAlgebraOpenFiniteQuotientProjection R G K x

The open-finite-limit projection after the comparison from the completed group algebra is the original finite-stage projection.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra

@[simp]
theorem completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (x : MonoidAlgebra R G) :
    completedGroupAlgebraToOpenFiniteQuotientLimit R G (toCompletedGroupAlgebra R G x) =
      toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x

The comparison from the completed group algebra to the open-finite quotient limit agrees with the canonical dense map on abstract group-algebra elements.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraToOpenFiniteQuotientLimitRingHom

def completedGroupAlgebraToOpenFiniteQuotientLimitRingHom
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
  toFun := completedGroupAlgebraToOpenFiniteQuotientLimit R G
  map_zero' := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_zero (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
  map_one' := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_one (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
  map_add' x y := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_add (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
  map_mul' x y := by
    apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
    intro K
    exact map_mul (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y

The canonical map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is bundled as a ring homomorphism.

Theorem CompletedGroupAlgebra.openFiniteLimitProjection_comp_fromCompleted

@[simp]
theorem openFiniteLimitProjection_comp_fromCompleted
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K).comp
        (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G) =
      completedGroupAlgebraOpenFiniteQuotientProjection R G K

Projection from the open-finite quotient limit, composed with the comparison from the completion, recovers the corresponding completed projection.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA

@[simp]
theorem completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA :
    (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G).comp
        (toCompletedGroupAlgebraRingHom R G) =
      toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G

Composing the comparison map with the dense map from the abstract group algebra recovers the canonical completed group-algebra map.

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraToOpenFiniteQuotientLimit

theorem continuous_completedGroupAlgebraToOpenFiniteQuotientLimit :
    Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)

The comparison map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is continuous.

Show Lean proof

Theorem CompletedGroupAlgebra.denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit

theorem denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit
    [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    DenseRange (completedGroupAlgebraToOpenFiniteQuotientLimit R G)

The image of the map from the completed group algebra to the open-finite quotient limit is dense in the target completed group-algebra object.

Show Lean proof

Theorem CompletedGroupAlgebra.injective_completedGroupAlgebraToOpenFiniteQuotientLimit

theorem injective_completedGroupAlgebraToOpenFiniteQuotientLimit
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] :
    Function.Injective (completedGroupAlgebraToOpenFiniteQuotientLimit R G)

The comparison map to the two-parameter kernel-neighborhood limit is injective when the coefficient ring is profinite. This is the completed-stage form of the kernel-intersection claim in Lemma 5.3.5(a).

Show Lean proof

Theorem CompletedGroupAlgebra.surjective_completedGroupAlgebraToOpenFiniteQuotientLimit

theorem surjective_completedGroupAlgebraToOpenFiniteQuotientLimit
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    Function.Surjective (completedGroupAlgebraToOpenFiniteQuotientLimit R G)

For profinite coefficients, the comparison map to the Hausdorff two-parameter kernel-neighborhood limit has compact closed dense image and is surjective.

Show Lean proof

Theorem CompletedGroupAlgebra.bijective_completedGroupAlgebraToOpenFiniteQuotientLimit

theorem bijective_completedGroupAlgebraToOpenFiniteQuotientLimit
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    Function.Bijective (completedGroupAlgebraToOpenFiniteQuotientLimit R G)

The comparison map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is a bijection under the profinite coefficient hypothesis.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv

def completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    CompletedGroupAlgebraCarrier R G ≃+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
  RingEquiv.ofBijective (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G)
    (bijective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))

Ribes--Zalesskii Section \(5.3\) comparison: the fixed-coefficient inverse-limit model \(\widehat{R[G]}\) is ring-isomorphic to the two-parameter kernel-neighborhood limit \(\varprojlim_{I,U} (R/I)[G/U]\) for profinite coefficient rings.

Theorem CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv_apply

@[simp]
theorem completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv_apply
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)]
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G) x =
      completedGroupAlgebraToOpenFiniteQuotientLimit R G x

The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph

def completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    CompletedGroupAlgebraCarrier R G ≃ₜ CompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
  letI : CompactSpace (CompletedGroupAlgebraCarrier R G) :=
    completedGroupAlgebra_compactSpace (R := R) (G := G)
  letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
    completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G)
  let e : CompletedGroupAlgebraCarrier R G ≃ CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
    (completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G)).toEquiv
  exact Continuous.homeoOfEquivCompactToT2 (f := e) (by
    change Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)
    exact continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))

The fixed-coefficient completed group algebra is homeomorphic to the two-parameter open finite quotient inverse limit.

Theorem CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebra

theorem denseRange_toCompletedGroupAlgebra :
    DenseRange (toCompletedGroupAlgebra R G)

In Lemma 5.3.5(c), fixed-coefficient inverse-limit form, the abstract group algebra maps dense into the completed group algebra.

Show Lean proof

Theorem CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraRingHom

theorem denseRange_toCompletedGroupAlgebraRingHom :
    DenseRange (toCompletedGroupAlgebraRingHom R G)

The image of the canonical ring homomorphism into the completed group algebra is dense.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalTopology

@[reducible]
def completedGroupAlgebraNaturalTopology (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    TopologicalSpace (MonoidAlgebra R G) :=
  TopologicalSpace.induced (toCompletedGroupAlgebra R G) inferInstance

The completion topology on the abstract group algebra, induced by the canonical map into \(\widehat{R[G]}\); below it is identified with the kernel-neighborhood topology generated by the maps \(R[G] \to (R/I)[G/U]\).

Structure CompletedGroupAlgebra.CompletedGroupAlgebraNaturalSource

@[ext]
structure CompletedGroupAlgebraNaturalSource (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] where
  /-- The group-algebra element carried by the natural-topology wrapper. -/
  toMonoidAlgebra : MonoidAlgebra R G

A genuine copy of the abstract group algebra reserved for the topology induced by the canonical map into [[R G]].

This is deliberately a structure, not a reducible type synonym: the natural and kernel-neighborhood topologies therefore cannot compete as instances on the same type.

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceEquiv

def completedGroupAlgebraNaturalSourceEquiv :
    CompletedGroupAlgebraNaturalSource R G ≃ MonoidAlgebra R G where
  toFun := CompletedGroupAlgebraNaturalSource.toMonoidAlgebra
  invFun := fun x => CompletedGroupAlgebraNaturalSource.mk x
  left_inv x := by cases x; rfl
  right_inv _ := rfl

Forget the natural-topology wrapper.

Instance CompletedGroupAlgebra.instRingCompletedGroupAlgebraNaturalSource

instance instRingCompletedGroupAlgebraNaturalSource :
    Ring (CompletedGroupAlgebraNaturalSource R G) :=
  (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).ring

Transport the group-algebra ring structure to its natural-topology wrapper.

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceRingEquiv

def completedGroupAlgebraNaturalSourceRingEquiv :
    CompletedGroupAlgebraNaturalSource R G ≃+* MonoidAlgebra R G :=
  (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).ringEquiv

Algebraic form of the forgetful equivalence from the natural-topology source.

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceOf

def completedGroupAlgebraNaturalSourceOf :
    MonoidAlgebra R G →+* CompletedGroupAlgebraNaturalSource R G :=
  (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).symm.toRingHom

Insert a raw group-algebra element into the natural-topology source. Keeping this as a bundled ring homomorphism avoids making downstream APIs unpack the topology wrapper.

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceOf_toMonoidAlgebra

@[simp]
theorem completedGroupAlgebraNaturalSourceOf_toMonoidAlgebra (x : MonoidAlgebra R G) :
    (completedGroupAlgebraNaturalSourceOf (R := R) (G := G) x).toMonoidAlgebra = x

Forgetting the natural-topology wrapper after inserting a group-algebra element returns that element.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceCoefficientRingHom

def completedGroupAlgebraNaturalSourceCoefficientRingHom :
    R →+* CompletedGroupAlgebraNaturalSource R G :=
  (completedGroupAlgebraNaturalSourceOf (R := R) (G := G)).comp
    (MonoidAlgebra.singleOneRingHom (R := R) (M := G))

The coefficient-ring embedding into the natural-topology source.

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupMonoidHom

def completedGroupAlgebraNaturalSourceGroupMonoidHom :
    G →* CompletedGroupAlgebraNaturalSource R G :=
  (completedGroupAlgebraNaturalSourceOf (R := R) (G := G)).toMonoidHom.comp
    (MonoidAlgebra.of R G)

The group-like embedding into the natural-topology source.

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupUnitsHom

def completedGroupAlgebraNaturalSourceGroupUnitsHom :
    G →* (CompletedGroupAlgebraNaturalSource R G)ˣ :=
  (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G)).toHomUnits

The same group-like map with its invertibility recorded in the codomain.

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupUnitsHom_coe

@[simp]
theorem completedGroupAlgebraNaturalSourceGroupUnitsHom_coe (g : G) :
    ((completedGroupAlgebraNaturalSourceGroupUnitsHom (R := R) (G := G) g :
        (CompletedGroupAlgebraNaturalSource R G)ˣ) :
      CompletedGroupAlgebraNaturalSource R G) =
      completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g

Forgetting invertibility from the group-like units map gives the group-like monoid map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra

@[simp]
theorem completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra (r : R) :
    (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r).toMonoidAlgebra =
      MonoidAlgebra.single 1 r

The wrapped coefficient embedding forgets to the group algebra's scalar at the identity.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra

@[simp]
theorem completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra (g : G) :
    (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g).toMonoidAlgebra =
      MonoidAlgebra.of R G g

The wrapped group-like embedding forgets to the usual group-algebra basis element.

Show Lean proof

Instance CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraNaturalSource

instance instTopologicalSpaceCompletedGroupAlgebraNaturalSource :
    TopologicalSpace (CompletedGroupAlgebraNaturalSource R G) := by
  letI : TopologicalSpace (MonoidAlgebra R G) :=
    completedGroupAlgebraNaturalTopology R G
  exact (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).topologicalSpace

Equip the natural-source wrapper with the topology induced by the completed group algebra.

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceHomeomorph

def completedGroupAlgebraNaturalSourceHomeomorph :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      completedGroupAlgebraNaturalTopology R G
    CompletedGroupAlgebraNaturalSource R G ≃ₜ MonoidAlgebra R G := by
  letI : TopologicalSpace (MonoidAlgebra R G) :=
    completedGroupAlgebraNaturalTopology R G
  exact (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).homeomorph

The forgetful equivalence is a homeomorphism to the raw group algebra carrying the natural topology.

Structure CompletedGroupAlgebra.CompletedGroupAlgebraKernelSource

@[ext]
structure CompletedGroupAlgebraKernelSource (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
  /-- The group-algebra element carried by the kernel-neighborhood-topology wrapper. -/
  toMonoidAlgebra : MonoidAlgebra R G

A genuine copy of the abstract group algebra reserved for the open-ideal/finite-group kernel-neighborhood topology.

Definition CompletedGroupAlgebra.completedGroupAlgebraKernelSourceEquiv

def completedGroupAlgebraKernelSourceEquiv :
    CompletedGroupAlgebraKernelSource R G ≃ MonoidAlgebra R G where
  toFun := CompletedGroupAlgebraKernelSource.toMonoidAlgebra
  invFun := fun x => CompletedGroupAlgebraKernelSource.mk x
  left_inv x := by cases x; rfl
  right_inv _ := rfl

Forget the kernel-neighborhood-topology wrapper.

Instance CompletedGroupAlgebra.instRingCompletedGroupAlgebraKernelSource

instance instRingCompletedGroupAlgebraKernelSource :
    Ring (CompletedGroupAlgebraKernelSource R G) :=
  (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).ring

Transport the group-algebra ring structure to its kernel-neighborhood wrapper.

Definition CompletedGroupAlgebra.completedGroupAlgebraKernelSourceRingEquiv

def completedGroupAlgebraKernelSourceRingEquiv :
    CompletedGroupAlgebraKernelSource R G ≃+* MonoidAlgebra R G :=
  (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).ringEquiv

Algebraic form of the forgetful equivalence from the kernel-neighborhood source.

Instance CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraKernelSource

instance instTopologicalSpaceCompletedGroupAlgebraKernelSource :
    TopologicalSpace (CompletedGroupAlgebraKernelSource R G) := by
  letI : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  exact (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).topologicalSpace

Equip the kernel-source wrapper with the open-finite-quotient kernel topology.

Definition CompletedGroupAlgebra.completedGroupAlgebraKernelSourceHomeomorph

def completedGroupAlgebraKernelSourceHomeomorph :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    CompletedGroupAlgebraKernelSource R G ≃ₜ MonoidAlgebra R G := by
  letI : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  exact (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).homeomorph

The forgetful equivalence is a homeomorphism to the raw group algebra carrying the kernel-neighborhood topology.

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraNaturalSourceRingHom

def toCompletedGroupAlgebraNaturalSourceRingHom :
    CompletedGroupAlgebraNaturalSource R G →+* CompletedGroupAlgebraCarrier R G :=
  (toCompletedGroupAlgebraRingHom R G).comp
    (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).toRingHom

Canonical map from the natural-topology source wrapper.

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraNaturalSourceRingHom_coefficient

@[simp]
theorem toCompletedGroupAlgebraNaturalSourceRingHom_coefficient (r : R) :
    toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
        (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r) =
      algebraMap R (CompletedGroupAlgebraCarrier R G) r

On coefficients, the wrapped canonical map is the completed algebra's scalar map.

Show Lean proof

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraNaturalSourceRingHom_group

@[simp]
theorem toCompletedGroupAlgebraNaturalSourceRingHom_group (g : G) :
    toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
        (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g) =
      toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)

On group-like elements, the wrapped canonical map is the usual completed group element.

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraRingHom_naturalTopology

theorem continuous_toCompletedGroupAlgebraRingHom_naturalTopology :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      completedGroupAlgebraNaturalTopology R G
    Continuous (toCompletedGroupAlgebraRingHom R G)

The dense map from the abstract group algebra to the completed group algebra is continuous for the natural finite-quotient topology.

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraNaturalSourceRingHom

theorem continuous_toCompletedGroupAlgebraNaturalSourceRingHom :
    Continuous (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G))

The natural-source wrapper's canonical map is continuous by construction.

Show Lean proof

Theorem CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraNaturalSourceRingHom

theorem denseRange_toCompletedGroupAlgebraNaturalSourceRingHom
    : DenseRange (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G))

The natural-source wrapper has the same dense image as the raw algebraic group ring.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceStageMap

def completedGroupAlgebraNaturalSourceStageMap (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraNaturalSource R G →+* CompletedGroupAlgebraStage R G U :=
  (completedGroupAlgebraStageMap R G U).comp
    (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).toRingHom

A finite-stage group-algebra map with the natural-topology source kept explicit in its type.

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceStageMap_apply

@[simp]
theorem completedGroupAlgebraNaturalSourceStageMap_apply
    (U : CompletedGroupAlgebraIndex G) (x : CompletedGroupAlgebraNaturalSource R G) :
    completedGroupAlgebraNaturalSourceStageMap R G U x =
      completedGroupAlgebraStageMap R G U x.toMonoidAlgebra

The finite-stage map from the natural-source wrapper is the ordinary stage map after forgetting the wrapper.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraContinuousLinearMap_naturalTopology

def toCompletedGroupAlgebraContinuousLinearMap_naturalTopology :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      completedGroupAlgebraNaturalTopology R G
    MonoidAlgebra R G →L[R] CompletedGroupAlgebraCarrier R G := by
  letI : TopologicalSpace (MonoidAlgebra R G) :=
    completedGroupAlgebraNaturalTopology R G
  exact
    { toLinearMap := toCompletedGroupAlgebraLinearMap R G
      cont := continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G) }

The canonical map as a continuous \(R\)-linear map for the topology induced from \(\widehat{R[G]}\).

Theorem CompletedGroupAlgebra.groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit

omit [IsTopologicalRing R] in
theorem groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit :
    groupAlgebraOpenFiniteQuotientKernelTopology R G =
      TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
          inferInstance

The kernel-neighborhood topology is exactly the topology induced by the canonical map from \(R[G]\) to the two-parameter kernel-neighborhood limit.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit

theorem completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    completedGroupAlgebraNaturalTopology R G =
      TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
          inferInstance

Under the profinite coefficient hypothesis, the topology on \(R[G]\) induced from \(\widehat{R[G]}\) agrees with the topology induced by the two-parameter kernel-neighborhood limit.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology

theorem completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    completedGroupAlgebraNaturalTopology R G =
      groupAlgebraOpenFiniteQuotientKernelTopology R G

Ribes--Zalesskii Section \(5.3\) natural topology comparison: the topology on the abstract group algebra induced from \(\widehat{R[G]}\) is the kernel-neighborhood topology generated by the maps \(R[G] \to (R/I)[G/U]\).

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceHomeomorphKernelSource

def completedGroupAlgebraNaturalSourceHomeomorphKernelSource
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    CompletedGroupAlgebraNaturalSource R G ≃ₜ CompletedGroupAlgebraKernelSource R G where
  toEquiv :=
    (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).trans
      (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm
  continuous_toFun := by
    let τnat := completedGroupAlgebraNaturalTopology R G
    let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
    have hτ : τnat = τker :=
      completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
        (R := R) (G := G)
    have hforget :
        @Continuous (CompletedGroupAlgebraNaturalSource R G) (MonoidAlgebra R G)
          inferInstance τnat
          (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)) := by
      letI : TopologicalSpace (MonoidAlgebra R G) := τnat
      exact
        (completedGroupAlgebraNaturalSourceHomeomorph (R := R) (G := G)).continuous
    have hid : @Continuous (MonoidAlgebra R G) (MonoidAlgebra R G) τnat τker id := by
      rw [hτ]
      exact continuous_id
    have hwrap :
        @Continuous (MonoidAlgebra R G) (CompletedGroupAlgebraKernelSource R G)
          τker inferInstance
          (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm :=
      (completedGroupAlgebraKernelSourceHomeomorph (R := R) (G := G)).symm.continuous
    have hraw :=
      @Continuous.comp
        (CompletedGroupAlgebraNaturalSource R G) (MonoidAlgebra R G) (MonoidAlgebra R G)
        inferInstance τnat τker
        (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)) id hid hforget
    have htotal :=
      @Continuous.comp
        (CompletedGroupAlgebraNaturalSource R G) (MonoidAlgebra R G)
        (CompletedGroupAlgebraKernelSource R G)
        inferInstance τker inferInstance
        (id ∘ completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G))
        (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm hwrap hraw
    change Continuous
      ((completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm ∘ id ∘
        (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)))
    exact htotal
  continuous_invFun := by
    let τnat := completedGroupAlgebraNaturalTopology R G
    let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
    have hτ : τnat = τker :=
      completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
        (R := R) (G := G)
    have hforget :
        @Continuous (CompletedGroupAlgebraKernelSource R G) (MonoidAlgebra R G)
          inferInstance τker
          (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)) :=
      (completedGroupAlgebraKernelSourceHomeomorph (R := R) (G := G)).continuous
    have hid : @Continuous (MonoidAlgebra R G) (MonoidAlgebra R G) τker τnat id := by
      rw [hτ]
      exact continuous_id
    have hwrap :
        @Continuous (MonoidAlgebra R G) (CompletedGroupAlgebraNaturalSource R G)
          τnat inferInstance
          (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).symm := by
      letI : TopologicalSpace (MonoidAlgebra R G) := τnat
      exact
        (completedGroupAlgebraNaturalSourceHomeomorph (R := R) (G := G)).symm.continuous
    have hraw :=
      @Continuous.comp
        (CompletedGroupAlgebraKernelSource R G) (MonoidAlgebra R G) (MonoidAlgebra R G)
        inferInstance τker τnat
        (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)) id hid hforget
    have htotal :=
      @Continuous.comp
        (CompletedGroupAlgebraKernelSource R G) (MonoidAlgebra R G)
        (CompletedGroupAlgebraNaturalSource R G)
        inferInstance τnat inferInstance
        (id ∘ completedGroupAlgebraKernelSourceEquiv (R := R) (G := G))
        (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).symm hwrap hraw
    change Continuous
      ((completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).symm ∘ id ∘
        (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)))
    exact htotal

The two source wrappers are canonically homeomorphic once the coefficient ring is profinite.

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraKernelSourceRingHom

def toCompletedGroupAlgebraKernelSourceRingHom :
    CompletedGroupAlgebraKernelSource R G →+* CompletedGroupAlgebraCarrier R G :=
  (toCompletedGroupAlgebraRingHom R G).comp
    (completedGroupAlgebraKernelSourceRingEquiv (R := R) (G := G)).toRingHom

Canonical map from the kernel-neighborhood source wrapper.

Theorem CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraRingHom_kernelTopology

theorem continuous_toCompletedGroupAlgebraRingHom_kernelTopology
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    Continuous (toCompletedGroupAlgebraRingHom R G)

The canonical map \(R[G] \to \widehat{R[G]}\) is continuous for the kernel-neighborhood topology on \(R[G]\).

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraKernelSourceRingHom

theorem continuous_toCompletedGroupAlgebraKernelSourceRingHom
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    Continuous (toCompletedGroupAlgebraKernelSourceRingHom (R := R) (G := G))

The kernel-wrapper canonical map is continuous under the profinite coefficient hypothesis.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraContinuousLinearMap_kernelTopology

def toCompletedGroupAlgebraContinuousLinearMap_kernelTopology
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    MonoidAlgebra R G →L[R] CompletedGroupAlgebraCarrier R G := by
  letI : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  exact
    { toLinearMap := toCompletedGroupAlgebraLinearMap R G
      cont := continuous_toCompletedGroupAlgebraRingHom_kernelTopology
        (R := R) (G := G) }

The canonical map as a continuous \(R\)-linear map for the kernel-neighborhood topology.

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

Declarations