ModuleSemidirect.lean
Nyll.ProCGroups.FoxDifferential.Discrete.FoxCalculus.Semidirect
2 declarations indexed from sourceView source ↗ Module documentation
Fox differential: discrete — fox calculus — semidirect
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\).
The canonical group-ring scalar action of H on relative Fox-coordinate vectors.
Declarations
FoxDifferential.FoxCalculus.RelativeFreeFoxCoordinates
DocumentationFox-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\).
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
FoxDifferential.FoxCalculus.RelativeFoxAction
DocumentationThe canonical group-ring scalar action of H on relative Fox-coordinate vectors.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)