FoxDifferential.RightDerivative.Basic
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
import
structure RightDerivation (G : Type*) [Group G] where
toAddHom : FoxDifferential.GroupRing G →+ FoxDifferential.GroupRing G
map_mul' : ∀ u v : FoxDifferential.GroupRing G,
toAddHom (u * v) =
toAddHom u * v + FoxDifferential.augmentation G u • toAddHom vA right derivation satisfies the right Fox Leibniz rule.
instance instCoeFunRightDerivation : CoeFun (RightDerivation G) (fun _ =>
FoxDifferential.GroupRing G → FoxDifferential.GroupRing G) :=
⟨fun D => D.toAddHom⟩
@[simp]A right derivation is coerced to its underlying function.
theorem map_zero (D : RightDerivation G) : D 0 = 0The right derivation satisfies the corresponding group-ring formula.
Show proof
D.toAddHom.map_zero
@[simp]Proof. 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_add (D : RightDerivation G) (u v : FoxDifferential.GroupRing G) :
D (u + v) = D u + D vA right derivation preserves addition.
Show proof
D.toAddHom.map_add u vProof. 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_mul (D : RightDerivation G) (u v : FoxDifferential.GroupRing G) :
D (u * v) = D u * v + FoxDifferential.augmentation G u • D vA right derivation satisfies the product rule.
Show proof
D.map_mul' u v
@[simp]Proof. 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_one (D : RightDerivation G) : D 1 = 0A right derivation sends the identity element to zero.
Show proof
by
have h := D.map_mul (1 : FoxDifferential.GroupRing G) 1
simp only [mul_one, augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe,
_root_.map_one, one_smul, left_eq_add] at h
exact hProof. 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_inv_groupElement (D : RightDerivation G) (g : G) :
D (MonoidAlgebra.of ℤ G g⁻¹ : FoxDifferential.GroupRing G) =
-D (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G) *
(MonoidAlgebra.of ℤ G g⁻¹ : FoxDifferential.GroupRing G)A right derivation satisfies the inverse formula for group elements.
Show proof
by
have h := D.map_mul
(MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G)
(MonoidAlgebra.of ℤ G g⁻¹ : FoxDifferential.GroupRing G)
have h0 :
D.toAddHom (MonoidAlgebra.single (1 : G) 1 : FoxDifferential.GroupRing G) = 0 := by
change D (1 : FoxDifferential.GroupRing G) = 0
exact D.map_one
simp only [MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_inv_cancel, mul_one, augmentation,
augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
one_smul] at h
rw [h0] at h
simpa [neg_mul] using eq_neg_of_add_eq_zero_right h.symmProof. 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_pow_groupElement (D : RightDerivation G) (g : G) :
∀ n : ℕ,
D (MonoidAlgebra.of ℤ G (g ^ n) : FoxDifferential.GroupRing G) =
D (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G) * geomSeries g n
| 0 => by
simp only [pow_zero, MonoidAlgebra.of_apply, geomSeries, Finset.range_zero, Finset.sum_empty, mul_zero]
change D (1 : FoxDifferential.GroupRing G) = 0
exact D.map_one
| n + 1 => by
rw [pow_succ]
have hmul :
(MonoidAlgebra.of ℤ G (g ^ n * g) : FoxDifferential.GroupRing G) =
(MonoidAlgebra.of ℤ G (g ^ n) : FoxDifferential.GroupRing G) *
MonoidAlgebra.of ℤ G gA right derivation satisfies the power formula for group elements.
Show proof
by
simp only [MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
rw [hmul, map_mul]
rw [map_pow_groupElement D g n]
simp only [MonoidAlgebra.of_apply, mul_assoc, augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe,
RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, mul_one, one_smul,
geomSeries_succ_eq_mul_add_one, mul_add]Proof. 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.
□def groupRingLinearExtension (δ : G → FoxDifferential.GroupRing G) :
FoxDifferential.GroupRing G →ₗ[ℤ] FoxDifferential.GroupRing G :=
Finsupp.linearCombination ℤ δ
@[simp]A right derivation extends linearly to the group ring.
theorem groupRingLinearExtension_single (δ : G → FoxDifferential.GroupRing G) (g : G)
(n : ℤ) :
groupRingLinearExtension δ (MonoidAlgebra.single g n : FoxDifferential.GroupRing G) =
n • δ gThe group-ring linear extension of a right derivation sends a single group element to the right-derivation value on that element.
Show proof
by
exact Finsupp.linearCombination_single ℤ n gProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem groupRingLinearExtension_map_mul
(δ : G → FoxDifferential.GroupRing G)
(hδ : ∀ g h : G, δ (g * h) = δ g * MonoidAlgebra.of ℤ G h + δ h)
(u v : FoxDifferential.GroupRing G) :
groupRingLinearExtension δ (u * v) =
groupRingLinearExtension δ u * v +
FoxDifferential.augmentation G u • groupRingLinearExtension δ vA right derivation satisfies the product rule.
Show proof
by
classical
induction u using Finsupp.induction_linear with
| zero =>
simp only [groupRingLinearExtension, zero_mul, _root_.map_zero, zero_smul, add_zero]
| add u₁ u₂ hu₁ hu₂ =>
simp only [add_mul, _root_.map_add, hu₁, zsmul_eq_mul, add_comm, hu₂, add_left_comm, add_assoc, Int.cast_add]
| single g n =>
induction v using Finsupp.induction_linear with
| zero =>
simp only [groupRingLinearExtension, mul_zero, _root_.map_zero, smul_zero, add_zero]
| add v₁ v₂ hv₁ hv₂ =>
simp only [mul_add, _root_.map_add, hv₁, groupRingLinearExtension_single, zsmul_eq_mul, hv₂, add_left_comm,
add_assoc, smul_add]
| single h m =>
rw [MonoidAlgebra.single_mul_single]
rw [groupRingLinearExtension_single, groupRingLinearExtension_single,
groupRingLinearExtension_single]
rw [hδ]
simp only [MonoidAlgebra.of_apply, smul_add, zsmul_eq_mul, Int.cast_mul, augmentation, augmentationAlgHom,
AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, mul_one]
rw [show (Finsupp.single h m : FoxDifferential.GroupRing G) =
algebraMap ℤ (FoxDifferential.GroupRing G) m *
(MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G) by
simpa using (MonoidAlgebra.single_eq_algebraMap_mul_of (M := G) h m)]
change ((n : FoxDifferential.GroupRing G) * (m : FoxDifferential.GroupRing G)) *
(δ g * (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)) +
((n : FoxDifferential.GroupRing G) * (m : FoxDifferential.GroupRing G)) * δ h =
(n : FoxDifferential.GroupRing G) * δ g *
((m : FoxDifferential.GroupRing G) *
(MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)) +
(n : FoxDifferential.GroupRing G) *
((m : FoxDifferential.GroupRing G) * δ h)
rw [mul_assoc (n : FoxDifferential.GroupRing G) (δ g)
((m : FoxDifferential.GroupRing G) *
(MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G))]
rw [← mul_assoc (δ g) (m : FoxDifferential.GroupRing G)
(MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)]
rw [(Int.cast_commute m (δ g)).eq.symm]
rw [mul_assoc (m : FoxDifferential.GroupRing G) (δ g)
(MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)]
rw [← mul_assoc (n : FoxDifferential.GroupRing G) (m : FoxDifferential.GroupRing G)
(δ g * (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G))]
rw [← mul_assoc (n : FoxDifferential.GroupRing G) (m : FoxDifferential.GroupRing G)
(δ h)]Proof. 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.
□def ofGroupMap (δ : G → FoxDifferential.GroupRing G)
(hδ : ∀ g h : G, δ (g * h) = δ g * MonoidAlgebra.of ℤ G h + δ h) :
RightDerivation G where
toAddHom := (groupRingLinearExtension δ).toAddMonoidHom
map_mul' := groupRingLinearExtension_map_mul δ hδThe group-map construction defines a right derivation.