FoxDifferential.Completed.ProCIntegerCoefficients.Core
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
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection
- FoxDifferential.Completed.ProCIntegerCoefficients
- FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
- FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Derivative
- FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
- FoxDifferential.Completed.Semidirect
- Yama2026_Sections_1_And_2_1.main
abbrev ZCCoeff (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
ProCIntegerLimitCarrier CThe pro-\(C\) integer coefficient ring.
abbrev ZCCompletedGroupAlgebraIndex
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] : Type u :=
ProCIntegerIndex C × CompletedGroupAlgebraIndexInClass H Cabbrev ZCCompletedGroupAlgebraStage
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) : Type u :=
ModNCompletedGroupAlgebraStageInClass i.1.modulus H C i.2A finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) of the pro-\(C\) completed group algebra.
def zcCompletedGroupAlgebraTransition
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j) :
ZCCompletedGroupAlgebraStage C H j →+* ZCCompletedGroupAlgebraStage C H i := by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
exact
(modNCompletedGroupAlgebraStageCoeffMapInClass
(n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1).comp
(modNCompletedGroupAlgebraTransitionInClass (n := j.1.modulus) (G := H) C hij.2)Transition maps for the true pro-\(C\) completed group algebra. The coefficient direction is divisibility of allowed pro-\(C\) integer moduli, and the group direction is refinement of \(C\)-quotients.
theorem zcCompletedGroupAlgebraTransition_of
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
(q : CompletedGroupAlgebraQuotientInClass H C j.2) :
zcCompletedGroupAlgebraTransition C H hij
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus) _ q) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)Evaluation of a pro-\(C\) transition on a group-like basis element.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
modNCompletedGroupAlgebraTransitionInClass_of]
simpa using
(modNCompletedGroupAlgebraStageCoeffMapInClass_of
(n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q))Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraTransition_single
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
(q : CompletedGroupAlgebraQuotientInClass H C j.2)
(a : ModNCompletedCoeff j.1.modulus) :
zcCompletedGroupAlgebraTransition C H hij (MonoidAlgebra.single q a) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
(modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a)The transition map \(R[G/V] \to R[G/U]\) sends a singleton supported at a class of \(G/V\) to the singleton supported at its image in \(G/U\), with the same coefficient.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
modNCompletedGroupAlgebraTransitionInClass_single,
modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraTransition_id
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) :
zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) = RingHom.id _Transition maps compose compatibly along refinements of finite quotients.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
rw [zcCompletedGroupAlgebraTransition]
rw [modNCompletedGroupAlgebraTransitionInClass_id,
modNCompletedGroupAlgebraStageCoeffMapInClass_rfl]
simp only [RingHomCompTriple.comp_eq]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraTransition_comp
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{i j k : ZCCompletedGroupAlgebraIndex C H}
(hij : i ≤ j) (hjk : j ≤ k) :
(zcCompletedGroupAlgebraTransition C H hij).comp
(zcCompletedGroupAlgebraTransition C H hjk) =
zcCompletedGroupAlgebraTransition C H (hij.trans hjk)Transition maps compose compatibly along refinements of finite quotients.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
letI : Fact (0 < k.1.modulus) := ⟨k.1.positive⟩
apply RingHom.ext
intro x
refine MonoidAlgebra.induction_on
(p := fun x =>
((zcCompletedGroupAlgebraTransition C H hij).comp
(zcCompletedGroupAlgebraTransition C H hjk)) x =
zcCompletedGroupAlgebraTransition C H (hij.trans hjk) x)
x ?_ ?_ ?_
· intro q
rw [RingHom.comp_apply, zcCompletedGroupAlgebraTransition_of C H hjk,
zcCompletedGroupAlgebraTransition_of C H (hij.trans hjk)]
change
zcCompletedGroupAlgebraTransition C H hij
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C j.2)
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual j.2) (V := OrderDual.ofDual k.2) hjk.2) q)) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2)
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual k.2) (hij.2.trans hjk.2)) q)
rw [zcCompletedGroupAlgebraTransition_of C H hij]
congr 1
exact congrFun
(congrArg DFunLike.coe
(OpenNormalSubgroupInClass.map_comp
(C := C) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2)
(W := OrderDual.ofDual k.2) hij.2 hjk.2)) q
· intro x y hx hy
simp only [RingHom.map_add, hx, hy]
· intro a x hx
rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
have hcoeff :
((zcCompletedGroupAlgebraTransition C H hij).comp
(zcCompletedGroupAlgebraTransition C H hjk))
(algebraMap (ModNCompletedCoeff k.1.modulus)
(ZCCompletedGroupAlgebraStage C H k) a) =
zcCompletedGroupAlgebraTransition C H (hij.trans hjk)
(algebraMap (ModNCompletedCoeff k.1.modulus)
(ZCCompletedGroupAlgebraStage C H k) a) := by
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
simp only [zcCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass,
modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, modNCompletedGroupAlgebraTransitionInClass, map_intCast]
rw [hcoeff]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□def zcCompletedGroupAlgebraSystem
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
X := ZCCompletedGroupAlgebraStage C H
topologicalSpace := fun _ => ⊥
map := fun {i j} hij => zcCompletedGroupAlgebraTransition C H hij
continuous_map := by
intro i j hij
letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H i) := ⊥
letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H j) := ⊥
letI : DiscreteTopology (ZCCompletedGroupAlgebraStage C H j) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro i
funext x
exact congrFun
(congrArg DFunLike.coe
(zcCompletedGroupAlgebraTransition_id C H i)) x
map_comp := by
intro i j k hij hjk
funext x
exact congrFun
(congrArg DFunLike.coe
(zcCompletedGroupAlgebraTransition_comp C H hij hjk)) xThe inverse system defining the pro-\(C\) completed group algebra.
def ZCCompletedGroupAlgebraCompatible
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i) : Prop :=
∀ i j, ∀ hij : i ≤ j, zcCompletedGroupAlgebraTransition C H hij (x j) = x iCompatibility for a family of finite \(\mathbb{Z}_C\llbracket H\rrbracket\) stage elements.
abbrev ZCCompletedGroupAlgebra
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] : Type u :=
{x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i //
ZCCompletedGroupAlgebraCompatible C H x}The completed group algebra \(\mathbb{Z}_C\llbracket H\rrbracket\).
abbrev zcCompletedGroupAlgebraProjection
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) :
ZCCompletedGroupAlgebra C H → ZCCompletedGroupAlgebraStage C H i :=
fun x => x.1 iThe projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite \(C\)-coefficient and \(C\)-quotient stage.
instance instZeroZCCompletedGroupAlgebra : Zero (ZCCompletedGroupAlgebra C H) where
zero := ⟨fun i => 0, by intro i j hij; exact map_zero _⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddZCCompletedGroupAlgebra : Add (ZCCompletedGroupAlgebra C H) where
add x y := ⟨fun i => x.1 i + y.1 i, by
intro i j hij
rw [map_add]
exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩Addition on \(\mathbb{Z}_C\llbracket H\rrbracket\) is defined coordinatewise through finite-stage group-algebra additions.
instance instNegZCCompletedGroupAlgebra : Neg (ZCCompletedGroupAlgebra C H) where
neg x := ⟨fun i => -x.1 i, by
intro i j hij
rw [map_neg]
exact congrArg Neg.neg (x.2 i j hij)⟩Negation on the \(\mathbb{Z}_C\)-completed group algebra is defined coordinatewise through finite-stage group-algebra negations.
instance instSubZCCompletedGroupAlgebra : Sub (ZCCompletedGroupAlgebra C H) where
sub x y := ⟨fun i => x.1 i - y.1 i, by
intro i j hij
rw [map_sub]
exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.
instance instSMulNatZCCompletedGroupAlgebra : SMul ℕ (ZCCompletedGroupAlgebra C H) where
smul n x := ⟨fun i => n • x.1 i, by
intro i j hij
rw [map_nsmul]
exact congrArg (n • ·) (x.2 i j hij)⟩The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
instance instSMulIntZCCompletedGroupAlgebra : SMul ℤ (ZCCompletedGroupAlgebra C H) where
smul n x := ⟨fun i => n • x.1 i, by
intro i j hij
rw [map_zsmul]
exact congrArg (n • ·) (x.2 i j hij)⟩
@[simp]The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
theorem coe_zero_zcCompletedGroupAlgebra :
((0 : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 0The zero element of \(\mathbb{Z}_C\llbracket H\rrbracket\) is represented by the compatible family of finite-stage zero elements.
Show proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_add_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
((x + y : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x + yShow proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_neg_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) :
((-x : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = -xShow proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_sub_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
((x - y : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x - yShow proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_nsmul_zcCompletedGroupAlgebra (n : ℕ) (x : ZCCompletedGroupAlgebra C H) :
((n • x : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • xNatural-number scalar multiplication in \(\mathbb{Z}_C\llbracket H\rrbracket\) is computed coordinatewise at every finite stage.
Show proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_zsmul_zcCompletedGroupAlgebra (n : ℤ) (x : ZCCompletedGroupAlgebra C H) :
((n • x : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • xInteger scalar multiplication in \(\mathbb{Z}_C\llbracket H\rrbracket\) is computed coordinatewise at every finite stage.
Show proof
by
funext i
rflProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□instance instAddCommGroupZCCompletedGroupAlgebra : AddCommGroup (ZCCompletedGroupAlgebra C H) :=
Function.Injective.addCommGroup
(fun x : ZCCompletedGroupAlgebra C H =>
(x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
Subtype.val_injective
(coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
(fun x n => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
(fun x n => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)Addition on \(\mathbb{Z}_C\llbracket H\rrbracket\) is defined coordinatewise through finite-stage group-algebra additions.
instance instOneZCCompletedGroupAlgebra : One (ZCCompletedGroupAlgebra C H) where
one := ⟨fun i => 1, by intro i j hij; exact map_one _⟩The unit of \(\mathbb{Z}_C\llbracket H\rrbracket\) is the compatible family of finite-stage units.
instance instMulZCCompletedGroupAlgebra : Mul (ZCCompletedGroupAlgebra C H) where
mul x y := ⟨fun i => x.1 i * y.1 i, by
intro i j hij
rw [map_mul]
exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.
instance instNatCastZCCompletedGroupAlgebra : NatCast (ZCCompletedGroupAlgebra C H) where
natCast n := ⟨fun i => n, by intro i j hij; exact map_natCast _ _⟩Natural number casts in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise from finite-stage natural number casts.
instance instIntCastZCCompletedGroupAlgebra : IntCast (ZCCompletedGroupAlgebra C H) where
intCast n := ⟨fun i => n, by intro i j hij; exact map_intCast _ _⟩Integer casts in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise from finite-stage integer casts.
instance instPowZCCompletedGroupAlgebra : Pow (ZCCompletedGroupAlgebra C H) ℕ where
pow x n := ⟨fun i => x.1 i ^ n, by
intro i j hij
rw [map_pow]
exact congrArg (fun z => z ^ n) (x.2 i j hij)⟩
@[simp]The completed group algebra has powers computed at every finite-stage coordinate.
theorem coe_one_zcCompletedGroupAlgebra :
((1 : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 1The unit of \(\mathbb{Z}_C\llbracket H\rrbracket\) is represented by the compatible family of finite-stage units.
Show proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_mul_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
((x * y : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x * yShow proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_natCast_zcCompletedGroupAlgebra (n : ℕ) :
((n : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = nNatural number casts in the completed group algebra are computed coefficientwise after projection to every completed finite quotient stage.
Show proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_intCast_zcCompletedGroupAlgebra (n : ℤ) :
((n : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = nInteger casts in the completed group algebra are computed coefficientwise after projection to every completed finite quotient stage.
Show proof
by
funext i
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem coe_pow_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) (n : ℕ) :
((x ^ n : ZCCompletedGroupAlgebra C H) :
(i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x ^ nPowers in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise at every finite stage.
Show proof
by
funext i
rflProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□instance instRingZCCompletedGroupAlgebra : Ring (ZCCompletedGroupAlgebra C H) :=
Function.Injective.ring
(fun x : ZCCompletedGroupAlgebra C H =>
(x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
Subtype.val_injective
(coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_one_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_mul_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
(coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
(fun n x => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
(fun n x => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
(fun x n => coe_pow_zcCompletedGroupAlgebra (C := C) (H := H) x n)
(by intro n; exact coe_natCast_zcCompletedGroupAlgebra (C := C) (H := H) n)
(by intro z; exact coe_intCast_zcCompletedGroupAlgebra (C := C) (H := H) z)
@[simp]The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
theorem zcCompletedGroupAlgebraProjection_one
(i : ZCCompletedGroupAlgebraIndex C H) :
zcCompletedGroupAlgebraProjection C H i (1 : ZCCompletedGroupAlgebra C H) = 1The finite-stage projection sends \(1\) to \(1\).
Show proof
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_mul
(i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjection C H i (x * y) =
zcCompletedGroupAlgebraProjection C H i x *
zcCompletedGroupAlgebraProjection C H i yThe finite-stage projection preserves multiplication.
Show proof
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_zero
(i : ZCCompletedGroupAlgebraIndex C H) :
zcCompletedGroupAlgebraProjection C H i (0 : ZCCompletedGroupAlgebra C H) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_add
(i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjection C H i (x + y) =
zcCompletedGroupAlgebraProjection C H i x +
zcCompletedGroupAlgebraProjection C H i yThe finite-stage projection preserves addition.
Show proof
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_neg
(i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjection C H i (-x) =
-zcCompletedGroupAlgebraProjection C H i xThe finite-stage projection preserves negation.
Show proof
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_sub
(i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjection C H i (x - y) =
zcCompletedGroupAlgebraProjection C H i x -
zcCompletedGroupAlgebraProjection C H i yThe finite-stage projection preserves subtraction.
Show proof
rflProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□def zcCompletedGroupAlgebraProjectionRingHom
(i : ZCCompletedGroupAlgebraIndex C H) :
ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebraStage C H i where
toFun := zcCompletedGroupAlgebraProjection C H i
map_zero' := zcCompletedGroupAlgebraProjection_zero C H i
map_one' := zcCompletedGroupAlgebraProjection_one C H i
map_add' := zcCompletedGroupAlgebraProjection_add C H i
map_mul' := zcCompletedGroupAlgebraProjection_mul C H i
@[simp]The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite stage is bundled as a ring homomorphism.
theorem zcCompletedGroupAlgebraProjectionRingHom_apply
(i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjectionRingHom C H i x =
zcCompletedGroupAlgebraProjection C H i xThe ring-homomorphism projection has the same underlying coordinate map as the finite-stage projection.
Show proof
rflProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□instance instModuleZCCompletedGroupAlgebraStage
(i : ZCCompletedGroupAlgebraIndex C H) :
Module (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebraStage C H i) :=
Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i)The \(\mathbb{Z}_C\)-completed group algebra stage is a module over its coefficient ring.
theorem zcCompletedGroupAlgebraProjection_ext
{x y : ZCCompletedGroupAlgebra C H}
(h : ∀ i : ZCCompletedGroupAlgebraIndex C H,
zcCompletedGroupAlgebraProjection C H i x =
zcCompletedGroupAlgebraProjection C H i y) :
x = yFinite-stage projections separate points of \(\mathbb{Z}_C\llbracket H\rrbracket\).
Show proof
by
apply Subtype.ext
funext i
exact h iProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraTransition_projection
{i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
(x : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraTransition C H hij
(zcCompletedGroupAlgebraProjection C H j x) =
zcCompletedGroupAlgebraProjection C H i xFinite projections from \(\mathbb{Z}_C\llbracket H\rrbracket\) commute with the finite transition maps.
Show proof
x.2 i j hijProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□def zcCompletedGroupAlgebraProjectionLinearMap
(i : ZCCompletedGroupAlgebraIndex C H) :
ZCCompletedGroupAlgebra C H →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedGroupAlgebraStage C H i where
toFun := zcCompletedGroupAlgebraProjection C H i
map_add' x y := zcCompletedGroupAlgebraProjection_add C H i x y
map_smul' r x := by
change zcCompletedGroupAlgebraProjection C H i (r * x) =
zcCompletedGroupAlgebraProjection C H i r *
zcCompletedGroupAlgebraProjection C H i x
exact zcCompletedGroupAlgebraProjection_mul C H i r x
@[simp]A finite stage projection as a linear map over the completed group algebra.
theorem zcCompletedGroupAlgebraProjectionLinearMap_apply
(i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjectionLinearMap C H i x =
zcCompletedGroupAlgebraProjection C H i xThe \(\mathbb{Z}_C\)-completed group-algebra projection, bundled as a linear map, acts by its defining finite-stage coordinate formula.
Show proof
rflProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_sum
(C : ProCGroups.FiniteGroupClass.{u})
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{I : Type v} [Fintype I]
(j : ZCCompletedGroupAlgebraIndex C H)
(f : I → ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjection C H j (∑ i : I, f i) =
∑ i : I, zcCompletedGroupAlgebraProjection C H j (f i)Show proof
by
classical
refine Finset.induction_on (s := Finset.univ) ?_ ?_
· rfl
· intro a s has ih
rw [Finset.sum_insert has, Finset.sum_insert has]
rw [zcCompletedGroupAlgebraProjection_add, ih]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□def zcCompletedGroupAlgebraCoeff
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(a : ZCCoeff C) : ZCCompletedGroupAlgebra C H :=
⟨fun i =>
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a), by
intro i j hij
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
change zcCompletedGroupAlgebraTransition C H hij
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C j.2)
(proCIntegerProj (C := C) j.1 a)) =
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a)
rw [zcCompletedGroupAlgebraTransition_single]
have ha : modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
(proCIntegerProj (C := C) j.1 a) =
proCIntegerProj (C := C) i.1 a :=
proCIntegerProj_transition (C := C) hij.1 a
simpa using congrArg
(fun b : ProCIntegerStage C i.1 =>
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2) b)
ha⟩The coefficient element of \(\mathbb{Z}_C\llbracket H\rrbracket\) supported at the identity of \(H\).
def zcCompletedGroupAlgebraCoeffMap
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
ZCCoeff C →+* ZCCompletedGroupAlgebra C H where
toFun := zcCompletedGroupAlgebraCoeff C H
map_zero' := by
apply Subtype.ext
funext i
simp only [zcCompletedGroupAlgebraCoeff, proCIntegerProj_zero, Finsupp.single_zero,
zcCompletedGroupAlgebraProjection_zero]
map_one' := by
apply Subtype.ext
funext i
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
simp only [zcCompletedGroupAlgebraCoeff, proCIntegerProj_one, zcCompletedGroupAlgebraProjection_one,
MonoidAlgebra.one_def]
map_add' a b := by
apply Subtype.ext
funext i
simp only [zcCompletedGroupAlgebraCoeff, proCIntegerProj_add, Finsupp.single_add,
zcCompletedGroupAlgebraProjection_add]
map_mul' a b := by
apply Subtype.ext
funext i
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
change MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 (a * b)) =
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a) *
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 b)
simp only [proCIntegerProj_mul, MonoidAlgebra.single_mul_single, mul_one]
@[simp]Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism.
theorem zcCompletedGroupAlgebraProjection_coeffMap
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) :
zcCompletedGroupAlgebraProjection C H i
(zcCompletedGroupAlgebraCoeffMap C H a) =
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a)The completed group-algebra projection commutes with the coefficient-change map at the corresponding finite stage.
Show proof
rflProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□def zcGroupLike
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
H →* ZCCompletedGroupAlgebra C H where
toFun h := ⟨fun i =>
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h), by
intro i j hij
change
zcCompletedGroupAlgebraTransition C H hij
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C j.2) (QuotientGroup.mk h)) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)
rw [zcCompletedGroupAlgebraTransition_of C H hij]
rfl⟩
map_one' := by
apply Subtype.ext
funext i
simp only [MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk_one, MonoidHom.coe_mk, OneHom.coe_mk,
zcCompletedGroupAlgebraProjection_one, MonoidAlgebra.one_def]
map_mul' h₁ h₂ := by
apply Subtype.ext
funext i
change
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk (h₁ * h₂)) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₁) *
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₂)
simp only [MonoidAlgebra.of, QuotientGroup.mk_mul, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.single_mul_single, mul_one]The group-like map \(H \to \mathbb{Z}_C\llbracket H\rrbracket\).
theorem zcCompletedGroupAlgebraProjection_groupLike
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
zcCompletedGroupAlgebraProjection C H i (zcGroupLike C H h) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)Projecting a group-like element of \(\mathbb{Z}_C\llbracket H\rrbracket\) gives its finite-stage group-like image.
Show proof
rfl
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjectionRingHom_groupLike
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
zcCompletedGroupAlgebraProjectionRingHom C H i (zcGroupLike C H h) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)The projection ring homomorphism sends a group-like element to its image in the corresponding finite group-algebra stage.
Show proof
zcCompletedGroupAlgebraProjection_groupLike C H i hProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebra_projection_sub_one_mul_eq_zero
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(h : H) (y : ZCCompletedGroupAlgebra C H)
(i : ZCCompletedGroupAlgebraIndex C H)
(hrel : (zcGroupLike C H h - 1) * y = 0) :
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2)
(QuotientGroup.mk h) - 1) *
zcCompletedGroupAlgebraProjection C H i y = 0A completed group-algebra relation \((h - 1)y = 0\) descends to every finite stage.
Show proof
by
have hproj :=
congrArg (zcCompletedGroupAlgebraProjection C H i) hrel
simpa only [zcCompletedGroupAlgebraProjection_mul,
zcCompletedGroupAlgebraProjection_sub,
zcCompletedGroupAlgebraProjection_groupLike,
zcCompletedGroupAlgebraProjection_one,
zcCompletedGroupAlgebraProjection_zero] using hprojProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebra_projection_zpow_sub_one_mul_eq_zero
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(h : H) (n : ℤ) (y : ZCCompletedGroupAlgebra C H)
(i : ZCCompletedGroupAlgebraIndex C H)
(hrel : (zcGroupLike C H (h ^ n) - 1) * y = 0) :
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C i.2)
((QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2) ^ n) -
1) *
zcCompletedGroupAlgebraProjection C H i y = 0Integer-power version of finite-stage descent for \((h^n - 1)y = 0\).
Show proof
by
have hstage :=
zcCompletedGroupAlgebra_projection_sub_one_mul_eq_zero
C H (h ^ n) y i hrel
simpa only [map_zpow] using hstageProof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraTransition_sameCoeff
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(coeff : ProCIntegerIndex C)
{U V : OpenNormalSubgroupInClass C H}
(hUV : (V.1 : Subgroup H) ≤ (U.1 : Subgroup H)) :
zcCompletedGroupAlgebraTransition C H
(i := (coeff, OrderDual.toDual U))
(j := (coeff, OrderDual.toDual V))
(show (coeff, OrderDual.toDual U) ≤ (coeff, OrderDual.toDual V) from
⟨dvd_rfl, hUV⟩) =
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff coeff.modulus)
(OpenNormalSubgroupInClass.map
(C := C) (G := H) (U := U) (V := V) hUV)A \(\mathbb{Z}_C\llbracket H\rrbracket\) transition with unchanged coefficient modulus is just the quotient map on the finite group-algebra domain.
Show proof
by
letI : Fact (0 < coeff.modulus) := ⟨coeff.positive⟩
apply MonoidAlgebra.ringHom_ext
· intro r
rw [zcCompletedGroupAlgebraTransition_single]
change
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := C) (G := H) (U := U) (V := V) hUV) 1)
((modNCompletedCoeffMap (n := coeff.modulus)
(m := coeff.modulus) dvd_rfl) r) =
MonoidAlgebra.mapDomain
(OpenNormalSubgroupInClass.map
(C := C) (G := H) (U := U) (V := V) hUV)
(MonoidAlgebra.single 1 r)
rw [MonoidAlgebra.mapDomain_single]
simp only [map_one, modNCompletedCoeffMap, ZMod.castHom_self, RingHom.id_apply]
· intro q
rw [zcCompletedGroupAlgebraTransition_single]
change
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := C) (G := H) (U := U) (V := V) hUV) q)
((modNCompletedCoeffMap (n := coeff.modulus)
(m := coeff.modulus) dvd_rfl) (1 : ModNCompletedCoeff coeff.modulus)) =
MonoidAlgebra.mapDomain
(OpenNormalSubgroupInClass.map
(C := C) (G := H) (U := U) (V := V) hUV)
(MonoidAlgebra.single q (1 : ModNCompletedCoeff coeff.modulus))
rw [MonoidAlgebra.mapDomain_single]
simp only [modNCompletedCoeffMap, ZMod.castHom_self, RingHom.id_apply]
@[simp]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_coeffMap_mul_groupLike
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) (h : H) :
zcCompletedGroupAlgebraProjection C H i
(zcCompletedGroupAlgebraCoeffMap C H a * zcGroupLike C H h) =
MonoidAlgebra.single
(QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a)After coefficient change, projection of multiplication by a group-like element is computed in the corresponding finite group-algebra stage.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
rw [zcCompletedGroupAlgebraProjection_mul, zcCompletedGroupAlgebraProjection_coeffMap,
zcCompletedGroupAlgebraProjection_groupLike]
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.single_mul_single, one_mul,
mul_one]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□theorem zcCompletedGroupAlgebraProjection_surjective
(C : ProCGroups.FiniteGroupClass.{u})
(H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : ZCCompletedGroupAlgebraIndex C H) :
Function.Surjective (zcCompletedGroupAlgebraProjection C H i)Every finite-stage projection from the pro-\(C\) completed group algebra is surjective.
Show proof
by
classical
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : DecidableEq (CompletedGroupAlgebraQuotientInClass H C i.2) := Classical.decEq _
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, by simp only [zcCompletedGroupAlgebraProjection_zero]⟩
| @single_add q a x hq hx ih =>
rcases ih with ⟨y, hy⟩
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
⟨h, rfl⟩
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
let aLift : ZCCoeff C := (t : ProCIntegerLimitCarrier C)
refine ⟨zcCompletedGroupAlgebraCoeffMap C H aLift * zcGroupLike C H h + y, ?_⟩
rw [zcCompletedGroupAlgebraProjection_add,
zcCompletedGroupAlgebraProjection_coeffMap_mul_groupLike, hy]
simp only [proCIntegerProj_intCast, QuotientGroup.mk'_apply, aLift]Proof. Unfold \(\mathbb{Z}_C\llbracket H\rrbracket\) as the inverse limit over coefficient moduli and finite \(C\)-quotients of \(H\). Operations, projections, transition maps, group-like elements, and coefficient changes are computed coordinatewise at each finite group-algebra stage. Compatibility under refinement and extensionality of the inverse limit give the completed identities.
□def zcCompletedGroupAlgebraScalar (ψ : G →* H) :
G →* ZCCompletedGroupAlgebra C H :=
(zcGroupLike C H).comp ψ
@[simp]The completed coefficient homomorphism \(G \to \mathbb{Z}_C\llbracket H\rrbracket\) induced by \(\psi: G \to H\).
theorem zcCompletedGroupAlgebraScalar_apply (ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraScalar C ψ g = zcGroupLike C H (ψ g)The composite map is computed pointwise by applying the constituent coordinate formulas in succession.
Show proof
rfl
@[simp]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraScalar_subtype_ker (ψ : G →* H) (g : ψ.ker) :
zcCompletedGroupAlgebraScalar C ψ g = 1If \(g\in\ker \psi\), then the completed coefficient homomorphism induced by \(\psi\) sends \(g\) to the unit element.
Show proof
by
rw [zcCompletedGroupAlgebraScalar_apply, g.2, map_one]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□abbrev ZCCompletedDifferentialModule (ψ : G →* H) : Type _ :=
CrossedDifferentialModule (zcCompletedGroupAlgebraScalar C ψ)The algebraic universal \(\mathbb{Z}_C\llbracket H\rrbracket\) differential module attached to \(\psi : G \to H\). It is the \(\mathbb{Z}_C\llbracket H\rrbracket\)-module generated by the symbols dg, subject to the Leibniz relations \(d(gh)=dg+\) \([\psi(g)]\) dh, i.e. the quotient by the raw crossed-differential relation submodule. The final profinite Crowell middle term is the separated finite-stage quotient \(\mathbb{Z}_C\)-separated completed differential module, not this algebraic quotient.
def zcUniversalDifferential (ψ : G →* H) (g : G) :
ZCCompletedDifferentialModule C ψ :=
universalCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) gThe universal completed crossed differential.
theorem zcUniversalDifferential_mul (ψ : G →* H) (g₁ g₂ : G) :
zcUniversalDifferential C ψ (g₁ * g₂) =
zcUniversalDifferential C ψ g₁ +
zcCompletedGroupAlgebraScalar C ψ g₁ • zcUniversalDifferential C ψ g₂The universal completed crossed differential satisfies the crossed product rule on a product of group elements.
Show proof
universalCrossedDifferential_mul (zcCompletedGroupAlgebraScalar C ψ) g₁ g₂
@[simp]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcUniversalDifferential_one (ψ : G →* H) :
zcUniversalDifferential C ψ (1 : G) = 0The universal completed crossed differential vanishes at the identity element.
Show proof
universalCrossedDifferential_one (zcCompletedGroupAlgebraScalar C ψ)Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcUniversalDifferential_isCrossedDifferential (ψ : G →* H) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψ) (zcUniversalDifferential C ψ)The universal completed differential is a crossed differential for the completed group-algebra scalar action.
Show proof
universalCrossedDifferential_isCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ)Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCrossedDifferentialKernelAddMonoidHom
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
Additive ψ.ker →+ A :=
IsCrossedDifferential.restrictTrivialSubgroupAddMonoidHom hdelta ψ.ker
(zcCompletedGroupAlgebraScalar_subtype_ker (C := C) (ψ := ψ))
@[simp]A completed \(\mathbb{Z}_C\llbracket H\rrbracket\) crossed differential restricts to an ordinary additive homomorphism on \(\ker \psi\).
theorem zcCrossedDifferentialKernelAddMonoidHom_apply
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(g : ψ.ker) :
zcCrossedDifferentialKernelAddMonoidHom C ψ delta hdelta (Additive.ofMul g) = delta gThe additive homomorphism on the profinite kernel is evaluated by applying the crossed differential to the underlying kernel element.
Show proof
rflProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCompletedGroupAlgebraBoundary (ψ : G →* H) (g : G) :
ZCCompletedGroupAlgebra C H :=
zcGroupLike C H (ψ g) - 1
@[simp]The completed Fox boundary \(g \mapsto [\psi(g)] - 1\) in \(\mathbb{Z}_C\llbracket H\rrbracket\).
theorem zcCompletedGroupAlgebraBoundary_one (ψ : G →* H) :
zcCompletedGroupAlgebraBoundary C ψ (1 : G) = 0The completed Crowell--Fox boundary of \(1\) is zero.
Show proof
by
simp only [zcCompletedGroupAlgebraBoundary, map_one, sub_self]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
(ψ : G →* H) {g : G} (hg : ψ g = 1) :
zcCompletedGroupAlgebraBoundary C ψ g = 0The completed Fox boundary vanishes on elements in the kernel of the target map.
Show proof
by
rw [zcCompletedGroupAlgebraBoundary, hg, map_one]
simp only [sub_self]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_subtype_ker
(ψ : G →* H) (g : ψ.ker) :
zcCompletedGroupAlgebraBoundary C ψ g = 0The completed Fox boundary restricted to the kernel subgroup is zero.
Show proof
zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker (C := C) (ψ := ψ) g.2Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_isCrossedDifferential (ψ : G →* H) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψ) (zcCompletedGroupAlgebraBoundary C ψ)The boundary map on the completed group algebra is a crossed differential, characterized by finite-stage Fox coordinate formulas.
Show proof
by
intro g h
simp only [zcCompletedGroupAlgebraBoundary, map_mul, sub_eq_add_neg, add_comm,
zcCompletedGroupAlgebraScalar_apply, smul_eq_mul, mul_add, mul_neg, mul_one, add_assoc, add_neg_cancel_comm_assoc]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_mul (ψ : G →* H) (g₁ g₂ : G) :
zcCompletedGroupAlgebraBoundary C ψ (g₁ * g₂) =
zcCompletedGroupAlgebraBoundary C ψ g₁ +
zcCompletedGroupAlgebraScalar C ψ g₁ •
zcCompletedGroupAlgebraBoundary C ψ g₂The completed Crowell--Fox boundary of a product satisfies the crossed-derivation formula in \(\mathbb{Z}_C\llbracket H\rrbracket\).
Show proof
zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ g₁ g₂Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_inv (ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraBoundary C ψ g⁻¹ =
-(zcCompletedGroupAlgebraScalar C ψ g⁻¹ •
zcCompletedGroupAlgebraBoundary C ψ g)The completed Crowell--Fox boundary of an inverse satisfies the corresponding inverse formula in \(\mathbb{Z}_C\llbracket H\rrbracket\).
Show proof
IsCrossedDifferential.inv
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ) gProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_pow (ψ : G →* H) (g : G) (m : ℕ) :
zcCompletedGroupAlgebraBoundary C ψ (g ^ m) =
(Finset.range m).sum
(fun k => zcCompletedGroupAlgebraScalar C ψ (g ^ k) •
zcCompletedGroupAlgebraBoundary C ψ g)The completed Crowell--Fox boundary of a power satisfies the corresponding power formula in \(\mathbb{Z}_C\llbracket H\rrbracket\).
Show proof
IsCrossedDifferential.pow
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ) g mProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCompletedDifferentialModuleLift
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A :=
crossedDifferentialModuleLift (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta
@[simp]The universal lift from the \(\mathbb{Z}_C\)-completed differential module associated to a completed crossed differential.
theorem zcCompletedDifferentialModuleLift_universal
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) (g : G) :
zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta
(zcUniversalDifferential C ψ g) =
delta gThe universal lift sends each completed universal differential to the value of the given completed crossed differential.
Show proof
crossedDifferentialModuleLift_universal
(A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta g
@[ext]Proof. Unfold the \(\mathbb{Z}_C\)-completed differential module as an inverse-limit quotient of the finite-stage universal differential modules. Source maps, lift maps, and homomorphism extensionality are checked after projecting to finite source, target, and coefficient stages; finite-stage compatibility then assembles the completed module statement by inverse-limit extensionality.
□theorem zcCompletedDifferentialModuleHom_ext
(ψ : G →* H)
{f h : ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A}
(hfh : ∀ g, f (zcUniversalDifferential C ψ g) =
h (zcUniversalDifferential C ψ g)) :
f = hLinear maps out of the \(\mathbb{Z}_C\)-completed differential module are equal when they agree on all completed universal differentials.
Show proof
crossedDifferentialModuleHom_ext (A := A) (zcCompletedGroupAlgebraScalar C ψ) hfhProof. Unfold the \(\mathbb{Z}_C\)-completed differential module as an inverse-limit quotient of the finite-stage universal differential modules. Source maps, lift maps, and homomorphism extensionality are checked after projecting to finite source, target, and coefficient stages; finite-stage compatibility then assembles the completed module statement by inverse-limit extensionality.
□theorem zcCompletedDifferentialModuleLift_unique
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(f : ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A)
(hf : ∀ g, f (zcUniversalDifferential C ψ g) = delta g) :
f = zcCompletedDifferentialModuleLift (A := A) C ψ delta hdeltaThe universal lift is the unique linear map with the prescribed values on completed universal differentials.
Show proof
crossedDifferentialModuleLift_unique
(A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta f hfProof. Unfold the \(\mathbb{Z}_C\)-completed differential module as an inverse-limit quotient of the finite-stage universal differential modules. Source maps, lift maps, and homomorphism extensionality are checked after projecting to finite source, target, and coefficient stages; finite-stage compatibility then assembles the completed module statement by inverse-limit extensionality.
□theorem existsUnique_zcCompletedDifferentialModuleLift
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
∃! f : ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A,
∀ g, f (zcUniversalDifferential C ψ g) = delta gThere exists a unique linear lift from the \(\mathbb{Z}_C\)-completed differential module representing the given completed crossed differential.
Show proof
existsUnique_crossedDifferentialModuleLift
(A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdeltaProof. Unfold the \(\mathbb{Z}_C\)-completed differential module as an inverse-limit quotient of the finite-stage universal differential modules. Source maps, lift maps, and homomorphism extensionality are checked after projecting to finite source, target, and coefficient stages; finite-stage compatibility then assembles the completed module statement by inverse-limit extensionality.
□def zcCompletedCrossedDifferentialEquivLinearMap (ψ : G →* H) :
{delta : G → A // IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta} ≃
(ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A) :=
crossedDifferentialModuleEquivLinearMap (A := A) (zcCompletedGroupAlgebraScalar C ψ)Crossed differentials with \(\mathbb{Z}_C\)-completed coefficients are equivalent to \(\mathbb{Z}_C\)-completed group-algebra linear maps out of the completed differential module.
def zcToCompletedGroupAlgebra (ψ : G →* H) :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedGroupAlgebra C H :=
zcCompletedDifferentialModuleLift (A := ZCCompletedGroupAlgebra C H) C ψ
(zcCompletedGroupAlgebraBoundary C ψ)
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ)
@[simp]The universal \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear map from the completed crossed-differential module to the completed group algebra is induced by the completed Fox boundary \(g\mapsto [\psi(g)]-1\).
theorem zcToCompletedGroupAlgebra_universal (ψ : G →* H) (g : G) :
zcToCompletedGroupAlgebra C ψ (zcUniversalDifferential C ψ g) =
zcCompletedGroupAlgebraBoundary C ψ gThe universal map to the completed group algebra sends the universal differential of \(g\) to the completed Fox boundary \([\psi(g)]-1\).
Show proof
zcCompletedDifferentialModuleLift_universal
(A := ZCCompletedGroupAlgebra C H) C ψ
(zcCompletedGroupAlgebraBoundary C ψ)
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ) gProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem existsUnique_zcToCompletedGroupAlgebra (ψ : G →* H) :
∃! f :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedGroupAlgebra C H,
∀ g, f (zcUniversalDifferential C ψ g) =
zcCompletedGroupAlgebraBoundary C ψ gThere is a unique \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear map from the completed crossed-differential module to the completed group algebra that sends every universal differential to the corresponding completed Fox boundary.
Show proof
existsUnique_zcCompletedDifferentialModuleLift
(A := ZCCompletedGroupAlgebra C H) C ψ
(zcCompletedGroupAlgebraBoundary C ψ)
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ)Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCompletedDifferentialModuleSourceMap
(ψ' : G' →* H) (f : G →* G') :
ZCCompletedDifferentialModule C (ψ'.comp f) →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedDifferentialModule C ψ' :=
zcCompletedDifferentialModuleLift (A := ZCCompletedDifferentialModule C ψ')
C (ψ'.comp f) (fun g => zcUniversalDifferential C ψ' (f g)) (by
intro g h
change zcUniversalDifferential C ψ' (f (g * h)) =
zcUniversalDifferential C ψ' (f g) +
zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
zcUniversalDifferential C ψ' (f h)
rw [map_mul, zcUniversalDifferential_mul]
rfl)
@[simp]theorem zcCompletedDifferentialModuleSourceMap_universal
(ψ' : G' →* H) (f : G →* G') (g : G) :
zcCompletedDifferentialModuleSourceMap (C := C) ψ' f
(zcUniversalDifferential C (ψ'.comp f) g) =
zcUniversalDifferential C ψ' (f g)The universal source map on the completed differential module is determined by the source quotient maps at finite stages.
Show proof
zcCompletedDifferentialModuleLift_universal
(A := ZCCompletedDifferentialModule C ψ') C (ψ'.comp f)
(fun g => zcUniversalDifferential C ψ' (f g))
(by
intro g h
change zcUniversalDifferential C ψ' (f (g * h)) =
zcUniversalDifferential C ψ' (f g) +
zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
zcUniversalDifferential C ψ' (f h)
rw [map_mul, zcUniversalDifferential_mul]
rfl)
gProof. Unfold the \(\mathbb{Z}_C\)-completed differential module as an inverse-limit quotient of the finite-stage universal differential modules. Source maps, lift maps, and homomorphism extensionality are checked after projecting to finite source, target, and coefficient stages; finite-stage compatibility then assembles the completed module statement by inverse-limit extensionality.
□theorem zcUniversalDifferential_eq_zero_of_source
(ψ' : G' →* H) (f : G →* G') {g : G}
(hg : zcUniversalDifferential C (ψ'.comp f) g = 0) :
zcUniversalDifferential C ψ' (f g) = 0Completed universal zero descends along a source homomorphism.
Show proof
by
rw [← zcCompletedDifferentialModuleSourceMap_universal (C := C) ψ' f g, hg, map_zero]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem crossedDifferential_eq_zero_of_zcUniversalDifferential_eq_zero
(ψ : G →* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) D)
{g : G} (hg : zcUniversalDifferential C ψ g = 0) :
D g = 0A zero universal differential is killed by every crossed differential represented by the completed universal module.
Show proof
by
rw [← zcCompletedDifferentialModuleLift_universal (A := A) C ψ D hD g, hg, map_zero]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□