NYLL
Module

CompletionMap.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — completion map

The principal declarations in this module are:

  • toModNCompletedGroupAlgebra

The canonical map \((\mathbb{Z}/n\mathbb{Z})[G] \to \varprojlim_U (\mathbb{Z}/n\mathbb{Z})[G/U]\).

  • modNCompletedGroupAlgebraStageMap_compatibleMaps

The mod-\(n\) completed group-algebra stage maps are compatible with transition maps and coordinate projections.

  • modNCompletedGroupAlgebraProjection_toCompleted

The finite-stage projection to the completed mod-\(n\) group algebra is given by the corresponding coordinate formula.

Imports1
Imported by4

Declarations

theorem

modNCompletedGroupAlgebraStageMap_compatibleMaps

L42 ↗
FoxDifferential.modNCompletedGroupAlgebraStageMap_compatibleMaps
Documentation

The mod-\(n\) completed group-algebra stage maps are compatible with transition maps and coordinate projections.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · full declaration
theorem modNCompletedGroupAlgebraStageMap_compatibleMaps :
    (modNCompletedGroupAlgebraSystem n G).CompatibleMaps
      (fun U => modNCompletedGroupAlgebraStageMap n G U) := by
  intro U V hUV
  funext x
  exact congrFun
    (congrArg DFunLike.coe
      (modNCompletedGroupAlgebraStageMap_compatible (n := n) (G := G) (U := U) (V := V) hUV))
    x
def

toModNCompletedGroupAlgebra

L56 ↗
FoxDifferential.toModNCompletedGroupAlgebra
Documentation

The canonical map \((\mathbb{Z}/n\mathbb{Z})[G] \to \varprojlim_U (\mathbb{Z}/n\mathbb{Z})[G/U]\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def toModNCompletedGroupAlgebra :
    ModNCompletedGroupRing n G → ModNCompletedGroupAlgebra n G
theorem

modNCompletedGroupAlgebraProjection_toCompleted

L70 ↗
FoxDifferential.modNCompletedGroupAlgebraProjection_toCompleted
Documentation

The finite-stage projection to the completed mod-\(n\) group algebra is given by the corresponding coordinate formula.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjection_toCompleted
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x : ModNCompletedGroupRing
        n G) :
    modNCompletedGroupAlgebraProjection n G U (toModNCompletedGroupAlgebra n G x) =
      modNCompletedGroupAlgebraStageMap n G U x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.