Module

ClassComparison.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison

31 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / Class Comparison

This module compares the all-finite and \(C\)-indexed named completed carriers through their canonical projections, and bundles the resulting inverse maps as ring, algebra, and topological equivalences for pro-\(C\) groups.

Imports2

Imported by2

def

completedGroupAlgebraProjectionToStageInClass

L36 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjectionToStageInClass

Documentation

The projection from the all-finite completion to a stage indexed by a finite quotient class \(C\), bundled as a ring homomorphism.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

def completedGroupAlgebraProjectionToStageInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraStageInClass C R G U

theorem

completedGroupAlgebraProjectionToStageInClass_compatible

L47 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjectionToStageInClass_compatible

Documentation

The all-finite projection to a \(C\)-indexed stage is compatible with the transition maps of the \(C\)-indexed tower.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraProjectionToStageInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraTransitionInClass C R G hUV
        (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C V x) =
      completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C U x

def

completedGroupAlgebraToInClass

L67 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass

Documentation

The comparison map from the ordinary all-finite completed group algebra to the inverse limit over any finite-quotient class.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

def completedGroupAlgebraToInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraInClass C R G

theorem

completedGroupAlgebraToInClass_projection

L88 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_projection

Documentation

Projecting the comparison map \(\widehat{R[G]}\to\widehat{R[G]}_{C}\) to a \(C\)-indexed finite stage recovers the corresponding all-finite projection.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraToInClass_projection
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraProjectionInClass C R G U
        (completedGroupAlgebraToInClass (R := R) (G := G) C x) =
      completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C U x

def

completedGroupAlgebraToInClassRingHom

L100 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom

Documentation

The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit is bundled as a ring homomorphism.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraToInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v}) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraInClass C R G where
  toFun := completedGroupAlgebraToInClass (R := R) (G := G) C
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl

theorem

completedGroupAlgebraToInClassRingHom_apply

L126 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom_apply

Documentation

The comparison map from the all-finite completed group algebra to the \(C\)-indexed model is evaluated by reading the corresponding finite-stage coordinate.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraToInClassRingHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

def

completedGroupAlgebraToInClassAlgHom

L137 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassAlgHom

Documentation

The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit, as an \(R\)-algebra homomorphism.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraToInClassAlgHom
    (C : ProCGroups.FiniteGroupClass.{v}) :
    CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraInClass C R G where
  toRingHom := completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
  commutes' := by
    intro r
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl

theorem

completedGroupAlgebraToInClassAlgHom_apply

L152 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassAlgHom_apply

Documentation

The comparison map from the all-finite completed group algebra to the \(C\)-indexed model is evaluated by reading the corresponding finite-stage coordinate.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraToInClassAlgHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

theorem

continuous_completedGroupAlgebraToInClass

L163 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraToInClass

Documentation

The comparison map from the all-finite completed group algebra to the \(C\)-indexed completed group algebra is continuous for the inverse-limit topology.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem continuous_completedGroupAlgebraToInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Continuous (completedGroupAlgebraToInClass (R := R) (G := G) C )

def

completedGroupAlgebraFromInClass

L192 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass

Documentation

For a pro-\(C\) group, the \(C\)-indexed inverse limit maps back to the ordinary all-finite completed group algebra by reading the same open-normal quotient stages.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

def completedGroupAlgebraFromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraInClass C R G → CompletedGroupAlgebraCarrier R G

theorem

completedGroupAlgebraFromInClass_projection

L222 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass_projection

Documentation

Projecting the comparison map \(\widehat{R[G]}_{C}\to\widehat{R[G]}\) to an all-finite stage recovers the matching \(C\)-indexed projection.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraFromInClass_projection
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (U :
        CompletedGroupAlgebraIndex G)
    (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) =
      completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraIndexToInClass G C hForm hG U) x

def

completedGroupAlgebraFromInClassRingHom

L237 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom

Documentation

The ring-homomorphism form of the comparison map is the bundled ring map determined by the underlying coordinate formula for the completed group algebra.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraFromInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraInClass C R G →+* CompletedGroupAlgebraCarrier R G where
  toFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
  map_zero' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG 0) =
      completedGroupAlgebraProjection R G U (0 : CompletedGroupAlgebraCarrier R G)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_zero (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U))
  map_one' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG 1) =
      completedGroupAlgebraProjection R G U (1 : CompletedGroupAlgebraCarrier R G)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_one (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U))
  map_add' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG (x + y)) =
      completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x +
          completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG y)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_add (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y
  map_mul' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG (x * y)) =
      completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x *
          completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG y)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_mul (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y

theorem

completedGroupAlgebraFromInClassRingHom_apply

L288 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_apply

Documentation

The comparison map from the \(C\)-indexed completed group algebra to the all-finite model is evaluated by reading the corresponding finite-stage coordinate.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraFromInClassRingHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

def

completedGroupAlgebraFromInClassAlgHom

L300 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassAlgHom

Documentation

The algebra homomorphism form of the comparison map is the bundled algebra map determined by the underlying coordinate formula for the completed group algebra.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraFromInClassAlgHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraCarrier R G where
  toRingHom := completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG
  commutes' := by
    intro r
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
          (algebraMap R (CompletedGroupAlgebraInClass C R G) r)) =
      completedGroupAlgebraProjection R G U (algebraMap R (CompletedGroupAlgebraCarrier R G) r)
    rw [completedGroupAlgebraFromInClass_projection]
    change completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraIndexToInClass G C hForm hG U)
        (algebraMap R (CompletedGroupAlgebraInClass C R G) r) =
      algebraMap R (CompletedGroupAlgebraStage R G U) r
    exact completedGroupAlgebraProjectionInClass_algebraMap (R := R) (G := G) C
      (completedGroupAlgebraIndexToInClass G C hForm hG U) r

theorem

completedGroupAlgebraFromInClassAlgHom_apply

L326 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassAlgHom_apply

Documentation

The comparison map from the \(C\)-indexed completed group algebra to the all-finite model is evaluated by reading the corresponding finite-stage coordinate.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraFromInClassAlgHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

theorem

continuous_completedGroupAlgebraFromInClass

L338 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraFromInClass

Documentation

The comparison map from the \(C\)-indexed completed group algebra to the all-finite completed group algebra is continuous for the inverse-limit topology.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem continuous_completedGroupAlgebraFromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Continuous (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG)

theorem

completedGroupAlgebraFromInClass_toInClass

L383 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass_toInClass

Documentation

The composite from a \(C\)-indexed completion to the all-finite completion and back is the identity on the \(C\)-indexed completion.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraFromInClass_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
        (completedGroupAlgebraToInClass (R := R) (G := G) C x) = x

theorem

completedGroupAlgebraToInClass_fromInClass

L404 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_fromInClass

Documentation

The composite from the all-finite completion to the \(C\)-indexed completion and back is the identity on the all-finite completion.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraToInClass_fromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraToInClass (R := R) (G := G) C
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) = x

theorem

completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom

L427 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom

Documentation

The two comparison ring homomorphisms are inverse to one another after composition.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp
        (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =
      RingHom.id (CompletedGroupAlgebraCarrier R G)

theorem

completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom

L439 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom

Documentation

The two comparison ring homomorphisms are inverse to one another after composition.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp
        (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG) =
      RingHom.id (CompletedGroupAlgebraInClass C R G)

def

completedGroupAlgebraInClassRingEquiv

L453 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv

Documentation

For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same ring, via the comparison maps.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraInClassRingEquiv
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraCarrier R G ≃+* CompletedGroupAlgebraInClass C R G where
  toFun := completedGroupAlgebraToInClass (R := R) (G := G) C
  invFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
  left_inv := by
    intro x
    exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hForm hG x
  right_inv := by
    intro x
    exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hForm hG x
  map_mul' := by
    intro x y
    exact map_mul (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) x y
  map_add' := by
    intro x y
    exact map_add (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) x y

theorem

completedGroupAlgebraInClassRingEquiv_apply

L477 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv_apply

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraInClassRingEquiv_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

theorem

completedGroupAlgebraInClassRingEquiv_symm_apply

L490 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv_symm_apply

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraInClassRingEquiv_symm_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).symm x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

def

completedGroupAlgebraInClassAlgEquiv

L502 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv

Documentation

For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same \(R\)-algebra.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

def completedGroupAlgebraInClassAlgEquiv
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraCarrier R G ≃ₐ[R] CompletedGroupAlgebraInClass C R G

theorem

completedGroupAlgebraInClassAlgEquiv_apply

L516 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv_apply

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraInClassAlgEquiv_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

theorem

completedGroupAlgebraInClassAlgEquiv_symm_apply

L529 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv_symm_apply

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraInClassAlgEquiv_symm_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG).symm x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

def

completedGroupAlgebraInClassHomeomorph

L538 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassHomeomorph

Documentation

The comparison equivalence is an equivalence of topological spaces.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraInClassHomeomorph
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraCarrier R G ≃ₜ CompletedGroupAlgebraInClass C R G where
  toEquiv := (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).toEquiv
  continuous_toFun := continuous_completedGroupAlgebraToInClass (R := R) (G := G) C
  continuous_invFun := continuous_completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

theorem

completedGroupAlgebraInClassHomeomorph_apply

L551 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassHomeomorph_apply

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraInClassHomeomorph_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

theorem

completedGroupAlgebraInClassHomeomorph_symm_apply

L564 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassHomeomorph_symm_apply

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraInClassHomeomorph_symm_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    (completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hForm hG).symm x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

theorem

completedGroupAlgebraToInClass_surjective

L576 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_surjective

Documentation

Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or dense algebraic model, together with closedness of the image in the completed target.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraToInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Function.Surjective (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )

theorem

completedGroupAlgebraFromInClass_surjective

L588 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClass_surjective

Documentation

Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or dense algebraic model, together with closedness of the image in the completed target.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem completedGroupAlgebraFromInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Function.Surjective (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)

Module documentation

Completed Group Algebra / Basic / Class Comparison

Declarations