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

ProCGroups.FoxDifferential.Completed

9 sections | 234 files | 2437 declarations

This module formalizes completed Fox coordinates for profinite groups.

imports
Imported by

CoefficientRings

52 files | 427 declarations | 245 Theorems | 74 Definitions | 30 Abbreviations | 78 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.CoefficientRings.AugmentationIdealPrimePower` - `Completed.CoefficientRings.CompletedGrou...

Comparison

6 files | 87 declarations | 76 Theorems | 6 Definitions | 4 Abbreviations | 1 Structure
This aggregate re-exports the following parts of the Fox differential API: - `Completed.Comparison.DiscreteCompletion` - `Completed.Comparison.FiniteStage` - `Completed.Comparis...

Continuous

32 files | 679 declarations | 487 Theorems | 138 Definitions | 14 Abbreviations | 1 Structure | 39 Instances
The principal declarations in this module are: - `allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse` The named inverse linear map for the completed Fox-Jacobi...

DifferentialModule

14 files | 44 declarations | 31 Theorems | 13 Definitions
This aggregate re-exports the following parts of the Fox differential API: - `Completed.DifferentialModule.Identity` - `Completed.DifferentialModule.Map` - `Completed.Differenti...

FiniteStage

80 files | 553 declarations | 397 Theorems | 112 Definitions | 15 Abbreviations | 1 Structure | 28 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.Basic` - `Completed.FiniteStage.Bifiltered` - `Completed.FiniteStage.Boundary...

FreeProC

28 files | 332 declarations | 259 Theorems | 67 Definitions | 2 Abbreviations | 4 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.FreeProC.BifilteredCoefficientStageProjection` - `Completed.FreeProC.BifilteredStageProje...

ProCIntegerCoefficients

13 files | 246 declarations | 170 Theorems | 53 Definitions | 10 Abbreviations | 13 Instances
This aggregate re-exports the following parts of the Fox differential API: - `Completed.ProCIntegerCoefficients.Augmentation` - `Completed.ProCIntegerCoefficients.AugmentationId...

Residue

8 files | 42 declarations | 25 Theorems | 14 Definitions | 3 Abbreviations
This aggregate re-exports the following parts of the Fox differential API: - `Completed.Residue.Core` - `Completed.Residue.FreeGroup`

Semidirect

1 file | 27 declarations | 18 Theorems | 4 Definitions | 1 Structure | 4 Instances
The principal declarations in this module are: - `ZCCompletedFoxSemidirect` The completed Fox semidirect target `Z_C[[H]]^X ⋊ H`. - `rightMonoidHom` The right projection from th...