FoxDifferential.RightDerivative.IntegerPower
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
def signedGeomSeries {G : Type*} [Group G] (g : G) : ℤ → FoxDifferential.GroupRing G
| Int.ofNat n => geomSeries g n
| Int.negSucc n => -(MonoidAlgebra.of ℤ G g⁻¹ * geomSeries g⁻¹ (n + 1))The signed geometric series gives the right Fox derivative of an integer power.
theorem map_zpow_groupElement (D : RightDerivation G) (g : G) :
∀ n : ℤ,
D (MonoidAlgebra.of ℤ G (g ^ n) : FoxDifferential.GroupRing G) =
D (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G) * signedGeomSeries g n
| Int.ofNat n => by
simpa [signedGeomSeries] using D.map_pow_groupElement g n
| Int.negSucc n => by
have hpowThe right derivation satisfies the corresponding group-ring formula.
Show proof
D.map_pow_groupElement g⁻¹ (n + 1)
rw [map_inv_groupElement] at hpow
simpa [signedGeomSeries, mul_assoc] using hpowProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□