ModuleCoordinates.lean
Nyll.ProCGroups.FoxDifferential.Discrete.FoxCalculus.Coordinates
3 declarations indexed from sourceView source ↗ Module documentation
Fox differential: discrete — fox calculus — coordinates
The principal declarations in this module are:
relativeFreeFoxCoordinatesLinearEquivDifferential
The linear equivalence between pushed-forward Fox coordinates and the universal differential module of a finite-rank free group.
relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap
The coordinate map is a left inverse to the coordinate-to-differential map.
relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates
The coordinate-to-differential map is a left inverse to the differential-to-coordinate map.
Declarations
FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap
DocumentationThe coordinate map is a left inverse to the coordinate-to-differential map.
Source context 10 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)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates
DocumentationThe coordinate-to-differential map is a left inverse to the differential-to-coordinate map.
Source context 10 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)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearEquivDifferential
DocumentationThe linear equivalence between pushed-forward Fox coordinates and the universal differential module of a finite-rank free group.
Source context 10 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)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]