Yamaguchi Lean 4 Library
FoxDifferential.Completed.DifferentialModule
FoxDifferential/Completed/DifferentialModule

FoxDifferential.Completed.DifferentialModule

3 sections | 13 files | 44 declarations

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

Identity

1 files | 11 declarations | 5 Theorem | 6 Definition
The identity completed-group-algebra open subgroup used for the identity quotient stage.

Map

6 files | 20 declarations | 15 Theorem | 5 Definition
The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.

TargetQuotient

6 files | 13 declarations | 11 Theorem | 2 Definition
The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.