Source: ProCGroups.FoxDifferential
1import ProCGroups.FoxDifferential.Common
2import ProCGroups.FoxDifferential.Completed
3import ProCGroups.FoxDifferential.Discrete
4import ProCGroups.FoxDifferential.RightDerivative
6/-!
7# Fox differential calculus
9Fox differentials and Fox coordinates for free groups, group rings, finite algebraic stages, and
10profinite completions. The library includes bundled crossed homomorphisms, universal differential
11modules, Fox boundaries, Jacobians, completed derivatives, and right-derivative formulas.
13The canonical APIs are the bundled `CrossedHom` and `ScalarCrossedHom` constructions and the
14`foxAlgebraicStage*` finite stages. The universal construction's final topology and the locally
15installed free-pro-\(C\) coordinate topology are distinct; neither is called a completion without
16a comparison theorem.
18This Pro-C Groups aggregate layer may depend on the base `ProCGroups` modules and the
19`ProCGroups.ReidemeisterSchreier` and `ProCGroups.CompletedGroupAlgebra` layers. It also owns
20the reusable Fox-coordinate, Magnus, and relation-reflection lemmas used by the Crowell
21exact-sequence assembly. Application-level exact sequences are imported by
22`ProCGroups.CrowellExactSequence`.
23-/