ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

2 Theorems | 1 Definition

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.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup

Imported by

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMap_compatibleMaps

omit [Fact (0 < n)] in
theorem modNCompletedGroupAlgebraStageMap_compatibleMaps :
    (modNCompletedGroupAlgebraSystem n G).CompatibleMaps
      (fun U => modNCompletedGroupAlgebraStageMap n G U)

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

Show Lean proof

Definition FoxDifferential.toModNCompletedGroupAlgebra

def toModNCompletedGroupAlgebra :
    ModNCompletedGroupRing n G → ModNCompletedGroupAlgebra n G := by
  letI : TopologicalSpace (ModNCompletedGroupRing n G) := ⊥
  exact
    (modNCompletedGroupAlgebraSystem n G).inverseLimitLift
      (fun U => modNCompletedGroupAlgebraStageMap n G U)
      (modNCompletedGroupAlgebraStageMap_compatibleMaps (n := n) (G := G))

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

Theorem FoxDifferential.modNCompletedGroupAlgebraProjection_toCompleted

omit [Fact (0 < n)] in
@[simp]
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

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

Declarations