ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Coordinates

5 Theorems | 3 Definitions

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.

import

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal

Imported by

Definition FoxDifferential.residueDifferentialToFreeFoxCoordinates

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

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

Theorem FoxDifferential.residueDifferentialToFreeFoxCoordinates_universal

omit [Fintype X] in
@[simp]
theorem residueDifferentialToFreeFoxCoordinates_universal
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueDifferentialToFreeFoxCoordinates n ψ
        (residueUniversalDifferential n ψ w) =
      residueFreeGroupFoxDerivativeVector n ψ w

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

Show Lean proof

Definition FoxDifferential.residueFreeFoxCoordinatesLinearMap

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]

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

Theorem FoxDifferential.residueFreeFoxCoordinatesLinearMap_single

@[simp]
theorem residueFreeFoxCoordinatesLinearMap_single
    (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
    residueFreeFoxCoordinatesLinearMap n ψ
        (Pi.single x (1 : ResidueGroupRing n H)) =
      residueUniversalDifferential n ψ (FreeGroup.of x)

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

Show Lean proof

Theorem FoxDifferential.residueFreeFoxCoordinatesLinearMap_derivativeVector

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

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

Show Lean proof

Theorem FoxDifferential.residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap

theorem residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap
    (n : ℕ) (ψ : FreeGroup X →* H) :
    (residueDifferentialToFreeFoxCoordinates n ψ).comp
        (residueFreeFoxCoordinatesLinearMap n ψ) =
      LinearMap.id

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

Show Lean proof

Theorem FoxDifferential.residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates

theorem residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates
    (n : ℕ) (ψ : FreeGroup X →* H) :
    (residueFreeFoxCoordinatesLinearMap n ψ).comp
        (residueDifferentialToFreeFoxCoordinates n ψ) =
      LinearMap.id

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

Show Lean proof

Definition FoxDifferential.residueFreeFoxCoordinatesLinearEquivDifferential

def residueFreeFoxCoordinatesLinearEquivDifferential
    (n : ℕ) (ψ : FreeGroup X →* H) :
    ResidueFreeFoxCoordinates n H X ≃ₗ[ResidueGroupRing n H]
      ResidueDifferentialModule n ψ := by
  refine LinearEquiv.ofLinear
    (residueFreeFoxCoordinatesLinearMap n ψ)
    (residueDifferentialToFreeFoxCoordinates n ψ)
    ?_ ?_
  · exact residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates
      n ψ
  · exact residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap
      n ψ

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

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Coordinates

Declarations