FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic
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.
import
abbrev ModNCompletedGroupAlgebraStage (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) : Type _ :=
ModNCompletedGroupRing n (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coefficient quotient modulo \(N\).
instance instFiniteModNCompletedGroupAlgebraStage (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
Finite (ModNCompletedGroupAlgebraStage n G U) := by
classical
letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) := (OrderDual.ofDual U).2
letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) := Fintype.ofFinite _
letI : DecidableEq (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) := Classical.decEq _
letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U → ModNCompletedCoeff n) := by
letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U → ModNCompletedCoeff n) := inferInstance
exact Finite.of_fintype _
let f :
ModNCompletedGroupAlgebraStage n G U →
_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U → ModNCompletedCoeff n := fun x q => x q
refine Finite.of_injective f ?_
intro x y hxy
ext q
exact congrFun hxy qEach mod-\(n\) completed group-algebra stage is finite.
def modNCompletedGroupAlgebraTransition
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
ModNCompletedGroupAlgebraStage n G V →+* ModNCompletedGroupAlgebraStage n G U :=
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
(OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)Transition maps compose compatibly along refinements of finite quotients.
theorem modNCompletedGroupAlgebraTransition_of
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
(g : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V) :
modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.
Show proof
by
classical
simp only [modNCompletedGroupAlgebraTransition, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
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.
□theorem modNCompletedGroupAlgebraTransition_id (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
modNCompletedGroupAlgebraTransition n G (le_rfl : U ≤ U) = RingHom.id _The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.
Show proof
by
rw [modNCompletedGroupAlgebraTransition, OpenNormalSubgroupInClass.map_id]
exact MonoidAlgebra.mapDomainRingHom_id
(R := ModNCompletedCoeff n) (M := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)Proof. 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.
□theorem modNCompletedGroupAlgebraTransition_comp
{U V W : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤ W) :
(modNCompletedGroupAlgebraTransition n G hUV).comp
(modNCompletedGroupAlgebraTransition n G hVW) =
modNCompletedGroupAlgebraTransition n G (hUV.trans hVW)The finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [modNCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraTransition,
modNCompletedGroupAlgebraTransition, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1
exact OpenNormalSubgroupInClass.map_comp
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
hUV hVWProof. 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.
□theorem modNCompletedGroupAlgebraTransition_single_apply
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
(q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)
(a : ModNCompletedCoeff n) :
modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.single q a) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) aThe \(n\)-modular completed group-algebra transition sends a singleton to the singleton supported at the induced quotient class with the same coefficient.
Show proof
by
simp only [modNCompletedGroupAlgebraTransition, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
Finsupp.mapDomain_single]
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.
□theorem modNCompletedGroupAlgebraTransition_surjective
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
Function.Surjective (modNCompletedGroupAlgebraTransition n G hUV)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
by
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero _⟩
| single_add q a x _ _ ih =>
rcases OpenNormalSubgroupInClass.map_surjective
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV q with
⟨q', hq'⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single q' a : ModNCompletedGroupAlgebraStage n G V) + y, ?_⟩
rw [map_add, modNCompletedGroupAlgebraTransition_single_apply, hy, hq']Proof. 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 modNCompletedGroupAlgebraStageMap (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStage n G U :=
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\).
theorem modNCompletedGroupAlgebraStageMap_of
(U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (g : G) :
modNCompletedGroupAlgebraStageMap n G U (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
MonoidAlgebra.single (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1The finite-stage group-like map sends a group element to the corresponding singleton basis element in the quotient group algebra in the Fox differential construction.
Show proof
by
classical
simp only [modNCompletedGroupAlgebraStageMap, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
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.
□theorem modNCompletedGroupAlgebraStageMap_compatible
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
(modNCompletedGroupAlgebraTransition n G hUV).comp
(modNCompletedGroupAlgebraStageMap n G V) =
modNCompletedGroupAlgebraStageMap n G UThe mod-\(n\) completed group-algebra stage maps are compatible with quotient refinement.
Show proof
by
rw [modNCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageMap,
modNCompletedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1Proof. Unfold the mod-\(n\) completed group-algebra stage map. Refinement of finite quotients gives the same quotient support map, and the coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) is unchanged, so the two transition composites agree on basis elements and hence by linearity.
□def modNCompletedGroupAlgebraSystem :
InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
X := ModNCompletedGroupAlgebraStage n G
topologicalSpace := fun _ => ⊥
map := fun {U V} hUV => modNCompletedGroupAlgebraTransition n G hUV
continuous_map := by
intro U V hUV
letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G U) := ⊥
letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G V) := ⊥
letI : DiscreteTopology (ModNCompletedGroupAlgebraStage n G V) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro U
funext x
exact congrFun
(congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U)) x
map_comp := by
intro U V W hUV hVW
funext x
exact congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW)) xThe inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\).
abbrev ModNCompletedGroupAlgebra :=
(modNCompletedGroupAlgebraSystem n G).inverseLimitThe inverse-limit object of the residue-coefficient stage tower.
abbrev modNCompletedGroupAlgebraProjection (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
ModNCompletedGroupAlgebra n G → ModNCompletedGroupAlgebraStage n G U :=
(modNCompletedGroupAlgebraSystem n G).projection U