FoxDifferential.Completed.FreeProC.SemidirectKernelBasis
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def HasAdditiveIdentityQuotientKernelNeighbourhoodBasis : Prop :=
∀ U : Set A, IsOpen U → (0 : A) ∈ U →
∃ j : J, ∀ z : A, π j z = 0 → z ∈ UAdditive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive analogue of HasIdentityQuotientKernelNeighborhoodBasis. It is used for the left coordinate \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), whose finite-stage maps are additive homomorphisms rather than multiplicative homomorphisms.
def HasFiniteCoordinateZeroRectangularNeighbourhoods : Prop :=
∀ U : Set (X → A), IsOpen U → (0 : X → A) ∈ U →
∃ V : X → Set A,
(∀ x : X, IsOpen (V x) ∧ (0 : A) ∈ V x) ∧
∀ v : X → A, (∀ x : X, v x ∈ V x) → v ∈ Utheorem coordinatewiseAddMonoidHom_apply
(π : ∀ j : J, A →+ B j) (j : J) (v : X → A) (x : X) :
coordinatewiseAddMonoidHom (X := X) π j v x = π j (v x)The coordinatewise additive homomorphism evaluates by applying the chosen additive map to each coordinate.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem coordinatewiseAdditiveKernelBasis_of_component_basis
(π : ∀ j : J, A →+ B j)
(hrect : HasFiniteCoordinateZeroRectangularNeighbourhoods (A := A) (X := X))
(hdir : Directed (· ≤ ·) (id : J → J))
(hbasis : HasAdditiveIdentityQuotientKernelNeighbourhoodBasis (A := A) π)
(hmono : ∀ {i j : J}, i ≤ j → ∀ a : A, π j a = 0 → π i a = 0) :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := X → A)
(fun j : J => coordinatewiseAddMonoidHom (X := X) π j)Show proof
by
intro U hU hUzero
rcases hrect U hU hUzero with ⟨V, hV, hrectU⟩
have hstage : ∀ x : X, ∃ j : J, ∀ a : A, π j a = 0 → a ∈ V x := by
intro x
exact hbasis (V x) (hV x).1 (hV x).2
choose jx hjx using hstage
classical
have hupper : ∀ s : Finset X, ∃ k : J, ∀ x : X, x ∈ s → jx x ≤ k := by
intro s
induction s using Finset.induction_on with
| empty =>
exact ⟨Classical.choice (inferInstance : Nonempty J), by simp only [Finset.notMem_empty, IsEmpty.forall_iff, implies_true]⟩
| insert x s hxs ih =>
rcases ih with ⟨k, hk⟩
rcases hdir (jx x) k with ⟨l, hxl, hkl⟩
refine ⟨l, ?_⟩
intro y hy
rw [Finset.mem_insert] at hy
rcases hy with rfl | hy
· exact hxl
· exact (hk y hy).trans hkl
rcases hupper (Finset.univ : Finset X) with ⟨k, hk⟩
refine ⟨k, ?_⟩
intro v hv
refine hrectU v ?_
intro x
exact hjx x (v x) (hmono (hk x (by simp only [Finset.mem_univ])) (v x) (by
have hvx := congrArg (fun f : X → B k => f x) hv
simpa [coordinatewiseAddMonoidHom] using hvx))Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□def HasSemidirectRectangularIdentityNeighbourhoods
(C : ProCGroups.FiniteGroupClass.{u})
[TopologicalSpace (ZCCompletedGroupAlgebra C H)]
[TopologicalSpace (ZCCompletedFoxSemidirect C X H)] : Prop :=
∀ U : Set (ZCCompletedFoxSemidirect C X H),
IsOpen U → (1 : ZCCompletedFoxSemidirect C X H) ∈ U →
∃ UL : Set (ZCFreeFoxCoordinates C (X := X) (H := H)),
∃ UR : Set H,
IsOpen UL ∧ (0 : ZCFreeFoxCoordinates C (X := X) (H := H)) ∈ UL ∧
IsOpen UR ∧ (1 : H) ∈ UR ∧
∀ y : ZCCompletedFoxSemidirect C X H,
y.left ∈ UL → y.right ∈ UR → y ∈ UIdentity neighborhoods in the completed Fox semidirect product contain component rectangles. For the standard product topology this follows from the product homeomorphism \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H \cong \mathbb{Z}_C\llbracket H\rrbracket^{X} \times H\); it is kept as a named property so the algebraic componentwise kernel-basis theorem below is independent of the concrete topology.
theorem freeProCZCCompletedFoxSemidirectStageMap_identity_basis_of_component_bases
(hrect : HasSemidirectRectangularIdentityNeighbourhoods
(X := X) (H := H) ProC.finiteQuotientClass)
(hdir : Directed (· ≤ ·) (id : J → J))
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J, H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar : ∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hleft_basis :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
stageLeft)
(hright_basis :
HasIdentityQuotientKernelNeighbourhoodBasis (Y := H) stageRight)
(hleft_mono : ∀ {i j : J}, i ≤ j →
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
stageLeft j v = 0 → stageLeft i v = 0)
(hright_mono : ∀ {i j : J}, i ≤ j → ∀ h : H,
stageRight j h = 1 → stageRight i h = 1) :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j))If the coordinate kernels and target kernels are neighborhood bases in the two components, and the finite-stage kernels are monotone along the directed stage system, then the semidirect stage kernels are a neighborhood basis at the identity. This is the topological bridge needed to feed actual finite quotient projections into the completed Fox density theorem.
Show proof
by
intro U hU hUone
rcases hrect U hU hUone with
⟨UL, UR, hULopen, hULzero, hURopen, hURone, hrectangle⟩
rcases hleft_basis UL hULopen hULzero with ⟨i, hi⟩
rcases hright_basis UR hURopen hURone with ⟨j, hj⟩
rcases hdir i j with ⟨k, hik, hjk⟩
refine ⟨k, ?_⟩
intro y hy
have hycoords : stageLeft k y.left = 0 ∧ stageRight k y.right = 1 := by
exact
(freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff
(ProC := ProC) (X := X) (H := H) (N := Nstage k) (n := nstage k)
(stageLeft := stageLeft k) (stageRight := stageRight k)
(hscalar := hscalar k) (y := y)).1 hy
exact hrectangle y
(hi y.left (hleft_mono hik y.left hycoords.1))
(hj y.right (hright_mono hjk y.right hycoords.2))Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem zcFreeFoxCoordinatesBifilteredStageMap_kernel_mono
(hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
modNCompletedCoeffMap
(n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
(modNCompletedCoeffMap
(n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
(hzcIndex hij).1 a) =
modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
(modNCompletedCoeffMap
(n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
(hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hzcIndex hij).2) q) =
finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
{i j : J} (hij : i ≤ j)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hv :
zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
j v = 0) :
zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
i v = 0The left coordinate kernels of the actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered stage maps are monotone along stage refinement.
Show proof
by
have htransition :=
zcFreeFoxCoordinatesBifilteredStageMap_transition
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
(fun hij a =>
zcCompletedGroupAlgebraBifilteredStageCoeffMap_transition
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap hcoeff_mod hqmap_transition hij a)
hij v
-- The coefficient-map transition theorem above packages the exact finite target transition.
-- Reading the displayed equality backwards shows that the coarser coordinate is the transition
-- of the finer coordinate, hence a finer zero maps to a coarser zero.
calc
zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
i v
= finiteFoxStageBifilteredCoordinateVectorMap (X := X) (hN hij) (hn hij)
(zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
j v) := htransition.symm
_ = 0 := by
rw [hv]
funext x
exact map_zero (finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) (hN hij) (hn hij))Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem zcCompletedGroupAlgebraBifilteredStageCoeffMap_kernel_mono
(hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
modNCompletedCoeffMap
(n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
(modNCompletedCoeffMap
(n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
(hzcIndex hij).1 a) =
modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
(modNCompletedCoeffMap
(n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
(hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hzcIndex hij).2) q) =
finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
{i j : J} (hij : i ≤ j)
(a : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(ha :
zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a = 0) :
zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a = 0The coefficient kernels of actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite-stage maps are monotone along stage refinement.
Show proof
by
have htransition :=
zcCompletedGroupAlgebraBifilteredStageCoeffMap_transition
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap hcoeff_mod hqmap_transition hij a
calc
zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a
= finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) (hN hij) (hn hij)
(zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a) :=
htransition.symm
_ = 0 := by
rw [ha]
exact map_zero (finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) (hN hij) (hn hij))Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis
[Fintype X] [Nonempty J]
(hcoord_rect :
HasFiniteCoordinateZeroRectangularNeighbourhoods
(A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) (X := X))
(hdir : Directed (· ≤ ·) (id : J → J))
(hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
modNCompletedCoeffMap
(n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
(modNCompletedCoeffMap
(n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
(hzcIndex hij).1 a) =
modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
(modNCompletedCoeffMap
(n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
(hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hzcIndex hij).2) q) =
finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
(hcoeff_basis :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun j : J =>
(zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom)) :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(fun j : J =>
zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j)Additive kernel basis for completed Fox-coordinate projections, reduced to the coefficient ring projections. This is the next component-level target after semidirect kernel bases: prove that the coefficient maps \(\mathbb{Z}_C\llbracket H\rrbracket \to (\mathbb{Z}/n_j\mathbb{Z})[F/N_j]\) have a kernel-neighborhood basis, and the coordinate result follows for finite \(X\).
Show proof
by
change
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := X → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun j : J =>
coordinatewiseAddMonoidHom (X := X)
(fun k : J =>
(zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k).toAddMonoidHom) j)
exact
coordinatewiseAdditiveKernelBasis_of_component_basis
(X := X)
(fun k : J =>
(zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k).toAddMonoidHom)
hcoord_rect hdir hcoeff_basis
(fun hij a ha =>
zcCompletedGroupAlgebraBifilteredStageCoeffMap_kernel_mono
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap hcoeff_mod hqmap_transition hij a ha)Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem zcCompletedGroupAlgebraBifilteredStageRightMap_kernel_mono
(hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hzcIndex hij).2) q) =
finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
{i j : J} (hij : i ≤ j) (h : H)
(hh :
zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j h = 1) :
zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap i h = 1The right kernels of the automatically defined bifiltered stage maps are monotone along stage refinement.
Show proof
by
calc
zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap i h
= finiteFoxStageTargetQuotientMap (X := X) (hN hij)
(zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j h) :=
(zcCompletedGroupAlgebraBifilteredStageRightMap_transition
(ProC := ProC) (X := X) (H := H) (Nstage := Nstage) (hN := hN)
(zcIndex := zcIndex) (hzcIndex := hzcIndex) (qmap := qmap)
hqmap_transition hij h).symm
_ = 1 := by
rw [hh]
exact map_one (finiteFoxStageTargetQuotientMap (X := X) (hN hij))Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases
(hrect : HasSemidirectRectangularIdentityNeighbourhoods
(X := X) (H := H) ProC.finiteQuotientClass)
(hdir : Directed (· ≤ ·) (id : J → J))
(hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
modNCompletedCoeffMap
(n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
(modNCompletedCoeffMap
(n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
(hzcIndex hij).1 a) =
modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
(modNCompletedCoeffMap
(n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
(hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hzcIndex hij).2) q) =
finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
(hleft_basis :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(fun j : J =>
zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j))
(hright_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := H)
(fun j : J =>
zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j)) :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j)Componentwise zero/identity kernel bases imply the identity-neighborhood kernel basis for the actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered semidirect stage maps. This removes the need to prove the semidirect kernel basis in one monolithic step: it is enough to prove it for the completed Fox-coordinate projections and for the target quotient maps.
Show proof
by
refine
freeProCZCCompletedFoxSemidirectStageMap_identity_basis_of_component_bases
(ProC := ProC) (X := X) (H := H) Nstage nstage hrect hdir
(fun j =>
zcFreeFoxCoordinatesBifilteredStageMap
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j)
(fun j =>
zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j)
(fun j h v =>
zcFreeFoxCoordinatesBifilteredStageMap_smul_groupLike
(ProC := ProC) (X := X) (H := H) Nstage nstage
(fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
(zcCompletedGroupAlgebraBifilteredStageRightMap
(ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap)
(fun k h => zcCompletedGroupAlgebraBifilteredStageCoeffMap_groupLike_autoRight
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k h)
j h v)
hleft_basis hright_basis ?_ ?_
· intro i j hij v hv
exact zcFreeFoxCoordinatesBifilteredStageMap_kernel_mono
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap hcoeff_mod hqmap_transition hij v hv
· intro i j hij h hh
exact zcCompletedGroupAlgebraBifilteredStageRightMap_kernel_mono
(ProC := ProC) (X := X) (H := H) Nstage hN zcIndex hzcIndex qmap
hqmap_transition hij h hhProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□