ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal

2 Theorems | 2 Definitions

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.

import

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic

Imported by

Definition FoxDifferential.residueFreeCrossedHomEquivLinearMap

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

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

Definition FoxDifferential.residueFreeGroupFoxDerivativeVectorLinearMap

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

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

Theorem FoxDifferential.residueFreeGroupFoxDerivativeVectorLinearMap_universal

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

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

Show Lean proof

Theorem FoxDifferential.existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap

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

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal

Declarations