FoxDifferential.Completed.Comparison.DiscreteCompletion
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.
import
def finiteFoxStageGroupRingReduction :
GroupRing (finiteFoxStageTargetQuotient (X := X) N) →+*
finiteFoxStageTargetGroupAlgebra (X := X) N n :=
MonoidAlgebra.mapRangeRingHom
(finiteFoxStageTargetQuotient (X := X) N)
(Int.castRingHom (ModNCompletedCoeff n))Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).
theorem finiteFoxStageGroupRingReduction_of
(q : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxStageGroupRingReduction (X := X) N n
(MonoidAlgebra.of ℤ (finiteFoxStageTargetQuotient (X := X) N) q) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) qThe finite-stage group-ring reduction sends a group-like basis element to the same quotient basis element with reduced coefficient.
Show proof
by
simp only [finiteFoxStageGroupRingReduction, MonoidAlgebra.of_apply, MonoidAlgebra.mapRangeRingHom_single,
eq_intCast, Int.cast_one]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. 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. 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.
□theorem finiteFoxStageGroupRingReduction_apply
(x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
(q : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxStageGroupRingReduction (X := X) N n x q =
(x q : ModNCompletedCoeff n)Coefficients of the finite-stage group-ring reduction are ordinary reduction modulo \(n\).
Show proof
by
rw [finiteFoxStageGroupRingReduction, MonoidAlgebra.mapRangeRingHom_apply]
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. 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. 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.
□theorem int_eq_zero_of_forall_zmod_cast_eq_zero
(z : ℤ) (hz : ∀ n : ℕ, 0 < n → (z : ZMod n) = 0) :
z = 0An integer whose image in every positive residue ring is zero is zero.
Show proof
by
by_contra hzne
let n : ℕ := z.natAbs + 1
have hn : 0 < n := Nat.succ_pos z.natAbs
have hzmod : (z : ZMod n) = 0 := hz n hn
have hdvdInt : (n : ℤ) ∣ z := by
exact (ZMod.intCast_zmod_eq_zero_iff_dvd z n).mp hzmod
have hdvdNat : n ∣ z.natAbs := (Int.natCast_dvd).1 hdvdInt
have hzabs_pos : 0 < z.natAbs := Int.natAbs_pos.mpr hzne
have hle : n ≤ z.natAbs := Nat.le_of_dvd hzabs_pos hdvdNat
exact Nat.not_succ_le_self z.natAbs hleProof. 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\). 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□theorem int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero
(p : ℕ) [Fact (Nat.Prime p)] (z : ℤ)
(hz : ∀ k : ℕ, (z : ZMod (p ^ k)) = 0) :
z = 0An integer whose image in every \(p^k\) residue ring is zero is zero.
Show proof
by
by_contra hzne
let k : ℕ := Nat.log p z.natAbs + 1
have hp1 : 1 < p := (Fact.out : Nat.Prime p).one_lt
have hlt : z.natAbs < p ^ k := by
simpa [k, Nat.succ_eq_add_one] using
Nat.lt_pow_succ_log_self hp1 z.natAbs
have hzmod : (z : ZMod (p ^ k)) = 0 := hz k
have hdvdInt : ((p ^ k : ℕ) : ℤ) ∣ z := by
exact (ZMod.intCast_zmod_eq_zero_iff_dvd z (p ^ k)).mp hzmod
have hdvdNat : p ^ k ∣ z.natAbs := (Int.natCast_dvd).1 hdvdInt
have hzabs_pos : 0 < z.natAbs := Int.natAbs_pos.mpr hzne
have hle : p ^ k ≤ z.natAbs := Nat.le_of_dvd hzabs_pos hdvdNat
exact (not_lt_of_ge hle) hltProof. 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\). 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□theorem groupRing_eq_zero_of_nsmul_eq_zero
{M : Type*} [Monoid M] {n : ℕ} (hn : 0 < n) (x : GroupRing M)
(hx : n • x = 0) :
x = 0Integral group rings are torsion-free for positive natural scalar multiplication.
Show proof
by
ext m
have hcoeff : n • x m = 0 := by
exact congrArg (fun y : GroupRing M => y m) hx
have hmul : (n : ℤ) * x m = 0 := by
rw [← nsmul_eq_mul]
exact hcoeff
exact (Int.mul_eq_zero.mp hmul).resolve_left (by exact_mod_cast (Nat.ne_of_gt hn))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. 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. 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. 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 groupRing_eq_zero_of_forall_finiteFoxStageGroupRingReduction_eq_zero
(x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
(hx : ∀ n : ℕ, 0 < n →
finiteFoxStageGroupRingReduction (X := X) N n x = 0) :
x = 0Show proof
by
ext q
apply int_eq_zero_of_forall_zmod_cast_eq_zero
intro n hn
have hcoeff := congrArg (fun y => y q) (hx n hn)
simpa using hcoeffProof. 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\). 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. 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 groupRing_eq_zero_of_forall_finiteFoxStageGroupRingReduction_primePow_eq_zero
(p : ℕ) [Fact (Nat.Prime p)]
(x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
(hx : ∀ k : ℕ,
finiteFoxStageGroupRingReduction (X := X) N (p ^ k) x = 0) :
x = 0Show proof
by
ext q
apply int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero p
intro k
have hcoeff := congrArg (fun y => y q) (hx k)
simpa using hcoeffProof. 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\). 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. 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 exists_eq_nsmul_of_finiteFoxStageGroupRingReduction_eq_zero
{n : ℕ} (_hn : 0 < n)
(x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
(hx : finiteFoxStageGroupRingReduction (X := X) N n x = 0) :
∃ y : GroupRing (finiteFoxStageTargetQuotient (X := X) N), x = n • yShow proof
by
classical
let Q := finiteFoxStageTargetQuotient (X := X) N
have hdvd : ∀ q : Q, (n : ℤ) ∣ x q := by
intro q
exact (ZMod.intCast_zmod_eq_zero_iff_dvd (x q) n).mp (by
have hcoeff :=
congrArg
(fun y : finiteFoxStageTargetGroupAlgebra (X := X) N n => y q) hx
simpa using hcoeff)
let coeff : Q → ℤ := fun q =>
if x q = 0 then 0 else Classical.choose (hdvd q)
have hcoeff_support : ∀ q : Q, coeff q ≠ 0 → q ∈ x.support := by
intro q hq
rw [Finsupp.mem_support_iff]
intro hxq
have hzero : coeff q = 0 := by
dsimp [coeff]
rw [if_pos hxq]
exact hq hzero
let y : Q →₀ ℤ := Finsupp.onFinset x.support coeff hcoeff_support
refine ⟨y, ?_⟩
ext q
change x q = n • coeff q
by_cases hxq : x q = 0
· simp only [hxq, ↓reduceIte, nsmul_zero, coeff]
· have hchoose := Classical.choose_spec (hdvd q)
simpa [coeff, hxq, nsmul_eq_mul] using hchooseProof. 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. 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. 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.
□theorem finiteFoxStageDerivativeVector_eq_discreteReduction
(w : FreeGroup X) :
finiteFoxStageDerivativeVector (X := X) N n w =
fun i : X =>
finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w i)The finite-stage derivative vector is the image of the ordinary relative Fox derivative under coefficient reduction from \(\mathbb{Z}[F/N]\) to \((\mathbb{Z}/n\mathbb{Z})[F/N]\).
Show proof
by
let delta : FreeGroup X → finiteFoxStageCoordinateVector (X := X) N n :=
fun w i =>
finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w i)
have hdelta :
IsCrossedDifferential (finiteFoxStageCoefficient (X := X) N n) delta := by
intro u v
funext i
change finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) (u * v) i) =
finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) u i) +
finiteFoxStageCoefficient (X := X) N n u *
finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) v i)
rw [show
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) (u * v) i =
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) u i +
(MonoidAlgebra.of ℤ (finiteFoxStageTargetQuotient (X := X) N)
(QuotientGroup.mk' N u) :
FoxDifferential.GroupRing (finiteFoxStageTargetQuotient (X := X) N)) *
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) v i by
simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using
congrFun
(FoxCalculus.relativeFreeGroupFoxDerivative_mul
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) u v) i]
rw [map_add, map_mul, finiteFoxStageGroupRingReduction_of]
rfl
have hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : finiteFoxStageTargetGroupAlgebra (X := X) N n) := by
intro x
funext i
by_cases hix : i = x
· subst i
simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of, Pi.single_eq_same, map_one, delta]
· simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of, Pi.single_eq_of_ne hix, map_zero, delta]
have hdelta_eq :
delta = finiteFoxStageDerivativeVector (X := X) N n :=
finiteFoxStageDerivativeVector_unique (X := X) N n delta hdelta hbasis
exact (congrFun hdelta_eq w).symmProof. 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. 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. 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.
□theorem finiteFoxStageDerivative_eq_discreteReduction
(i : X) (w : FreeGroup X) :
finiteFoxStageDerivative (X := X) N n i w =
finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w i)The comparison between the finite-stage derivative and the ordinary relative Fox derivative holds componentwise.
Show proof
by
have h := congrFun
(finiteFoxStageDerivativeVector_eq_discreteReduction (X := X) N n w) i
simpa [finiteFoxStageDerivative] using hProof. 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\). 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. 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 exists_eq_nsmul_relFreeFoxDeriv_of_finiteFoxStageDerivativeVector_eq_zero
{n : ℕ} (hn : 0 < n) (w : FreeGroup X)
(hder : finiteFoxStageDerivativeVector (X := X) N n w = 0) :
∃ y : X → GroupRing (finiteFoxStageTargetQuotient (X := X) N),
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = n • yOne finite-stage derivative-vector vanishing says that the ordinary integral relative Fox derivative vector is divisible by the coefficient modulus.
Show proof
by
classical
have hred :
∀ i : X,
finiteFoxStageGroupRingReduction (X := X) N n
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w i) = 0 := by
intro i
have hcomp :=
congrFun (finiteFoxStageDerivativeVector_eq_discreteReduction (X := X) N n w) i
have hzero := congrFun hder i
exact hcomp.symm.trans hzero
choose y hy using fun i =>
exists_eq_nsmul_of_finiteFoxStageGroupRingReduction_eq_zero (X := X) N hn
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w i)
(hred i)
refine ⟨y, ?_⟩
funext i
exact hy iProof. 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. 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. 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.
□theorem exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero
[Fintype X] {n : ℕ} (hn : 0 < n) (w : FreeGroup X)
(hres : residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
∃ y : X → GroupRing (finiteFoxStageTargetQuotient (X := X) N),
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = n • yResidue-universal version of one-modulus divisibility for the ordinary integral relative Fox derivative vector.
Show proof
by
exact
exists_eq_nsmul_relFreeFoxDeriv_of_finiteFoxStageDerivativeVector_eq_zero
(X := X) N hn w
((finiteFoxStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
(X := X) N n w).2 hres)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. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_forall_finiteFoxStageDerivative_eq_zero
(w : FreeGroup X)
(hder :
∀ n : ℕ, 0 < n →
∀ i : X, finiteFoxStageDerivative (X := X) N n i w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = 0If every positive finite-stage derivative vanishes, then the ordinary integral relative Fox derivative vanishes.
Show proof
by
funext i
apply groupRing_eq_zero_of_forall_finiteFoxStageGroupRingReduction_eq_zero
(X := X) N
intro n hn
exact
(finiteFoxStageDerivative_eq_discreteReduction (X := X) N n i w).symm.trans
(hder n hn i)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\). 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. 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 relFreeFoxDeriv_eq_zero_of_forall_finiteFoxStageDerivative_primePow_eq_zero
(p : ℕ) [Fact (Nat.Prime p)] (w : FreeGroup X)
(hder :
∀ k : ℕ,
∀ i : X, finiteFoxStageDerivative (X := X) N (p ^ k) i w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = 0If every \(p^k\) finite-stage derivative vanishes, then the ordinary integral relative Fox derivative vanishes.
Show proof
by
funext i
apply groupRing_eq_zero_of_forall_finiteFoxStageGroupRingReduction_primePow_eq_zero
(X := X) N p
intro k
exact
(finiteFoxStageDerivative_eq_discreteReduction (X := X) N (p ^ k) i w).symm.trans
(hder k i)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\). 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. 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 zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
(i : X) (w : FreeGroup X)
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)))Projecting the completed \(\mathbb{Z}_C\) derivative to a finite pro-\(C\) target stage gives the stage map applied to the reduced ordinary relative Fox derivative.
Show proof
by
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
rw [zcFreeGroupFoxDerivative_finiteStageProjection C N j i w]
rw [finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]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. 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 zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
(w : FreeGroup X)
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
(fun i : X =>
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
fun i : X =>
letI : Fact (0 < j.1.modulus)Vector-valued form of the discrete-to-completed projection comparison.
Show proof
⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
funext i
exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
(C := C) (X := X) N i w jProof. 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. 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 zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction
(i : X)
(delta : FreeGroup X →
ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N))
(hprojection : ∀ w
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w) =
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)))) :
delta = zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) iThe completed \(\mathbb{Z}_C\) component derivative is uniquely determined by the finite-stage projections of the ordinary relative Fox derivative after coefficient reduction.
Show proof
by
refine zcFreeGroupFoxDerivative_unique_finiteStageProjection
(C := C) (X := X) N i delta ?_
intro w j
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
rw [hprojection w j]
rw [← finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]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. 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. 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.
□theorem existsUnique_zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
(i : X) :
∃! delta : FreeGroup X →
ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N),
∀ w
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w) =
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)))Existence and uniqueness of the completed \(\mathbb{Z}_C\) component derivative characterized by the finite-stage projections of the reduced ordinary relative Fox derivative.
Show proof
by
refine ⟨zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i, ?_, ?_⟩
· intro w j
exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
(C := C) (X := X) N i w j
· intro delta hprojection
exact zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction
(C := C) (X := X) N i delta hprojectionProof. 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. 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 zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction
(delta : FreeGroup X →
ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N))
(hprojection : ∀ w
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
(fun i : X =>
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w i)) =
fun i : X =>
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) :
delta = zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N)The completed \(\mathbb{Z}_C\) derivative vector is uniquely determined by the finite-stage projections of the ordinary relative Fox derivative after coefficient reduction.
Show proof
by
refine zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection
(C := C) (X := X) N delta ?_
intro w j
funext i
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
have hcoord := congrFun (hprojection w j) i
rw [hcoord]
rw [← finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]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. 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. 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.
□theorem existsUnique_zcFreeFoxDerivVec_finiteStageProj_discreteReduction :
∃! delta : FreeGroup X →
ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N),
∀ w
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
(fun i : X =>
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(delta w i)) =
fun i : X =>
letI : Fact (0 < j.1.modulus)Existence and uniqueness of the completed \(\mathbb{Z}_C\) derivative vector characterized by the finite-stage projections of the reduced ordinary relative Fox derivative.
Show proof
⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
refine ⟨zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N), ?_, ?_⟩
· intro w j
exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
(C := C) (X := X) N w j
· intro delta hprojection
exact zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction
(C := C) (X := X) N delta hprojectionProof. 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. 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 zcFreeGroupFoxDerivative_fundFormula_finiteStageProj_discreteReduction
[Fintype X]
(w : FreeGroup X)
(j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w) =
∑ i : X,
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) *
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcGroupLike C (zcFiniteStageTarget X N)
(QuotientGroup.mk' N (FreeGroup.of i)) - 1)Projecting the completed Fox-Euler formula and reducing the coefficients identifies the derivative coordinates with the ordinary relative Fox derivative.
Show proof
by
rw [zcFreeGroupFoxDerivative_fundamental_formula_finiteStageProjection_stageMap
(C := C) (X := X) N w j]
apply Finset.sum_congr rfl
intro i hi
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
rw [finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]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. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
[DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
[Finite (finiteFoxStageTargetQuotient (X := X) N)]
(w : FreeGroup X)
(hw :
zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
(QuotientGroup.mk' N) w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = 0Show proof
by
apply relFreeFoxDeriv_eq_zero_of_forall_finiteFoxStageDerivative_eq_zero
(X := X) N w
intro n hn i
let j : ProCGroups.Completion.ProCIntegerIndex
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}) :=
ProCGroups.Completion.ProCIntegerIndex.ofAllFiniteModulus n hn
have hjmod : j.modulus = n := rfl
have hCtarget :
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
(finiteFoxStageTargetQuotient (X := X) N) := by
exact (inferInstance :
Finite (finiteFoxStageTargetQuotient (X := X) N))
have hcomponent :
zcFreeGroupFoxDerivative
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
(QuotientGroup.mk' N) i w = 0 := by
simpa [zcFreeGroupFoxDerivative] using congrFun hw i
simpa [j, hjmod] using
finiteFoxStageDerivative_eq_zero_of_zcFreeGroupFoxDerivative_eq_zero
(C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
(X := X) N
(hIso := ProCGroups.FiniteGroupClass.allFinite_isomClosed)
(hCtarget := hCtarget)
j i hcomponentProof. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite
[DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
[Finite (finiteFoxStageTargetQuotient (X := X) N)]
(w : FreeGroup X)
(hw :
zcUniversalDifferential
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
(QuotientGroup.mk' N) w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = 0Show proof
by
exact
relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
(X := X) N w
(zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
(QuotientGroup.mk' N) hw)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. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
(p : ℕ) [Fact (Nat.Prime p)]
[DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
(hCtarget :
ProCGroups.FiniteGroupClass.pGroup p
(finiteFoxStageTargetQuotient (X := X) N))
(w : FreeGroup X)
(hw :
zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
(QuotientGroup.mk' N) w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = 0Show proof
by
apply relFreeFoxDeriv_eq_zero_of_forall_finiteFoxStageDerivative_primePow_eq_zero
(X := X) N p w
intro k i
let j : ProCGroups.Completion.ProCIntegerIndex
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}) :=
ProCGroups.Completion.ProCIntegerIndex.pGroupPower p k
have hjmod : j.modulus = p ^ k := rfl
have hcomponent :
zcFreeGroupFoxDerivative
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
(QuotientGroup.mk' N) i w = 0 := by
simpa [zcFreeGroupFoxDerivative] using congrFun hw i
simpa [j, hjmod] using
finiteFoxStageDerivative_eq_zero_of_zcFreeGroupFoxDerivative_eq_zero
(C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
(X := X) N
(hIso := (ProCGroups.FiniteGroupClass.pGroup_formation p).isomClosed)
(hCtarget := hCtarget)
j i hcomponentProof. 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. 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.
□theorem relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup
(p : ℕ) [Fact (Nat.Prime p)]
[DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
(hCtarget :
ProCGroups.FiniteGroupClass.pGroup p
(finiteFoxStageTargetQuotient (X := X) N))
(w : FreeGroup X)
(hw :
zcUniversalDifferential
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
(QuotientGroup.mk' N) w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative
(H := finiteFoxStageTargetQuotient (X := X) N)
X (QuotientGroup.mk' N) w = 0Show proof
by
exact
relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
(X := X) N p hCtarget w
(zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
(QuotientGroup.mk' N) hw)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. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj
[DiscreteTopology H] [Finite H]
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
(w : FreeGroup X)
(hw :
zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
ψ w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0Show proof
by
let N : Subgroup (FreeGroup X) := ψ.ker
let Q : Type u := finiteFoxStageTargetQuotient (X := X) N
letI : TopologicalSpace Q := ⊥
letI : DiscreteTopology Q := ⟨rfl⟩
letI : IsTopologicalGroup Q := inferInstance
let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
letI : Finite Q := Finite.of_injective e e.injective
let q : FreeGroup X →* Q := QuotientGroup.mk' N
have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
(QuotientGroup.mk' ψ.ker g) = ψ g
rfl
let eSymm : H →ₜ* Q :=
{ toMonoidHom := e.symm.toMonoidHom
continuous_toFun := continuous_of_discreteTopology }
have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
apply MonoidHom.ext
intro g
apply e.injective
change e (e.symm (ψ g)) = e (q g)
simpa using (he_apply g).symm
have hvecQ :
zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
q w = 0 := by
have htarget :=
zcFreeGroupFoxDerivativeVector_mapTarget
(C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
ProCGroups.FiniteGroupClass.allFinite_hereditary ψ eSymm w
rw [hcompSymm] at htarget
rw [htarget, hw]
rfl
have hq :
FoxCalculus.relativeFreeGroupFoxDerivative (H := Q) X q w = 0 :=
relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
(X := X) N w hvecQ
have hcomp : e.toMonoidHom.comp q = ψ := by
apply MonoidHom.ext
intro g
exact he_apply g
have hnat :=
FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
(H := Q) (K := H) q e.toMonoidHom w
rw [hcomp] at hnat
rw [hnat, hq]
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. 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. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. 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. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj
[DiscreteTopology H] [Finite H]
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
(w : FreeGroup X)
(hw :
zcUniversalDifferential
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
ψ w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0Show proof
relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj
(X := X) ψ hψ w
(zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
ψ hw)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. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj
(p : ℕ) [Fact (Nat.Prime p)]
[DiscreteTopology H]
(hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
(w : FreeGroup X)
(hw :
zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
ψ w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0Show proof
by
let N : Subgroup (FreeGroup X) := ψ.ker
let Q : Type u := finiteFoxStageTargetQuotient (X := X) N
letI : TopologicalSpace Q := ⊥
letI : DiscreteTopology Q := ⟨rfl⟩
letI : IsTopologicalGroup Q := inferInstance
let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
let q : FreeGroup X →* Q := QuotientGroup.mk' N
have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
(QuotientGroup.mk' ψ.ker g) = ψ g
rfl
let eSymm : H →ₜ* Q :=
{ toMonoidHom := e.symm.toMonoidHom
continuous_toFun := continuous_of_discreteTopology }
have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
apply MonoidHom.ext
intro g
apply e.injective
change e (e.symm (ψ g)) = e (q g)
simpa using (he_apply g).symm
have hQtarget :
ProCGroups.FiniteGroupClass.pGroup p Q :=
ProCGroups.FiniteGroupClass.IsomClosed.of_mulEquiv
(ProCGroups.FiniteGroupClass.pGroup_formation p).isomClosed
e.symm hCtarget
have hvecQ :
zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
q w = 0 := by
have htarget :=
zcFreeGroupFoxDerivativeVector_mapTarget
(C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
(ProCGroups.FiniteGroupClass.pGroup_hereditary p) ψ eSymm w
rw [hcompSymm] at htarget
rw [htarget, hw]
rfl
have hq :
FoxCalculus.relativeFreeGroupFoxDerivative (H := Q) X q w = 0 :=
relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
(X := X) N p hQtarget w hvecQ
have hcomp : e.toMonoidHom.comp q = ψ := by
apply MonoidHom.ext
intro g
exact he_apply g
have hnat :=
FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
(H := Q) (K := H) q e.toMonoidHom w
rw [hcomp] at hnat
rw [hnat, hq]
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. 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. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. 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. 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. 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.
□theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj
(p : ℕ) [Fact (Nat.Prime p)]
[DiscreteTopology H]
(hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
(w : FreeGroup X)
(hw :
zcUniversalDifferential
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
ψ w = 0) :
FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0Show proof
relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj
(X := X) p hCtarget ψ hψ w
(zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
ψ hw)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. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. 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. 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.
□