NYLL
Module

Coordinates.lean

Nyll.ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Coordinates
8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — residue — free group — coordinates

The principal declarations in this module are:

  • residueDifferentialToFreeFoxCoordinates

The linear map from the residue universal module to residue Fox-coordinate vectors.

  • residueFreeFoxCoordinatesLinearMap

The linear map from residue Fox-coordinate vectors to the residue universal module, sending the coordinate basis at \(x\) to \(d_{\psi}(x)\).

  • residueDifferentialToFreeFoxCoordinates_universal

The residue coordinate map sends a universal differential to the residue Fox derivative vector.

  • residueFreeFoxCoordinatesLinearMap_single

The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal residue differential.

Imports1
Imported by2

Declarations

def

residueDifferentialToFreeFoxCoordinates

L42 ↗
FoxDifferential.residueDifferentialToFreeFoxCoordinates
Documentation

The linear map from the residue universal module to residue Fox-coordinate vectors.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
def residueDifferentialToFreeFoxCoordinates (n : ℕ) (ψ : FreeGroup X →* H) :
    ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
      ResidueFreeFoxCoordinates n H X
theorem

residueDifferentialToFreeFoxCoordinates_universal

L52 ↗
FoxDifferential.residueDifferentialToFreeFoxCoordinates_universal
Documentation

The residue coordinate map sends a universal differential to the residue Fox derivative vector.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
omit [Fintype X] in
Lean source · statement
theorem residueDifferentialToFreeFoxCoordinates_universal
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueDifferentialToFreeFoxCoordinates n ψ
        (residueUniversalDifferential n ψ w) =
      residueFreeGroupFoxDerivativeVector n ψ w
def

residueFreeFoxCoordinatesLinearMap

L63 ↗
FoxDifferential.residueFreeFoxCoordinatesLinearMap
Documentation

The linear map from residue Fox-coordinate vectors to the residue universal module, sending the coordinate basis at \(x\) to \(d_{\psi}(x)\).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · full declaration
def residueFreeFoxCoordinatesLinearMap (n : ℕ) (ψ : FreeGroup X →* H) :
    ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H]
      ResidueDifferentialModule n ψ where
  toFun v := ∑ x : X, v x • residueUniversalDifferential n ψ (FreeGroup.of x)
  map_add' := by
    intro v w
    simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
  map_smul' := by
    intro r v
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
theorem

residueFreeFoxCoordinatesLinearMap_single

L79 ↗
FoxDifferential.residueFreeFoxCoordinatesLinearMap_single
Documentation

The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal residue differential.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
theorem residueFreeFoxCoordinatesLinearMap_single
    (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
    residueFreeFoxCoordinatesLinearMap n ψ
        (Pi.single x (1 : ResidueGroupRing n H)) =
      residueUniversalDifferential n ψ (FreeGroup.of x)
theorem

residueFreeFoxCoordinatesLinearMap_derivativeVector

L98 ↗
FoxDifferential.residueFreeFoxCoordinatesLinearMap_derivativeVector
Documentation

The coordinate-to-differential map recovers the universal residue differential from the residue derivative vector.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
theorem residueFreeFoxCoordinatesLinearMap_derivativeVector
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueFreeFoxCoordinatesLinearMap n ψ
        (residueFreeGroupFoxDerivativeVector n ψ w) =
      residueUniversalDifferential n ψ w
theorem

residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap

L142 ↗
FoxDifferential.residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap
Documentation

The coordinate map is a left inverse to the coordinate-to-differential map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
theorem residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap
    (n : ℕ) (ψ : FreeGroup X →* H) :
    (residueDifferentialToFreeFoxCoordinates n ψ).comp
        (residueFreeFoxCoordinatesLinearMap n ψ) =
      LinearMap.id
theorem

residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates

L172 ↗
FoxDifferential.residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates
Documentation

The coordinate-to-differential map is a left inverse to the residue coordinate map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
theorem residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates
    (n : ℕ) (ψ : FreeGroup X →* H) :
    (residueFreeFoxCoordinatesLinearMap n ψ).comp
        (residueDifferentialToFreeFoxCoordinates n ψ) =
      LinearMap.id
def

residueFreeFoxCoordinatesLinearEquivDifferential

L186 ↗
FoxDifferential.residueFreeFoxCoordinatesLinearEquivDifferential
Documentation

The linear equivalence between residue Fox coordinates and the residue universal differential module of a finite-rank free group.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
def residueFreeFoxCoordinatesLinearEquivDifferential
    (n : ℕ) (ψ : FreeGroup X →* H) :
    ResidueFreeFoxCoordinates n H X ≃ₗ[ResidueGroupRing n H]
      ResidueDifferentialModule n ψ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.