FoxDifferential/RightDerivative/CommutatorFormula.lean
1import FoxDifferential.RightDerivative.IntegerPower
2import Mathlib.Tactic.NoncommRing
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/RightDerivative/CommutatorFormula.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Right Fox derivatives
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable section
21/-- The paper commutator convention `u⁻¹ * v⁻¹ * u * v`, kept local to Fox calculus so that
22metabelian applications depend on `FoxDifferential`, not conversely. -/
24 u⁻¹ * v⁻¹ * u * v
26namespace RightDerivation
28variable {G : Type*} [Group G]
30theorem map_conjugated_groupElement (D : RightDerivation G) (u v : G) :
31 D (MonoidAlgebra.of ℤ G (v⁻¹ * u * v) : FoxDifferential.GroupRing G) =
32 D (MonoidAlgebra.of ℤ G v : FoxDifferential.GroupRing G) *
33 (1 - MonoidAlgebra.of ℤ G (v⁻¹ * u * v)) +
34 D (MonoidAlgebra.of ℤ G u : FoxDifferential.GroupRing G) *
35 MonoidAlgebra.of ℤ G v := by
36 have hmul :
37 (MonoidAlgebra.of ℤ G (v⁻¹ * u * v) : FoxDifferential.GroupRing G) =
38 ((MonoidAlgebra.of ℤ G v⁻¹ : FoxDifferential.GroupRing G) *
39 MonoidAlgebra.of ℤ G u) * MonoidAlgebra.of ℤ G v := by
40 simp only [mul_assoc, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
41 rw [hmul]
42 rw [map_mul, map_mul, map_inv_groupElement]
43 simp only [MonoidAlgebra.of_apply, neg_mul, mul_assoc, MonoidAlgebra.single_mul_single, mul_one, augmentation,
44 augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
45 one_smul, sub_eq_add_neg]
46 rw [add_mul, neg_mul]
47 simp only [mul_assoc, MonoidAlgebra.single_mul_single, mul_one]
48 noncomm_ring
50theorem map_paperComm_groupElement (D : RightDerivation G) (u v : G) :
51 D (MonoidAlgebra.of ℤ G (paperComm u v) : FoxDifferential.GroupRing G) =
52 D (MonoidAlgebra.of ℤ G u : FoxDifferential.GroupRing G) *
54 D (MonoidAlgebra.of ℤ G v : FoxDifferential.GroupRing G) *
55 (1 - MonoidAlgebra.of ℤ G (v⁻¹ * u * v)) := by
56 have hmul :
57 (MonoidAlgebra.of ℤ G (paperComm u v) : FoxDifferential.GroupRing G) =
58 (((MonoidAlgebra.of ℤ G u⁻¹ : FoxDifferential.GroupRing G) *
59 MonoidAlgebra.of ℤ G v⁻¹) * MonoidAlgebra.of ℤ G u) * MonoidAlgebra.of ℤ G v := by
60 simp only [paperComm, mul_assoc, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
61 rw [hmul]
63 simp only [MonoidAlgebra.of_apply, neg_mul, mul_assoc, MonoidAlgebra.single_mul_single, mul_one, augmentation,
64 augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
65 smul_neg, one_smul, add_mul, sub_eq_add_neg]
66 noncomm_ring
70end
72end FoxDifferential