FoxDifferential.Completed.Continuous.SemidirectKernelBasis
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem finiteCoordinateZeroRectangularNeighbourhoods_pi :
HasFiniteCoordinateZeroRectangularNeighbourhoods (A := A) (X := X)Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This is the generic topological input needed to pass from coefficient-kernel bases for \(\mathbb{Z}_C\llbracket H\rrbracket\) to coordinate-kernel bases for \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\). It uses the product topology directly and keeps no algebraic assumptions.
Show proof
by
intro U hU hUzero
classical
rcases (isOpen_pi_iff.mp hU) (0 : X → A) hUzero with ⟨J, W, hW, hJU⟩
let V : X → Set A := fun x => if hx : x ∈ J then W x else Set.univ
refine ⟨V, ?_, ?_⟩
· intro x
by_cases hx : x ∈ J
· simpa [V, hx] using hW x hx
· simp only [dite_eq_ite, hx, ↓reduceIte, isOpen_univ, Set.mem_univ, and_self, V]
· intro v hv
apply hJU
intro x hx
have hvx := hv x
have hxJ : x ∈ J := by
simpa using hx
have hVx : V x = W x := by
simp only [dite_eq_ite, hxJ, ↓reduceIte, V]
rwa [hVx] at hvxProof. 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 zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods
(C : ProCGroups.FiniteGroupClass.{u}) (X H : Type u)
[Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
HasFiniteCoordinateZeroRectangularNeighbourhoods
(A := ZCCompletedGroupAlgebra C H) (X := X)Standard product-topology coordinate rectangles for completed Fox-coordinate families.
Show proof
finiteCoordinateZeroRectangularNeighbourhoods_piProof. 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. 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 zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods :
HasSemidirectRectangularIdentityNeighbourhoods
(X := X) (H := H) CIn the standard topology on \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\), every identity neighborhood contains a product rectangle around (0,1) in the coordinate and target components.
Show proof
by
intro U hU hUone
rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVeq⟩
have hVone :
((0 : ZCFreeFoxCoordinates C (X := X) (H := H)), (1 : H)) ∈ V := by
have hpre :
(1 : ZCCompletedFoxSemidirect C X H) ∈
(fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) ⁻¹' V := by
simpa [hVeq]
using hUone
simpa using hpre
have hVnhds : V ∈ 𝓝 ((0 : ZCFreeFoxCoordinates C (X := X) (H := H)), (1 : H)) :=
hVopen.mem_nhds hVone
rcases mem_nhds_prod_iff.mp hVnhds with ⟨UL₀, hUL₀, UR₀, hUR₀, hprod⟩
rcases mem_nhds_iff.mp hUL₀ with ⟨UL, hULsub, hULopen, hULzero⟩
rcases mem_nhds_iff.mp hUR₀ with ⟨UR, hURsub, hURopen, hURone⟩
refine ⟨UL, UR, hULopen, hULzero, hURopen, hURone, ?_⟩
intro y hyL hyR
have hyV : (y.left, y.right) ∈ V :=
hprod (show (y.left, y.right) ∈ UL₀ ×ˢ UR₀ from ⟨hULsub hyL, hURsub hyR⟩)
have hyUpre : y ∈
(fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) ⁻¹' V := hyV
simpa [hVeq] using hyUpreProof. 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. 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. 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. 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 freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology
(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)Standard-topology form of the componentwise kernel-basis theorem for actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite stages.
Show proof
by
exact
freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap
(zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods
(C := ProC.finiteQuotientClass) X H)
hdir hcoeff_mod hqmap_transition hleft_basis hright_basisProof. 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_additive_basis_of_coeff_basis_standardTopology
[Fintype X] [Nonempty J]
(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)Standard-topology additive kernel basis for completed Fox coordinates, reduced to the coefficient-ring kernel basis. For finite Fox coordinate families, product neighborhoods give the coordinate rectangles needed for the coordinate-kernel theorem.
Show proof
by
exact
zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap
(zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods
(C := ProC.finiteQuotientClass) X H)
hdir hcoeff_mod hqmap_transition hcoeff_basisProof. 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 semiZCBiStageMap_identityBasis_of_coeff_rightBases
[Fintype X] [Nonempty J]
(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))
(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)The semidirect kernel basis for the standard topology from coefficient and target component bases. This is the componentwise kernel-basis theorem with the left coordinate basis built internally from the coefficient maps \(\mathbb{Z}_C\llbracket H\rrbracket \to (\mathbb{Z}/n_j\mathbb{Z})[F/N_j]\).
Show proof
by
exact
freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap hdir hcoeff_mod hqmap_transition
(zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis_standardTopology
(ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
hmod qmap hdir hcoeff_mod hqmap_transition hcoeff_basis)
hright_basisProof. 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.
□