FoxDifferential.Common.CrossedDifferential
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
import
- Mathlib.Algebra.Group.Commutator
- Mathlib.Algebra.Group.Subgroup.Lattice
- Mathlib.Algebra.Module.BigOperators
- Mathlib.Algebra.Module.LinearMap.Basic
def IsCrossedDifferential
{R G A : Type*} [Semiring R] [Group G] [AddCommMonoid A] [Module R A]
(coeff : G →* R) (delta : G → A) : Prop :=
∀ g h, delta (g * h) = delta g + coeff g • delta hA crossed differential with coefficient homomorphism \(\mathrm{coeff}:G\to R\), viewed multiplicatively. The rule is the Fox Leibniz rule \(\delta(gh)=\delta(g)+\mathrm{coeff}(g)\,\delta(h)\).
theorem zero :
IsCrossedDifferential coeff (fun _ : G => (0 : A))The zero map is a crossed differential.
Show proof
by
intro g h
simp only [smul_zero, add_zero]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 add {delta epsilon : G → A}
(hdelta : IsCrossedDifferential coeff delta)
(hepsilon : IsCrossedDifferential coeff epsilon) :
IsCrossedDifferential coeff (fun g => delta g + epsilon g)Crossed differentials with the same coefficient homomorphism are closed under addition.
Show proof
by
intro g h
change delta (g * h) + epsilon (g * h) =
delta g + epsilon g + coeff g • (delta h + epsilon h)
rw [hdelta g h, hepsilon g h]
simp only [add_left_comm, add_assoc, smul_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.
□theorem neg (hdelta : IsCrossedDifferential coeff delta) :
IsCrossedDifferential coeff (fun g => -delta g)Crossed differentials are closed under negation.
Show proof
by
intro g h
change -delta (g * h) = -delta g + coeff g • -delta h
rw [hdelta g h]
simp only [neg_add_rev, add_comm, smul_neg]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 sub {delta epsilon : G → A}
(hdelta : IsCrossedDifferential coeff delta)
(hepsilon : IsCrossedDifferential coeff epsilon) :
IsCrossedDifferential coeff (fun g => delta g - epsilon g)Crossed differentials with the same coefficient homomorphism are closed under subtraction.
Show proof
by
simpa [sub_eq_add_neg] using add hdelta (neg hepsilon)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_linear {B : Type*} [AddCommGroup B] [Module R B]
(hdelta : IsCrossedDifferential coeff delta) (f : A →ₗ[R] B) :
IsCrossedDifferential coeff (fun g => f (delta g))A linear map sends crossed differentials to crossed differentials.
Show proof
by
intro g h
change f (delta (g * h)) = f (delta g) + coeff g • f (delta h)
rw [hdelta g h]
simp only [map_add, map_smul]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 comp_monoidHom {K : Type*} [Group K]
(hdelta : IsCrossedDifferential coeff delta) (φ : K →* G) :
IsCrossedDifferential (coeff.comp φ) (fun k : K => delta (φ k))Pulling a crossed differential back along a group homomorphism is a crossed differential.
Show proof
by
intro g h
simpa [MonoidHom.comp_apply, map_mul] using hdelta (φ 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 restrictTrivialSubgroupAddMonoidHom
(hdelta : IsCrossedDifferential coeff delta) (N : Subgroup G)
(hN : ∀ n : N, coeff n = 1) :
Additive N →+ A where
toFun x := delta ((Additive.toMul x : N) : G)
map_zero' := by
change delta (1 : G) = 0
have h := hdelta 1 1
rw [map_one, one_smul] at h
have h' := congrArg (fun z : A => z - delta 1) h
have hzero : 0 = delta 1 := by
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
simpa using hzero.symm
map_add' x y := by
change delta (((Additive.toMul x : N) * (Additive.toMul y : N) : N) : G) =
delta ((Additive.toMul x : N) : G) + delta ((Additive.toMul y : N) : G)
have h :=
hdelta ((Additive.toMul x : N) : G) ((Additive.toMul y : N) : G)
simpa [hN (Additive.toMul x)] using h
@[simp]Restricting a crossed differential to any subgroup on which the coefficient homomorphism is trivial gives an ordinary additive homomorphism.
theorem restrictTrivialSubgroupAddMonoidHom_apply
(hdelta : IsCrossedDifferential coeff delta) (N : Subgroup G)
(hN : ∀ n : N, coeff n = 1) (g : N) :
restrictTrivialSubgroupAddMonoidHom hdelta N hN (Additive.ofMul g) = delta gThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
rflProof. 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 one (hdelta : IsCrossedDifferential coeff delta) :
delta 1 = 0A crossed differential vanishes at the identity.
Show proof
by
have h := hdelta 1 1
rw [map_one, one_smul] at h
have h' := congrArg (fun z : A => z - delta 1) h
have hzero : 0 = delta 1 := by
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
simpa using hzero.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 inv (hdelta : IsCrossedDifferential coeff delta) (g : G) :
delta g⁻¹ = -(coeff g⁻¹ • delta g)The inverse rule for a crossed differential.
Show proof
by
have h := hdelta g⁻¹ g
rw [inv_mul_cancel, one hdelta] at h
rw [eq_neg_iff_add_eq_zero]
exact 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 mul (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
delta (g * h) = delta g + coeff g • delta hProduct rule, restated as a theorem for namespaced rewriting.
Show proof
hdelta g 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 inv_mul (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
delta (g⁻¹ * h) =
-(coeff g⁻¹ • delta g) + coeff g⁻¹ • delta hFormula for multiplying by an inverse on the left.
Show proof
by
rw [mul hdelta, inv hdelta]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 mul_inv (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
delta (g * h⁻¹) =
delta g - coeff (g * h⁻¹) • delta hFormula for multiplying by an inverse on the right.
Show proof
by
rw [mul hdelta, inv hdelta]
simp only [smul_neg, smul_smul, map_mul, sub_eq_add_neg]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 div (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
delta (g / h) =
delta g - coeff (g / h) • delta hDivision rule for a crossed differential.
Show proof
by
simpa [div_eq_mul_inv] using mul_inv hdelta g 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 conj (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
delta (g * h * g⁻¹) =
delta g + coeff g • delta h - coeff (g * h * g⁻¹) • delta gConjugation rule for a crossed differential.
Show proof
by
rw [mul_inv hdelta (g * h) g, mul hdelta 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.
□theorem commutator (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
delta ⁅g, h⁆ =
delta g + coeff g • delta h -
coeff (g * h * g⁻¹) • delta g -
coeff ⁅g, h⁆ • delta hCommutator rule for a crossed differential.
Show proof
by
rw [commutatorElement_def, mul_inv hdelta (g * h * g⁻¹) h,
conj hdelta 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.
□theorem eqOn_closure {delta epsilon : G → A}
(hdelta : IsCrossedDifferential coeff delta)
(hepsilon : IsCrossedDifferential coeff epsilon)
{s : Set G} (hs : Set.EqOn delta epsilon s) :
Set.EqOn delta epsilon ((Subgroup.closure s : Subgroup G) : Set G)Two crossed differentials with the same coefficients that agree on a set agree on the abstract subgroup generated by that set.
Show proof
by
intro g hg
exact
Subgroup.closure_induction
(p := fun g _ => delta g = epsilon g)
(fun x hx => hs hx)
(by
change delta 1 = epsilon 1
rw [hdelta.one, hepsilon.one])
(fun x y _ _ hx hy => by
change delta (x * y) = epsilon (x * y)
rw [hdelta.mul x y, hepsilon.mul x y, hx, hy])
(fun x _ hx => by
change delta x⁻¹ = epsilon x⁻¹
rw [hdelta.inv x, hepsilon.inv x, hx])
hgProof. 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 eq_of_closure_eq_top {delta epsilon : G → A}
(hdelta : IsCrossedDifferential coeff delta)
(hepsilon : IsCrossedDifferential coeff epsilon)
{s : Set G} (hsgen : Subgroup.closure s = ⊤)
(hs : Set.EqOn delta epsilon s) :
delta = epsilonCrossed differentials with the same coefficients are determined by a generating set.
Show proof
by
funext g
exact (eqOn_closure hdelta hepsilon hs) (by simp only [hsgen, Subgroup.coe_top, Set.mem_univ])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 pow (hdelta : IsCrossedDifferential coeff delta) (g : G) (n : ℕ) :
delta (g ^ n) =
(Finset.range n).sum (fun k => coeff (g ^ k) • delta g)Positive power rule for a crossed differential.
Show proof
by
induction n with
| zero =>
simp only [pow_zero, one hdelta, Finset.range_zero, map_pow, Finset.sum_empty]
| succ n ih =>
rw [pow_succ, hdelta, ih]
simp only [map_pow, Finset.sum_range_succ]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 pow_smul_sum (hdelta : IsCrossedDifferential coeff delta) (g : G) (n : ℕ) :
delta (g ^ n) =
((Finset.range n).sum (fun k => coeff (g ^ k))) • delta gPositive power rule with the coefficient sum factored out.
Show proof
by
rw [pow hdelta g n]
simp only [map_pow, Finset.sum_smul]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 inv_pow (hdelta : IsCrossedDifferential coeff delta) (g : G) (n : ℕ) :
delta (g⁻¹ ^ n) =
(Finset.range n).sum (fun k =>
coeff (g⁻¹ ^ k) • (-(coeff g⁻¹ • delta g)))Positive power rule applied to the inverse element.
Show proof
by
rw [pow hdelta g⁻¹ n, inv hdelta]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.
□