Module

Universal.lean

Nyll.ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal

4 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — residue — free group — universal

The principal declarations in this module are:

residueFreeCrossedHomEquivLinearMap

Residue crossed homomorphisms on a free group are represented by the universal residue module.

residueFreeGroupFoxDerivativeVectorLinearMap

The linear map from the residue universal module representing the residue derivative vector.

residueFreeGroupFoxDerivativeVectorLinearMap_universal

The representing linear map evaluates on the universal differential as the residue derivative vector.

existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap

Existence and uniqueness of the linear map representing the residue derivative vector.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic

Imported by2

def

residueFreeCrossedHomEquivLinearMap

L39 ↗

FoxDifferential.residueFreeCrossedHomEquivLinearMap

Documentation

Residue crossed homomorphisms on a free group are represented by the universal residue module.

Source context 5 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]

Lean source · statement

def residueFreeCrossedHomEquivLinearMap
    (n : ℕ) (ψ : FreeGroup X →* H) :
    ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueFreeFoxCoordinates n H X) ≃
      (ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
        ResidueFreeFoxCoordinates n H X)

def

residueFreeGroupFoxDerivativeVectorLinearMap

L48 ↗

FoxDifferential.residueFreeGroupFoxDerivativeVectorLinearMap

Documentation

The linear map from the residue universal module representing the residue derivative vector.

Source context 5 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]

Lean source · statement

def residueFreeGroupFoxDerivativeVectorLinearMap
    (n : ℕ) (ψ : FreeGroup X →* H) :
    ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
      ResidueFreeFoxCoordinates n H X

theorem

residueFreeGroupFoxDerivativeVectorLinearMap_universal

L61 ↗

FoxDifferential.residueFreeGroupFoxDerivativeVectorLinearMap_universal

Documentation

The representing linear map evaluates on the universal differential as the residue derivative vector.

Source context 5 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]

Lean source · statement

theorem residueFreeGroupFoxDerivativeVectorLinearMap_universal
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueFreeGroupFoxDerivativeVectorLinearMap n ψ
        (residueUniversalDifferential n ψ w) =
      residueFreeGroupFoxDerivativeVector n ψ w

theorem

existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap

L71 ↗

FoxDifferential.existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap

Documentation

Existence and uniqueness of the linear map representing the residue derivative vector.

Source context 5 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]

Lean source · statement

theorem existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap
    (n : ℕ) (ψ : FreeGroup X →* H) :
    ∃! f :
        ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
          ResidueFreeFoxCoordinates n H X,
      ∀ w : FreeGroup X,
        f (residueUniversalDifferential n ψ w) =
          residueFreeGroupFoxDerivativeVector n ψ w

Module documentation

Fox differential: completed — residue — free group — universal

Declarations

residueFreeCrossedHomEquivLinearMap

residueFreeGroupFoxDerivativeVectorLinearMap

residueFreeGroupFoxDerivativeVectorLinearMap_universal

existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap