Yamaguchi Lean 4 Library
FoxDifferential.Discrete.FoxCalculus
FoxDifferential/Discrete/FoxCalculus

FoxDifferential.Discrete.FoxCalculus

5 sections | 5 files | 44 declarations

This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Boundary

1 files | 10 declarations | 9 Theorem | 1 Definition
The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\).

Coordinates

1 files | 3 declarations | 2 Theorem | 1 Definition
The coordinate map is a left inverse to the coordinate-to-differential map.

Derivative

1 files | 12 declarations | 10 Theorem | 2 Definition
The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\), and whose right component is \(\psi\) itself.

Semidirect

1 files | 13 declarations | 7 Theorem | 1 Abbreviation | 1 Structure | 4 Instance
Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The coefficients are already pushed forward to \(\mathbb{Z}[H]\); this is the coordinate mod...

Universal

1 files | 6 declarations | 4 Theorem | 2 Definition
The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox derivative.