FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Within a Class / Augmentation.
def primePowerCompletedCoeffSystemInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
X := fun i => ModNCompletedCoeff (ℓ ^ i.1)
topologicalSpace := fun _ => ⊥
map := fun {i j} hij =>
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
continuous_map := by
intro i j hij
letI : TopologicalSpace (ModNCompletedCoeff (ℓ ^ i.1)) := ⊥
letI : TopologicalSpace (ModNCompletedCoeff (ℓ ^ j.1)) := ⊥
letI : DiscreteTopology (ModNCompletedCoeff (ℓ ^ j.1)) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro i
funext x
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
exact congrFun
(congrArg DFunLike.coe
(modNCompletedCoeffMap_rfl (n := ℓ ^ i.1))) x
map_comp := by
intro i j k hij hjk
funext x
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
letI : Fact (0 < ℓ ^ k.1) := ⟨primePower_pos ℓ k.1⟩
exact congrFun
(congrArg DFunLike.coe
(modNCompletedCoeffMap_comp
(n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
(primePow_dvd_primePow (ℓ := ℓ) hjk.1))) xThe class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coefficient stage is \(\mathrm{ZMod}\,(\ell^a)\).
def PrimePowerCompletedCoeffCompatibleInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
ModNCompletedCoeff (ℓ ^ i.1)) : Prop :=
(primePowerCompletedCoeffSystemInClass ℓ G C).Compatible xCompatibility for the class-indexed coefficient tower; the finite quotient component is retained only to match the surrounding pro-\(C\) index shape.
abbrev PrimePowerCompletedCoeffInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
{x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
ModNCompletedCoeff (ℓ ^ i.1) //
PrimePowerCompletedCoeffCompatibleInClass (ℓ := ℓ) (G := G) C x}The pro-\(C\)-indexed prime-power completed coefficient inverse limit.
def primePowerCompletedCoeffProjectionInClass
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
PrimePowerCompletedCoeffInClass ℓ G C → ModNCompletedCoeff (ℓ ^ i.1) :=
(primePowerCompletedCoeffSystemInClass ℓ G C).projection iinstance instZeroPrimePowerCompletedCoeffInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Zero (PrimePowerCompletedCoeffInClass ℓ G C) where
zero := ⟨fun _ => 0, by
dsimp [PrimePowerCompletedCoeffCompatibleInClass]
intro i j hij
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
exact map_zero
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩The zero element of the class-indexed prime-power completed coefficient ring is the compatible family of finite-stage zero elements.
instance instAddPrimePowerCompletedCoeffInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Add (PrimePowerCompletedCoeffInClass ℓ G C) where
add x y := ⟨fun i =>
(show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
dsimp [PrimePowerCompletedCoeffCompatibleInClass]
intro i j hij
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
change modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
(show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
rw [map_add]
exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.
instance instNegPrimePowerCompletedCoeffInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Neg (PrimePowerCompletedCoeffInClass ℓ G C) where
neg x := ⟨fun i => -(show ZMod (ℓ ^ i.1) from x.1 i), by
dsimp [PrimePowerCompletedCoeffCompatibleInClass]
intro i j hij
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
change modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
(-(show ZMod (ℓ ^ j.1) from x.1 j)) =
-(show ZMod (ℓ ^ i.1) from x.1 i)
rw [map_neg]
exact congrArg Neg.neg (x.2 i j hij)⟩Negation on the class-indexed prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient negations.
instance instSubPrimePowerCompletedCoeffInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Sub (PrimePowerCompletedCoeffInClass ℓ G C) where
sub x y := ⟨fun i =>
(show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
dsimp [PrimePowerCompletedCoeffCompatibleInClass]
intro i j hij
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
change modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
(show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
rw [map_sub]
exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩Subtraction in the class-indexed prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient-ring subtractions.
theorem primePowerCompletedCoeffProjectionInClass_zero
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
(0 : PrimePowerCompletedCoeffInClass ℓ G C) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
by
rflProof. Unfold the class-indexed prime-power completed coefficient ring as the inverse limit over the finite prime-power coefficient stages, with the finite quotient component retained only to match the class-restricted indexing. The coefficient projections, transition maps, additive operations, and zero element are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem primePowerCompletedCoeffProjectionInClass_add
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x y : PrimePowerCompletedCoeffInClass ℓ G C) :
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x +
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i yThe finite-stage projection evaluates a completed element by reading the corresponding inverse-limit coordinate.
Show proof
by
rflProof. Unfold the class-indexed prime-power completed coefficient ring as the inverse limit over the finite prime-power coefficient stages, with the finite quotient component retained only to match the class-restricted indexing. The coefficient projections, transition maps, additive operations, and zero element are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem primePowerCompletedCoeffProjectionInClass_neg
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x : PrimePowerCompletedCoeffInClass ℓ G C) :
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
-primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i xThe finite-stage projection evaluates a completed element by reading the corresponding inverse-limit coordinate.
Show proof
by
rflProof. Unfold the class-indexed prime-power completed coefficient ring as the inverse limit over the finite prime-power coefficient stages, with the finite quotient component retained only to match the class-restricted indexing. The coefficient projections, transition maps, additive operations, and zero element are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem primePowerCompletedCoeffProjectionInClass_sub
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x y : PrimePowerCompletedCoeffInClass ℓ G C) :
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x -
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i yThe finite-stage projection evaluates a completed element by reading the corresponding inverse-limit coordinate.
Show proof
by
rflProof. Unfold the class-indexed prime-power completed coefficient ring as the inverse limit over the finite prime-power coefficient stages, with the finite quotient component retained only to match the class-restricted indexing. The coefficient projections, transition maps, additive operations, and zero element are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□def primePowerCompletedGroupAlgebraAugmentationInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
PrimePowerCompletedGroupAlgebraInClass ℓ G C →
PrimePowerCompletedCoeffInClass ℓ G C := by
intro x
refine ⟨fun i => ?_, ?_⟩
· letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
exact modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2 (x.1 i)
· dsimp [PrimePowerCompletedCoeffCompatibleInClass]
intro i j hij
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
calc
modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)
(modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2 (x.1 j))
=
modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
(primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij (x.1 j)) := by
symm
exact congrFun
(congrArg DFunLike.coe
(primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition
(ℓ := ℓ) (G := G) C hij)) (x.1 j)
_ =
modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2 (x.1 i) := by
have hx :
primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(x.1 j) = x.1 i :=
x.2 i j hij
exact congrArg
(modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2) hxThe class-restricted prime-power completed group algebra carries a canonical augmentation to the pro-\(C\)-indexed coefficient limit.
theorem primePowerCompletedCoeffProjectionInClass_augmentation
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
(primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C x) =
modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
(primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x)Projecting the class-indexed prime-power completed augmentation to a coefficient stage agrees with the corresponding finite-stage augmentation.
Show proof
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 primePowerCompletedGroupAlgebraAugmentationInClass_surjective
(C : ProCGroups.FiniteGroupClass.{u}) :
Function.Surjective
(primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C)The class-indexed completed group-algebra augmentation has a canonical section, obtained by placing each compatible coefficient system on the identity monomial at every finite stage.
Show proof
by
intro x
refine ⟨⟨fun i => ?_, ?_⟩, ?_⟩
· exact MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)
· intro i j hij
change
primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass G C j.2) (x.1 j)) =
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)
rw [primePowerCompletedGroupAlgebraTransitionInClass_single]
have hxcoeff :
modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1) (x.1 j) = x.1 i := by
simpa [primePowerCompletedCoeffSystemInClass] using x.2 i j hij
simpa using congrArg
(fun a : ModNCompletedCoeff (ℓ ^ i.1) =>
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass G C i.2) a)
hxcoeff
· apply Subtype.ext
funext i
change
modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)) =
x.1 i
simp only [modNCompletedGroupAlgebraStageAugmentationInClass_single]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.
□