FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Module.
theorem primePowerCompletedGroupAlgebraTransition_algebraMap
{i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
(a : ZMod (ℓ ^ j.1)) :
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j) a) =
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1) a)Finite-stage transitions send scalar coefficients through the reduced coefficient algebra map.
Show proof
by
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
classical
rw [primePowerCompletedGroupAlgebraTransition_eq']
simp only [modNCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMap,
modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, map_intCast]Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraStageAugmentation_algebraMap
(i : PrimePowerCompletedGroupAlgebraIndex G) (a : ZMod (ℓ ^ i.1)) :
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
(algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i) a) = aThe finite-stage prime-power augmentation agrees with the scalar algebra map on coefficients.
Show proof
by
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
classical
simp only [modNCompletedGroupAlgebraStageAugmentation, map_intCast]Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□def primePowerCompletedCoeffToGroupAlgebra :
PrimePowerCompletedCoeff ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ G where
toFun a := ⟨fun i =>
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) =
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
rw [primePowerCompletedGroupAlgebraTransition_algebraMap]
exact congrArg
(algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
(a.2 i j hij)⟩
map_one' := by
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (1 : PrimePowerCompletedCoeff ℓ G))
= 1
rw [primePowerCompletedCoeffProjection_one]
exact map_one (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
map_mul' := by
intro a b
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) =
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) *
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
rw [primePowerCompletedCoeffProjection_mul]
exact
map_mul
(algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
map_zero' := by
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (0 : PrimePowerCompletedCoeff ℓ G))
= 0
rw [primePowerCompletedCoeffProjection_zero]
exact map_zero (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
map_add' := by
intro a b
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) =
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) +
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
rw [primePowerCompletedCoeffProjection_add]
exact
map_add
(algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)The coefficient inverse limit maps canonically into the completed group algebra by taking the stagewise scalar units.
theorem primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra
(i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a) =
algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)The prime-power completed group-algebra projection on coefficients is computed by the corresponding group-algebra coordinate map.
Show proof
by
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraTransition_smul
{i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
(a : ZMod (ℓ ^ j.1))
(x : PrimePowerCompletedGroupAlgebraStage ℓ G j) :
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (a • x) =
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij xFinite-stage transitions commute with scalar multiplication after reducing the scalar coefficient.
Show proof
by
rw [Algebra.smul_def, map_mul, primePowerCompletedGroupAlgebraTransition_algebraMap]
rw [← Algebra.smul_def]Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□instance instCommRingPrimePowerCompletedCoeffGroupAlgebraLocal :
CommRing (PrimePowerCompletedCoeff ℓ G) := by
infer_instanceThe completed group algebra has powers computed at every finite-stage coordinate.
instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily :
SMul (PrimePowerCompletedCoeff ℓ G)
((i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
smul a x := fun i =>
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
instance instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily :
Module (PrimePowerCompletedCoeff ℓ G)
((i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
one_smul x := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
(1 : PrimePowerCompletedCoeff ℓ G)) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
rw [primePowerCompletedCoeffProjection_one, one_smul]
mul_smul a b x := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i))
rw [primePowerCompletedCoeffProjection_mul, mul_smul]
smul_zero a := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
rw [smul_zero]
smul_add a x y := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
((show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)) =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)
rw [smul_add]
add_smul a b x := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
rw [primePowerCompletedCoeffProjection_add, add_smul]
zero_smul x := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
(0 : PrimePowerCompletedCoeff ℓ G)) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) = 0
rw [primePowerCompletedCoeffProjection_zero, zero_smul]The prime-power completed group-algebra family is a module over the prime-power completed coefficient ring.
instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra :
SMul (PrimePowerCompletedCoeff ℓ G)
(PrimePowerCompletedGroupAlgebra ℓ G) where
smul a x := ⟨fun i =>
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
intro i j hij
calc
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) := by
simpa using
primePowerCompletedGroupAlgebraTransition_smul
(ℓ := ℓ) (G := G) hij
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)
_ =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) := by
exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
theorem coe_smul_primePowerCompletedGroupAlgebra
(a : PrimePowerCompletedCoeff ℓ G)
(x : PrimePowerCompletedGroupAlgebra ℓ G) :
letIThe inclusion of the prime-power completed group algebra preserves scalar multiplication.
Show proof
instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra
(ℓ := ℓ) (G := G)
((a • x : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
a • (x :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
funext i
change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_smul
(i : PrimePowerCompletedGroupAlgebraIndex G)
(a : PrimePowerCompletedCoeff ℓ G)
(x : PrimePowerCompletedGroupAlgebra ℓ G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x) =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i xThe finite-stage projection is compatible with scalar multiplication.
Show proof
by
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□instance instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra :
Module (PrimePowerCompletedCoeff ℓ G)
(PrimePowerCompletedGroupAlgebra ℓ G) :=
Function.Injective.module (PrimePowerCompletedCoeff ℓ G)
{ toFun := Subtype.val
map_zero' := rfl
map_add' := fun _ _ => rfl }
Subtype.val_injective
(coe_smul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))The prime-power completed group algebra is a module over the prime-power completed coefficient ring.
theorem primePowerCompletedGroupAlgebraAugmentation_coeffToGroupAlgebra
(i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
(primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a)) =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i aThe prime-power completed augmentation is left inverse to the coefficient-to-group-algebra map.
Show proof
by
rw [primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra]
exact primePowerCompletedGroupAlgebraStageAugmentation_algebraMap (ℓ := ℓ) (G := G) i
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□