Module

CanonicalMaps.lean

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

37 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Open Finite Quotient Topology / Canonical Maps

This module constructs the canonical dense maps from the abstract group algebra to the \(C\)-indexed and all-finite named completions, together with their bundled ring, algebra, and linear forms and finite-stage characterizations.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison

Imported by5

def

completedGroupAlgebraStageMapInClass

L35 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass

Documentation

The quotient map from the abstract group algebra \(R[G]\) to one \(C\)-indexed finite stage.

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 completedGroupAlgebraStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    MonoidAlgebra R G →+* CompletedGroupAlgebraStageInClass C R G U

theorem

completedGroupAlgebraStageMapInClass_of

L49 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_of

Documentation

At a \(C\)-indexed stage \(U\), the quotient map sends the group-like element of \(g\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(1\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (g : G) :
    completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.of R G g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

theorem

completedGroupAlgebraStageMapInClass_single

L67 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_single

Documentation

At a \(C\)-indexed stage \(U\), the quotient map sends the singleton at \(g\) with coefficient \(r\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(r\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_single
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (g : G) (r : R) :
    completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.single g r) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) r

theorem

completedGroupAlgebraStageMapInClass_smul

L82 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_smul

Documentation

The \(C\)-indexed quotient-stage map preserves scalar multiplication by elements of \(R\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_smul
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (r : R) (x : MonoidAlgebra R G) :
    completedGroupAlgebraStageMapInClass C R G U (r • x) =
      r • completedGroupAlgebraStageMapInClass C R G U x

theorem

completedGroupAlgebraStageMapInClass_algebraMap

L102 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_algebraMap

Documentation

The \(C\)-indexed quotient-stage map commutes with the canonical embeddings of scalars from \(R\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (r : R) :
    completedGroupAlgebraStageMapInClass C R G U (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r

theorem

completedGroupAlgebraStageMapInClass_surjective

L117 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_surjective

Documentation

The quotient map \(R[G]\to R[G/U]\) is surjective for every \(C\)-indexed stage \(U\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
    Function.Surjective (completedGroupAlgebraStageMapInClass C R G U)

theorem

completedGroupAlgebraStageMapInClass_compatible

L135 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_compatible

Documentation

The class-restricted completed group-algebra stage map is compatible with transition maps and coordinate projections for the completed group algebra.

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraTransitionInClass C R G hUV).comp
        (completedGroupAlgebraStageMapInClass C R G V) =
      completedGroupAlgebraStageMapInClass C R G U

theorem

completedGroupAlgebraStageMapInClass_compatibleMaps

L161 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_compatibleMaps

Documentation

The \(C\)-indexed finite-stage quotient maps form a compatible family.

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 completedGroupAlgebraStageMapInClass_compatibleMaps
    (C : ProCGroups.FiniteGroupClass.{v}) :
    (completedGroupAlgebraSystemInClass C R G).CompatibleMaps
      (fun U => completedGroupAlgebraStageMapInClass C R G U) := by
  intro U V hUV
  funext x
  exact congrFun
    (congrArg DFunLike.coe
      (completedGroupAlgebraStageMapInClass_compatible (R := R) (G := G) C hUV))
    x

def

toCompletedGroupAlgebraInClass

L175 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClass

Documentation

The canonical map \(R[G] \to \widehat{R[G]}_C\), obtained from all \(C\)-indexed quotient maps.

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 toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (x : MonoidAlgebra R G) : CompletedGroupAlgebraInClass C R G

theorem

completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass

L192 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass

Documentation

The \(U\)-coordinate of the canonical dense element in the \(C\)-indexed completion is the \(C\)-indexed stage map at \(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 completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) (x : MonoidAlgebra R G) :
    completedGroupAlgebraProjectionInClass C R G U
        (toCompletedGroupAlgebraInClass C R G x) =
      completedGroupAlgebraStageMapInClass C R G U x

theorem

toCompletedGroupAlgebraInClass_smul

L205 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClass_smul

Documentation

The canonical map from \(R[G]\) into the \(C\)-indexed completed group algebra preserves scalar multiplication by \(R\).

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 toCompletedGroupAlgebraInClass_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    (r : R) (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClass C R G (r • x) =
      r • toCompletedGroupAlgebraInClass C R G x

def

toCompletedGroupAlgebraInClassRingHom

L217 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom

Documentation

The canonical map \(R[G] \to \widehat{R[G]}_C\) 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 toCompletedGroupAlgebraInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →+* CompletedGroupAlgebraInClass C R G where
  toFun := toCompletedGroupAlgebraInClass C R G
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_zero (completedGroupAlgebraStageMapInClass C R G U)
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_one (completedGroupAlgebraStageMapInClass C R G U)
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_add (completedGroupAlgebraStageMapInClass C R G U) x y
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_mul (completedGroupAlgebraStageMapInClass C R G U) x y

theorem

toCompletedGroupAlgebraInClassRingHom_apply

L245 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom_apply

Documentation

The bundled ring homomorphism has the same underlying function as the coordinatewise 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 toCompletedGroupAlgebraInClassRingHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassRingHom C R G x =
      toCompletedGroupAlgebraInClass C R G x

def

toCompletedGroupAlgebraInClassAlgHom

L253 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassAlgHom

Documentation

The canonical map \(R[G] \to \widehat{R[G]}_C\), as an algebra 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 toCompletedGroupAlgebraInClassAlgHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraInClass C R G where
  toRingHom := toCompletedGroupAlgebraInClassRingHom C R G
  commutes' := by
    intro r
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    change completedGroupAlgebraStageMapInClass C R G U
        (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
    exact completedGroupAlgebraStageMapInClass_algebraMap (R := R) (G := G) C U r

theorem

toCompletedGroupAlgebraInClassAlgHom_apply

L273 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassAlgHom_apply

Documentation

Evaluating the canonical \(C\)-indexed algebra homomorphism gives the coordinatewise dense map toCompletedGroupAlgebraInClass.

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 toCompletedGroupAlgebraInClassAlgHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassAlgHom C R G x =
      toCompletedGroupAlgebraInClass C R G x

def

toCompletedGroupAlgebraInClassLinearMap

L281 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassLinearMap

Documentation

The canonical map \(R[G] \to \widehat{R[G]}_C\), as a linear 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 · full declaration

def toCompletedGroupAlgebraInClassLinearMap
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraInClass C R G where
  toFun := toCompletedGroupAlgebraInClass C R G
  map_add' := by
    intro x y
    exact map_add (toCompletedGroupAlgebraInClassRingHom C R G) x y
  map_smul' := toCompletedGroupAlgebraInClass_smul (R := R) (G := G) C

theorem

toCompletedGroupAlgebraInClassLinearMap_apply

L294 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassLinearMap_apply

Documentation

The bundled linear map has the same underlying function as the coordinatewise 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 toCompletedGroupAlgebraInClassLinearMap_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassLinearMap C R G x =
      toCompletedGroupAlgebraInClass C R G x

theorem

completedGAProjectionInClass_comp_toCompletedGAInClass

L306 ↗

CompletedGroupAlgebra.completedGAProjectionInClass_comp_toCompletedGAInClass

Documentation

Composing the \(U\)-coordinate projection from the \(C\)-indexed completion with its canonical dense ring homomorphism gives the \(C\)-indexed stage map at \(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 completedGAProjectionInClass_comp_toCompletedGAInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraProjectionInClass C R G U).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      completedGroupAlgebraStageMapInClass C R G U

theorem

denseRange_toCompletedGroupAlgebraInClass

L320 ↗

CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraInClass

Documentation

The abstract group algebra is dense in the \(C\)-indexed completed group algebra when \(G\) is pro-\(C\) and \(C\) is a formation.

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_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    DenseRange (toCompletedGroupAlgebraInClass C R G)

theorem

completedGroupAlgebraTransition_comp_projection

L355 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransition_comp_projection

Documentation

Projecting to a finer stage \(V\) and then applying the transition to \(U\) agrees with projecting directly to \(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 completedGroupAlgebraTransition_comp_projection
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraTransition R G hUV).comp
        (completedGroupAlgebraProjection R G V) =
      completedGroupAlgebraProjection R G U

def

completedGroupAlgebraStageMap

L365 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap

Documentation

The quotient map from the abstract group algebra \(R[G]\) to one finite stage \(R[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 completedGroupAlgebraStageMap (R : Type u) (G : Type v) [CommRing R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    MonoidAlgebra R G →+* CompletedGroupAlgebraStage R G U

theorem

completedGroupAlgebraStageMap_of

L378 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_of

Documentation

At an all-finite stage \(U\), the quotient map sends the group-like element of \(g\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(1\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMap_of
    (U : CompletedGroupAlgebraIndex G) (g : G) :
    completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1

theorem

completedGroupAlgebraStageMap_single

L398 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_single

Documentation

At an all-finite stage \(U\), the quotient map sends the singleton at \(g\) with coefficient \(r\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(r\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMap_single
    (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
    completedGroupAlgebraStageMap R G U (MonoidAlgebra.single g r) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) r

theorem

completedGroupAlgebraStageMap_smul

L415 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_smul

Documentation

The all-finite quotient-stage map preserves scalar multiplication by elements of \(R\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMap_smul
    (U : CompletedGroupAlgebraIndex G) (r : R) (x : MonoidAlgebra R G) :
    completedGroupAlgebraStageMap R G U (r • x) =
      r • completedGroupAlgebraStageMap R G U x

theorem

completedGroupAlgebraStageMap_algebraMap

L435 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_algebraMap

Documentation

The all-finite quotient-stage map commutes with the canonical embeddings of scalars from \(R\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMap_algebraMap
    (U : CompletedGroupAlgebraIndex G) (r : R) :
    completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStage R G U) r

theorem

completedGroupAlgebraStageMap_surjective

L451 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_surjective

Documentation

The quotient map \(R[G]\to R[G/U]\) is surjective for every all-finite stage \(U\).

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMap_surjective (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (completedGroupAlgebraStageMap R G U)

theorem

completedGroupAlgebraStageMap_compatible

L469 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_compatible

Documentation

The completed group-algebra stage map is compatible with transition maps and coordinate projections for the completed group algebra.

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 [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageMap_compatible
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraTransition R G hUV).comp (completedGroupAlgebraStageMap R G V) =
      completedGroupAlgebraStageMap R G U

theorem

completedGroupAlgebraStageMap_compatibleMaps

L498 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_compatibleMaps

Documentation

The finite-stage quotient maps form a compatible family into the completed group algebra system.

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 completedGroupAlgebraStageMap_compatibleMaps :
    (completedGroupAlgebraSystem R G).CompatibleMaps
      (fun U => completedGroupAlgebraStageMap R G U) := by
  intro U V hUV
  funext x
  exact congrFun
    (congrArg DFunLike.coe
      (completedGroupAlgebraStageMap_compatible (R := R) (G := G) (U := U) (V := V) hUV))
    x

def

toCompletedGroupAlgebra

L512 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebra

Documentation

The canonical map \(R[G] \to \widehat{R[G]}\), obtained from all quotient maps \(R[G]\to R[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 toCompletedGroupAlgebra (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (x : MonoidAlgebra R G) : CompletedGroupAlgebraCarrier R G

theorem

completedGroupAlgebraProjection_toCompletedGroupAlgebra

L525 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjection_toCompletedGroupAlgebra

Documentation

The \(U\)-coordinate of the canonical dense element in the all-finite completion is the all-finite stage map at \(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 completedGroupAlgebraProjection_toCompletedGroupAlgebra
    (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
    completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
      completedGroupAlgebraStageMap R G U x

theorem

toCompletedGroupAlgebra_smul

L535 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebra_smul

Documentation

The canonical map from \(R[G]\) into the all-finite completed group algebra preserves scalar multiplication by \(R\).

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 toCompletedGroupAlgebra_smul (r : R) (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebra R G (r • x) =
      r • toCompletedGroupAlgebra R G x

def

toCompletedGroupAlgebraRingHom

L557 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraRingHom

Documentation

The canonical map \(R[G] \to \widehat{R[G]}\) 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 toCompletedGroupAlgebraRingHom (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    MonoidAlgebra R G →+* CompletedGroupAlgebraCarrier R G where
  toFun := toCompletedGroupAlgebra R G
  map_zero' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_zero (completedGroupAlgebraStageMap R G U)
  map_one' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_one (completedGroupAlgebraStageMap R G U)
  map_add' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_add (completedGroupAlgebraStageMap R G U) x y
  map_mul' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_mul (completedGroupAlgebraStageMap R G U) x y

theorem

completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra

L584 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra

Documentation

Restricting the all-finite completion to its \(C\)-indexed coordinates after applying the all-finite dense map agrees with the canonical \(C\)-indexed dense 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 completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
    (C : ProCGroups.FiniteGroupClass.{v}) :
    (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp
        (toCompletedGroupAlgebraRingHom R G) =
      toCompletedGroupAlgebraInClassRingHom C R G

theorem

completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass

L600 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass

Documentation

Under the formation and pro-\(C\) hypotheses, transporting the \(C\)-indexed dense map back to the all-finite completion recovers the all-finite dense 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 completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      toCompletedGroupAlgebraRingHom R G

def

toCompletedGroupAlgebraAlgHom

L611 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraAlgHom

Documentation

The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-algebra 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 toCompletedGroupAlgebraAlgHom (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraCarrier R G where
  toRingHom := toCompletedGroupAlgebraRingHom R G
  commutes' := by
    intro r
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStage R G U) r
    exact completedGroupAlgebraStageMap_algebraMap (R := R) (G := G) U r

def

toCompletedGroupAlgebraLinearMap

L625 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraLinearMap

Documentation

The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-linear 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 · full declaration

def toCompletedGroupAlgebraLinearMap (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraCarrier R G where
  toFun := toCompletedGroupAlgebra R G
  map_add' := by
    intro x y
    exact map_add (toCompletedGroupAlgebraRingHom R G) x y
  map_smul' := toCompletedGroupAlgebra_smul (R := R) (G := G)

theorem

completedGroupAlgebraProjection_comp_toCompletedGroupAlgebra

L640 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjection_comp_toCompletedGroupAlgebra

Documentation

Composing the \(U\)-coordinate projection from the all-finite completion with its canonical dense ring homomorphism gives the all-finite stage map at \(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 completedGroupAlgebraProjection_comp_toCompletedGroupAlgebra
    (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraProjection R G U).comp
        (toCompletedGroupAlgebraRingHom R G) =
      completedGroupAlgebraStageMap R G U

Module documentation

Completed Group Algebra / Open Finite Quotient Topology / Canonical Maps

Declarations