ModuleNaturality.lean
Nyll.ProCGroups.FoxDifferential.Discrete.Naturality
4 declarations indexed from sourceView source ↗ Module documentation
Fox differential: discrete — naturality
The principal declarations in this module are:
relativeFreeFoxCoordinatesMap
A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward.
relativeFreeFoxCoordinatesMap_apply
Pushing a relative Fox-coordinate vector along φ applies groupRingMap φ to the selected coordinate.
relativeFreeGroupFoxDerivative_mapDomain
Relative Fox derivatives are natural under coefficient push-forward.
relativeFreeGroupFoxDerivative_mapDomain_apply
Component form of coefficient-push-forward naturality for relative free-group Fox derivatives.
Declarations
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesMap
DocumentationA homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
namespace FoxCalculus
universe u v w
variable {H : Type v} {K : Type w} [Group H] [Group K]
variable {X : Type u} [DecidableEq X]
variable (ψ : FreeGroup X →* H) (φ : H →* K)
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesMap_apply
DocumentationPushing a relative Fox-coordinate vector along φ applies groupRingMap φ to the selected coordinate.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
namespace FoxCalculus
universe u v w
variable {H : Type v} {K : Type w} [Group H] [Group K]
variable {X : Type u} [DecidableEq X]
variable (ψ : FreeGroup X →* H) (φ : H →* K)
omit [DecidableEq X] in
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
DocumentationRelative Fox derivatives are natural under coefficient push-forward.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
namespace FoxCalculus
universe u v w
variable {H : Type v} {K : Type w} [Group H] [Group K]
variable {X : Type u} [DecidableEq X]
variable (ψ : FreeGroup X →* H) (φ : H →* K)
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain_apply
DocumentationComponent form of coefficient-push-forward naturality for relative free-group Fox derivatives.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
namespace FoxCalculus
universe u v w
variable {H : Type v} {K : Type w} [Group H] [Group K]
variable {X : Type u} [DecidableEq X]
variable (ψ : FreeGroup X →* H) (φ : H →* K)