ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness

5 sections | 5 files | 20 declarations

This aggregate re-exports the following parts of the Fox differential API:

Completed.FreeProC.Uniqueness.Derivative - Completed.FreeProC.Uniqueness.Existence - Completed.FreeProC.Uniqueness.Lift - Completed.FreeProC.Uniqueness.Morphism - Completed.FreeProC.Uniqueness.SemidirectHom

imports

Imported by

ProCGroups.FoxDifferential.Completed.FreeProC

Derivative

1 file | 4 declarations | 4 Theorems

The principal declarations in this module are: - `freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect` Any continuous semidirect lift with the prescribed generator compo...

Existence

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `existsUnique_freeProCZCCompletedFoxSemidirectLift` Existence and uniqueness of the continuous completed Fox semidirect lift fro...

Lift

1 file | 6 declarations | 6 Theorems

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectLift_unique` Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique ...

Morphism

1 file | 4 declarations | 4 Theorems

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectLiftMorphism_unique` Categorical completed Fox semidirect morphisms from a free pro-\(C\) sourc...

SemidirectHom

1 file | 4 declarations | 3 Theorems | 1 Definition

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential` A completed crossed differential and its coefficient homomorphism com...