FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite
- FoxDifferential.Completed.Residue.Core
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 proof
by
intro U V hUV
funext x
exact congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraStageMap_compatible (n := n) (G := G) (U := U) (V := V) hUV))
xProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□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 modNCompletedGroupAlgebraProjection_toCompleted
(U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x : ModNCompletedGroupRing n G) :
modNCompletedGroupAlgebraProjection n G U (toModNCompletedGroupAlgebra n G x) =
modNCompletedGroupAlgebraStageMap n G U xThe finite-stage projection to the completed mod-\(n\) group algebra is given by the corresponding coordinate formula.
Show proof
by
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□