Module

OpenFiniteComparison.lean

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

54 declarations indexed from sourceView source ↗

Module documentation

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

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.

Imports3

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

Imported by5

def

completedGroupAlgebraToOpenFiniteQuotientLimit

L40 ↗

CompletedGroupAlgebra.completedGroupAlgebraToOpenFiniteQuotientLimit

Documentation

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]\).

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

Lean source · statement

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

theorem

completedGroupAlgebraOpenFiniteQuotientLimitProjection_fromCompleted

L63 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_fromCompleted

Documentation

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

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

Lean source · statement

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

theorem

completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra

L77 ↗

CompletedGroupAlgebra.completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra

Documentation

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

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

Lean source · statement

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

def

completedGroupAlgebraToOpenFiniteQuotientLimitRingHom

L91 ↗

CompletedGroupAlgebra.completedGroupAlgebraToOpenFiniteQuotientLimitRingHom

Documentation

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

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

Lean source · full declaration

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

theorem

openFiniteLimitProjection_comp_fromCompleted

L116 ↗

CompletedGroupAlgebra.openFiniteLimitProjection_comp_fromCompleted

Documentation

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

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

Lean source · statement

theorem openFiniteLimitProjection_comp_fromCompleted
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K).comp
        (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G) =
      completedGroupAlgebraOpenFiniteQuotientProjection R G K

theorem

completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA

L130 ↗

CompletedGroupAlgebra.completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA

Documentation

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

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

Lean source · statement

theorem completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA :
    (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G).comp
        (toCompletedGroupAlgebraRingHom R G) =
      toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G

theorem

continuous_completedGroupAlgebraToOpenFiniteQuotientLimit

L139 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraToOpenFiniteQuotientLimit

Documentation

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

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

Lean source · statement

theorem continuous_completedGroupAlgebraToOpenFiniteQuotientLimit :
    Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)

theorem

denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit

L166 ↗

CompletedGroupAlgebra.denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit

Documentation

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.

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

Lean source · statement

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

theorem

injective_completedGroupAlgebraToOpenFiniteQuotientLimit

L190 ↗

CompletedGroupAlgebra.injective_completedGroupAlgebraToOpenFiniteQuotientLimit

Documentation

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

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

Lean source · statement

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

theorem

surjective_completedGroupAlgebraToOpenFiniteQuotientLimit

L228 ↗

CompletedGroupAlgebra.surjective_completedGroupAlgebraToOpenFiniteQuotientLimit

Documentation

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

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

Lean source · statement

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

theorem

bijective_completedGroupAlgebraToOpenFiniteQuotientLimit

L254 ↗

CompletedGroupAlgebra.bijective_completedGroupAlgebraToOpenFiniteQuotientLimit

Documentation

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

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

Lean source · statement

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

def

completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv

L266 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv

Documentation

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.

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

Lean source · statement

def completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    CompletedGroupAlgebraCarrier R G ≃+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G

theorem

completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv_apply

L278 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv_apply

Documentation

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

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

Lean source · statement

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

def

completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph

L290 ↗

CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph

Documentation

The fixed-coefficient completed group algebra is homeomorphic to the two-parameter open finite quotient 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
        (CompletedGroupAlgebraOpenQuotientIndex R G)] :
    CompletedGroupAlgebraCarrier R G ≃ₜ CompletedGroupAlgebraOpenFiniteQuotientLimit R G

theorem

denseRange_toCompletedGroupAlgebra

L308 ↗

CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebra

Documentation

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

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

Lean source · statement

theorem denseRange_toCompletedGroupAlgebra :
    DenseRange (toCompletedGroupAlgebra R G)

theorem

denseRange_toCompletedGroupAlgebraRingHom

L334 ↗

CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraRingHom

Documentation

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

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

Lean source · statement

theorem denseRange_toCompletedGroupAlgebraRingHom :
    DenseRange (toCompletedGroupAlgebraRingHom R G)

def

completedGroupAlgebraNaturalTopology

L345 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalTopology

Documentation

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]\).

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

Lean source · statement

def completedGroupAlgebraNaturalTopology (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    TopologicalSpace (MonoidAlgebra R G)

structure

CompletedGroupAlgebraNaturalSource

L357 ↗

CompletedGroupAlgebra.CompletedGroupAlgebraNaturalSource

Documentation

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.

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

Lean source · full declaration

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

def

completedGroupAlgebraNaturalSourceEquiv

L364 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceEquiv

Documentation

Forget the natural-topology wrapper.

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

Lean source · full declaration

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

instance

instRingCompletedGroupAlgebraNaturalSource

L372 ↗

CompletedGroupAlgebra.instRingCompletedGroupAlgebraNaturalSource

Documentation

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

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

Lean source · statement

instance instRingCompletedGroupAlgebraNaturalSource :
    Ring (CompletedGroupAlgebraNaturalSource R G)

def

completedGroupAlgebraNaturalSourceRingEquiv

L377 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceRingEquiv

Documentation

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

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

Lean source · statement

def completedGroupAlgebraNaturalSourceRingEquiv :
    CompletedGroupAlgebraNaturalSource R G ≃+* MonoidAlgebra R G

def

completedGroupAlgebraNaturalSourceOf

L383 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceOf

Documentation

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.

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

Lean source · statement

def completedGroupAlgebraNaturalSourceOf :
    MonoidAlgebra R G →+* CompletedGroupAlgebraNaturalSource R G

theorem

completedGroupAlgebraNaturalSourceOf_toMonoidAlgebra

L390 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceOf_toMonoidAlgebra

Documentation

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

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

Lean source · statement

theorem completedGroupAlgebraNaturalSourceOf_toMonoidAlgebra (x : MonoidAlgebra R G) :
    (completedGroupAlgebraNaturalSourceOf (R := R) (G := G) x).toMonoidAlgebra = x

def

completedGroupAlgebraNaturalSourceCoefficientRingHom

L398 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceCoefficientRingHom

Documentation

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

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

Lean source · statement

def completedGroupAlgebraNaturalSourceCoefficientRingHom :
    R →+* CompletedGroupAlgebraNaturalSource R G

def

completedGroupAlgebraNaturalSourceGroupMonoidHom

L404 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupMonoidHom

Documentation

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

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

Lean source · statement

def completedGroupAlgebraNaturalSourceGroupMonoidHom :
    G →* CompletedGroupAlgebraNaturalSource R G

def

completedGroupAlgebraNaturalSourceGroupUnitsHom

L410 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupUnitsHom

Documentation

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

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

Lean source · statement

def completedGroupAlgebraNaturalSourceGroupUnitsHom :
    G →* (CompletedGroupAlgebraNaturalSource R G)ˣ

theorem

completedGroupAlgebraNaturalSourceGroupUnitsHom_coe

L416 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupUnitsHom_coe

Documentation

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

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

Lean source · statement

theorem completedGroupAlgebraNaturalSourceGroupUnitsHom_coe (g : G) :
    ((completedGroupAlgebraNaturalSourceGroupUnitsHom (R := R) (G := G) g :
        (CompletedGroupAlgebraNaturalSource R G)ˣ) :
      CompletedGroupAlgebraNaturalSource R G) =
      completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g

theorem

completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra

L425 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra

Documentation

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

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

Lean source · statement

theorem completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra (r : R) :
    (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r).toMonoidAlgebra =
      MonoidAlgebra.single 1 r

theorem

completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra

L433 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra

Documentation

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

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

Lean source · statement

theorem completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra (g : G) :
    (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g).toMonoidAlgebra =
      MonoidAlgebra.of R G g

instance

instTopologicalSpaceCompletedGroupAlgebraNaturalSource

L440 ↗

CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraNaturalSource

Documentation

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

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

Lean source · statement

instance instTopologicalSpaceCompletedGroupAlgebraNaturalSource :
    TopologicalSpace (CompletedGroupAlgebraNaturalSource R G)

def

completedGroupAlgebraNaturalSourceHomeomorph

L448 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceHomeomorph

Documentation

The forgetful equivalence is a homeomorphism to the raw group algebra carrying the natural 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

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

structure

CompletedGroupAlgebraKernelSource

L459 ↗

CompletedGroupAlgebra.CompletedGroupAlgebraKernelSource

Documentation

A genuine copy of the abstract group algebra reserved for the open-ideal/finite-group kernel-neighborhood 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

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

def

completedGroupAlgebraKernelSourceEquiv

L465 ↗

CompletedGroupAlgebra.completedGroupAlgebraKernelSourceEquiv

Documentation

Forget the kernel-neighborhood-topology wrapper.

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

Lean source · full declaration

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

instance

instRingCompletedGroupAlgebraKernelSource

L473 ↗

CompletedGroupAlgebra.instRingCompletedGroupAlgebraKernelSource

Documentation

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

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

Lean source · statement

instance instRingCompletedGroupAlgebraKernelSource :
    Ring (CompletedGroupAlgebraKernelSource R G)

def

completedGroupAlgebraKernelSourceRingEquiv

L478 ↗

CompletedGroupAlgebra.completedGroupAlgebraKernelSourceRingEquiv

Documentation

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

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

Lean source · statement

def completedGroupAlgebraKernelSourceRingEquiv :
    CompletedGroupAlgebraKernelSource R G ≃+* MonoidAlgebra R G

instance

instTopologicalSpaceCompletedGroupAlgebraKernelSource

L483 ↗

CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraKernelSource

Documentation

Equip the kernel-source wrapper with the open-finite-quotient kernel 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instTopologicalSpaceCompletedGroupAlgebraKernelSource :
    TopologicalSpace (CompletedGroupAlgebraKernelSource R G)

def

completedGroupAlgebraKernelSourceHomeomorph

L491 ↗

CompletedGroupAlgebra.completedGroupAlgebraKernelSourceHomeomorph

Documentation

The forgetful equivalence is a homeomorphism to the raw group algebra carrying the kernel-neighborhood 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

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

def

toCompletedGroupAlgebraNaturalSourceRingHom

L500 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraNaturalSourceRingHom

Documentation

Canonical map from the natural-topology source wrapper.

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

Lean source · statement

def toCompletedGroupAlgebraNaturalSourceRingHom :
    CompletedGroupAlgebraNaturalSource R G →+* CompletedGroupAlgebraCarrier R G

theorem

toCompletedGroupAlgebraNaturalSourceRingHom_coefficient

L507 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraNaturalSourceRingHom_coefficient

Documentation

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

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

Lean source · statement

theorem toCompletedGroupAlgebraNaturalSourceRingHom_coefficient (r : R) :
    toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
        (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r) =
      algebraMap R (CompletedGroupAlgebraCarrier R G) r

theorem

toCompletedGroupAlgebraNaturalSourceRingHom_group

L525 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraNaturalSourceRingHom_group

Documentation

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

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

Lean source · statement

theorem toCompletedGroupAlgebraNaturalSourceRingHom_group (g : G) :
    toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
        (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g) =
      toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)

theorem

continuous_toCompletedGroupAlgebraRingHom_naturalTopology

L538 ↗

CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraRingHom_naturalTopology

Documentation

The dense map from the abstract group algebra to the completed group algebra is continuous for the natural finite-quotient 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

theorem continuous_toCompletedGroupAlgebraRingHom_naturalTopology :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      completedGroupAlgebraNaturalTopology R G
    Continuous (toCompletedGroupAlgebraRingHom R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) :=
    completedGroupAlgebraNaturalTopology R G
  change Continuous (toCompletedGroupAlgebra R G)
  exact (continuous_induced_dom : Continuous (toCompletedGroupAlgebra R G))

theorem

continuous_toCompletedGroupAlgebraNaturalSourceRingHom

L548 ↗

CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraNaturalSourceRingHom

Documentation

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

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

Lean source · statement

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

theorem

denseRange_toCompletedGroupAlgebraNaturalSourceRingHom

L557 ↗

CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraNaturalSourceRingHom

Documentation

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

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

Lean source · statement

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

def

completedGroupAlgebraNaturalSourceStageMap

L568 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceStageMap

Documentation

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

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

Lean source · statement

def completedGroupAlgebraNaturalSourceStageMap (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraNaturalSource R G →+* CompletedGroupAlgebraStage R G U

theorem

completedGroupAlgebraNaturalSourceStageMap_apply

L576 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceStageMap_apply

Documentation

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

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

Lean source · statement

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

def

toCompletedGroupAlgebraContinuousLinearMap_naturalTopology

L589 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraContinuousLinearMap_naturalTopology

Documentation

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

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

Lean source · full declaration

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

theorem

groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit

L604 ↗

CompletedGroupAlgebra.groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit

Documentation

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

Source context 12 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalRing R] in

Lean source · statement

theorem groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit :
    groupAlgebraOpenFiniteQuotientKernelTopology R G =
      TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
          inferInstance

theorem

completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit

L624 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit

Documentation

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.

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

Lean source · statement

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

theorem

completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology

L646 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology

Documentation

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]\).

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

Lean source · statement

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

def

completedGroupAlgebraNaturalSourceHomeomorphKernelSource

L656 ↗

CompletedGroupAlgebra.completedGroupAlgebraNaturalSourceHomeomorphKernelSource

Documentation

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

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

Lean source · full declaration

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
      let : 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
      let : 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

def

toCompletedGroupAlgebraKernelSourceRingHom

L739 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraKernelSourceRingHom

Documentation

Canonical map from the kernel-neighborhood source wrapper.

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

Lean source · statement

def toCompletedGroupAlgebraKernelSourceRingHom :
    CompletedGroupAlgebraKernelSource R G →+* CompletedGroupAlgebraCarrier R G

theorem

continuous_toCompletedGroupAlgebraRingHom_kernelTopology

L748 ↗

CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraRingHom_kernelTopology

Documentation

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

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

Lean source · full declaration

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) := by
  let τnat := completedGroupAlgebraNaturalTopology R G
  let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
  have hτ : τnat = τker :=
    completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
      (R := R) (G := G)
  change @Continuous (MonoidAlgebra R G) (CompletedGroupAlgebraCarrier R G)
    τker inferInstance (toCompletedGroupAlgebraRingHom R G)
  rw [← hτ]
  exact continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)

theorem

continuous_toCompletedGroupAlgebraKernelSourceRingHom

L765 ↗

CompletedGroupAlgebra.continuous_toCompletedGroupAlgebraKernelSourceRingHom

Documentation

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

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

Lean source · statement

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

def

toCompletedGroupAlgebraContinuousLinearMap_kernelTopology

L776 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraContinuousLinearMap_kernelTopology

Documentation

The canonical map as a continuous \(R\)-linear map for the kernel-neighborhood 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 w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

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

Module documentation

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

Declarations