Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential
ProCGroups/FoxDifferential

ProCGroups.FoxDifferential

4 sections | 271 files | 2956 declarations

Fox differentials and Fox coordinates for free groups, group rings, finite algebraic stages, and profinite completions. The library includes bundled crossed homomorphisms, universal differential modules, Fox boundaries, Jacobians, completed derivatives, and right-derivative formulas.

The canonical APIs are the bundled CrossedHom and ScalarCrossedHom constructions and the foxAlgebraicStage* finite stages. The universal construction's final topology and the locally installed free-pro-\(C\) coordinate topology are distinct; neither is called a completion without a comparison theorem.

This Pro-C Groups aggregate layer may depend on the base ProCGroups modules and the ProCGroups.ReidemeisterSchreier and ProCGroups.CompletedGroupAlgebra layers. It also owns the reusable Fox-coordinate, Magnus, and relation-reflection lemmas used by the Crowell exact-sequence assembly. Application-level exact sequences are imported by ProCGroups.CrowellExactSequence.

imports
Imported by

Common

7 files | 177 declarations | 121 Theorems | 43 Definitions | 4 Abbreviations | 1 Structure | 8 Instances
This module defines crossed homomorphisms for an additive group action and their scalar-character specialization. It supplies the Fox product, inverse, conjugation, commutator, ...

Completed

235 files | 2437 declarations | 1708 Theorems | 481 Definitions | 78 Abbreviations | 4 Structures | 166 Instances
This module formalizes completed Fox coordinates for profinite groups.

Discrete

26 files | 317 declarations | 206 Theorems | 92 Definitions | 18 Abbreviations | 1 Instance
This module formalizes the discrete Fox calculus.

RightDerivative

3 files | 25 declarations | 18 Theorems | 2 Definitions | 1 Structure | 4 Instances
This compatibility-free root collects the geometric-series and semidirect-product constructions used by right Fox calculus. Right differentials themselves use the general `Cross...