ProCGroups.FoxDifferential.Discrete.FoxCalculus.Semidirect

2 Abbreviations

The principal declarations in this module are:

RelativeFreeFoxCoordinates Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The coefficients are already pushed forward to \(\mathbb{Z}[H]\); this is the coordinate module which will identify \(A_{\psi}\) with \(\mathbb{Z}[H]^X\) for \(\psi:\mathrm{FreeGroup}(X)\to H\). - RelativeFoxAction The canonical group-ring scalar action of H on relative Fox-coordinate vectors.

import

ProCGroups.FoxDifferential.Discrete.DifferentialModule.Basic

Imported by

Abbreviation FoxDifferential.FoxCalculus.RelativeFreeFoxCoordinates

abbrev RelativeFreeFoxCoordinates : Type _ := X → GroupRing H

Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The coefficients are already pushed forward to \(\mathbb{Z}[H]\); this is the coordinate module which will identify \(A_{\psi}\) with \(\mathbb{Z}[H]^X\) for \(\psi:\mathrm{FreeGroup}(X)\to H\).

Abbreviation FoxDifferential.FoxCalculus.RelativeFoxAction

abbrev RelativeFoxAction :
    H →* Multiplicative (AddAut (RelativeFreeFoxCoordinates (H := H) X)) :=
  scalarCrossedAction (A := RelativeFreeFoxCoordinates (H := H) X)
    (groupRingScalar (MonoidHom.id H))

The canonical group-ring scalar action of H on relative Fox-coordinate vectors.

ProCGroups.FoxDifferential.Discrete.FoxCalculus.Semidirect

Declarations