ProCGroups.FoxDifferential.Completed.DifferentialModule.Map

5 sections | 5 files | 20 declarations

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

Completed.DifferentialModule.Map.Comap - Completed.DifferentialModule.Map.GroupLike - Completed.DifferentialModule.Map.Limit - Completed.DifferentialModule.Map.Stage - Completed.DifferentialModule.Map.Surjective

imports

Imported by

ProCGroups.FoxDifferential.Completed.DifferentialModule

Comap

1 file | 7 declarations | 5 Theorems | 2 Definitions

The principal declarations in this module are: - `completedGroupAlgebraComapIndex` The index map that sends a target finite quotient to its pullback finite quotient on the sourc...

GroupLike

1 file | 1 declaration | 1 Theorem

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMap_of` The completed prime-power group-algebra map sends the group-like element of `g` to the g...

Limit

1 file | 3 declarations | 2 Theorems | 1 Definition

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMap` The ring homomorphism on prime-power completed group algebras induced stagewise by a contin...

Stage

1 file | 6 declarations | 5 Theorems | 1 Definition

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMapStage` The finite-stage prime-power group-algebra map induced by the quotient map associated ...

Surjective

1 file | 3 declarations | 2 Theorems | 1 Definition

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMapLiftOfSurjective` A choice of a lift along the surjective completed group-algebra map \(\Lamb...