FoxDifferential.Discrete.FreeExpansion
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
def freeCrossedDifferentialExpansion (w : FreeGroup X) : A :=
∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X ψ w x • basisValue xPrescribed values on the free generators determine the Fox-coordinate expansion.
theorem freeCrossedDifferentialExpansion_one :
freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue 1 = 0The Fox-coordinate expansion of the identity word is zero.
Show proof
by
simp only [freeCrossedDifferentialExpansion, relativeFreeGroupFoxDerivative_one, Pi.zero_apply, zero_smul,
Finset.sum_const_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 freeCrossedDifferentialExpansion_of (x : X) :
freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue (FreeGroup.of x) =
basisValue xThe Fox-coordinate expansion of a free generator returns its prescribed basis value.
Show proof
by
rw [freeCrossedDifferentialExpansion]
rw [relativeFreeGroupFoxDerivative_of]
rw [Finset.sum_eq_single x]
· simp only [Pi.single_eq_same, one_smul]
· intro y _ hy
simp only [Pi.single_eq_of_ne hy, zero_smul]
· simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]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 freeCrossedDifferentialExpansion_isDifferentialMap :
IsDifferentialMap (A := A) ψ
(freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue)The Fox-coordinate expansion is a crossed differential.
Show proof
by
intro u v
rw [freeCrossedDifferentialExpansion, freeCrossedDifferentialExpansion]
change
(∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X ψ (u * v) x • basisValue x) =
(∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X ψ u x • basisValue x) +
(MonoidAlgebra.of ℤ H (ψ u) : GroupRing H) •
(∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X ψ v x • basisValue x)
rw [relativeFreeGroupFoxDerivative_mul]
simp only [MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_smul, Finset.sum_add_distrib,
Finset.smul_sum, smul_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 freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion (w : FreeGroup X) :
freeCrossedDifferentialWithCoeff (A := A) (groupRingScalar ψ) basisValue w =
freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue wThe coefficient-generic free crossed differential over a group ring is the Fox-coordinate expansion of its generator values.
Show proof
by
have h :=
freeCrossedDifferentialWithCoeff_unique (A := A) (groupRingScalar ψ) basisValue
(freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue)
(freeCrossedDifferentialExpansion_isDifferentialMap (H := H) (A := A) ψ basisValue)
(freeCrossedDifferentialExpansion_of (H := H) (A := A) ψ basisValue)
exact congrFun h.symm wProof. 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 freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
(w : FreeGroup X) :
freeCrossedDifferentialWithCoeffCoordinates
(X := X) (groupRingScalar ψ) w =
relativeFreeGroupFoxDerivative (H := H) X ψ wThe coefficient-generic coordinate crossed differential specializes to the usual relative Fox derivative over a group ring.
Show proof
by
exact congrFun (relativeFreeGroupFoxDerivative_unique (H := H) X ψ
(freeCrossedDifferentialWithCoeffCoordinates (X := X) (groupRingScalar ψ))
(freeCrossedDifferentialWithCoeffCoordinates_isCrossedDifferential
(X := X) (groupRingScalar ψ))
(freeCrossedDifferentialWithCoeffCoordinates_of
(X := X) (groupRingScalar ψ))) wProof. 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 crossedDifferential_comp_relativeFreeGroupFoxDerivative
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(delta : FreeGroup Y → A) (hdelta : IsDifferentialMap (A := A) ψ delta)
(w : FreeGroup X) :
delta (φ w) =
∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
delta (φ (FreeGroup.of x))Abstract Fox chain rule for an arbitrary crossed differential.
Show proof
by
calc
delta (φ w) =
freeCrossedDifferentialWithCoeffExpansion
(X := X) (groupRingScalar (ψ.comp φ))
(fun x : X => delta (φ (FreeGroup.of x))) w := by
exact freeCrossedDifferentialWithCoeff_comp_expansion
(X := X) (Y := Y) (B := A)
(groupRingScalar ψ) φ delta hdelta w
_ =
∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
delta (φ (FreeGroup.of x)) := by
rw [freeCrossedDifferentialWithCoeffExpansion,
freeCrossedDifferentialWithCoeffExpansionLinearMap_apply,
freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
(H := H) (X := X) (ψ.comp φ) w]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.
□