FoxDifferential.RightDerivative.CommutatorFormula
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
import
- FoxDifferential.RightDerivative.IntegerPower
- Mathlib.Tactic.NoncommRing
def paperComm {G : Type*} [Group G] (u v : G) : G :=
u⁻¹ * v⁻¹ * u * vThe paper commutator convention \(u{}^{-1} * v{}^{-1} * u * v\), kept local to Fox calculus so that metabelian applications depend on FoxDifferential, not conversely.
theorem map_conjugated_groupElement (D : RightDerivation G) (u v : G) :
D (MonoidAlgebra.of ℤ G (v⁻¹ * u * v) : FoxDifferential.GroupRing G) =
D (MonoidAlgebra.of ℤ G v : FoxDifferential.GroupRing G) *
(1 - MonoidAlgebra.of ℤ G (v⁻¹ * u * v)) +
D (MonoidAlgebra.of ℤ G u : FoxDifferential.GroupRing G) *
MonoidAlgebra.of ℤ G vThe right derivation satisfies the corresponding group-ring formula.
Show proof
by
have hmul :
(MonoidAlgebra.of ℤ G (v⁻¹ * u * v) : FoxDifferential.GroupRing G) =
((MonoidAlgebra.of ℤ G v⁻¹ : FoxDifferential.GroupRing G) *
MonoidAlgebra.of ℤ G u) * MonoidAlgebra.of ℤ G v := by
simp only [mul_assoc, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
rw [hmul]
rw [map_mul, map_mul, map_inv_groupElement]
simp only [MonoidAlgebra.of_apply, neg_mul, mul_assoc, MonoidAlgebra.single_mul_single, mul_one, augmentation,
augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
one_smul, sub_eq_add_neg]
rw [add_mul, neg_mul]
simp only [mul_assoc, MonoidAlgebra.single_mul_single, mul_one]
noncomm_ringProof. 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.
□theorem map_paperComm_groupElement (D : RightDerivation G) (u v : G) :
D (MonoidAlgebra.of ℤ G (paperComm u v) : FoxDifferential.GroupRing G) =
D (MonoidAlgebra.of ℤ G u : FoxDifferential.GroupRing G) *
(MonoidAlgebra.of ℤ G v - MonoidAlgebra.of ℤ G (paperComm u v)) +
D (MonoidAlgebra.of ℤ G v : FoxDifferential.GroupRing G) *
(1 - MonoidAlgebra.of ℤ G (v⁻¹ * u * v))The right derivation satisfies the corresponding group-ring formula.
Show proof
by
have hmul :
(MonoidAlgebra.of ℤ G (paperComm u v) : FoxDifferential.GroupRing G) =
(((MonoidAlgebra.of ℤ G u⁻¹ : FoxDifferential.GroupRing G) *
MonoidAlgebra.of ℤ G v⁻¹) * MonoidAlgebra.of ℤ G u) * MonoidAlgebra.of ℤ G v := by
simp only [paperComm, mul_assoc, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
rw [hmul]
rw [map_mul, map_mul, map_mul, map_inv_groupElement, map_inv_groupElement]
simp only [MonoidAlgebra.of_apply, neg_mul, mul_assoc, MonoidAlgebra.single_mul_single, mul_one, augmentation,
augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
smul_neg, one_smul, add_mul, sub_eq_add_neg]
noncomm_ringProof. 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.
□