Module

Coordinates.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Coordinates

12 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — free group — coordinates

The principal declarations in this module are:

zcFreeGroupFoxBoundary

The completed Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).

zcDifferentialToFreeFoxCoordinates

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

zcFreeGroupFoxBoundary_apply

The boundary map is evaluated on the canonical generators and then extended linearly to the completed coordinate module.

zcFreeGroupFoxBoundary_eq_foxBoundaryMap

The completed Fox boundary is the generic finite Fox boundary map specialized to \(x \mapsto [\psi(x)] - 1\).

Imports2

Imported by2

def

zcFreeGroupFoxBoundary

L45 ↗

FoxDifferential.zcFreeGroupFoxBoundary

Documentation

The completed Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · full declaration

def zcFreeGroupFoxBoundary (ψ : FreeGroup X →* H) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H where
  toFun v := ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)
  map_add' := by
    intro v w
    simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
  map_smul' := by
    intro r v
    simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]

theorem

zcFreeGroupFoxBoundary_apply

L61 ↗

FoxDifferential.zcFreeGroupFoxBoundary_apply

Documentation

The boundary map is evaluated on the canonical generators and then extended linearly to the completed coordinate module.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupFoxBoundary_apply
    (ψ : FreeGroup X →* H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeGroupFoxBoundary C ψ v =
      ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

theorem

zcFreeGroupFoxBoundary_eq_foxBoundaryMap

L72 ↗

FoxDifferential.zcFreeGroupFoxBoundary_eq_foxBoundaryMap

Documentation

The completed Fox boundary is the generic finite Fox boundary map specialized to \(x \mapsto [\psi(x)] - 1\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
omit [DecidableEq X] in

Lean source · full declaration

theorem zcFreeGroupFoxBoundary_eq_foxBoundaryMap
    (ψ : FreeGroup X →* H) :
    zcFreeGroupFoxBoundary C ψ =
      foxBoundaryMap
        (fun i : X =>
          coefficientFoxBoundary (zcCompletedGroupAlgebraScalar C ψ) (FreeGroup.of i)) := by
  ext v
  rfl

theorem

zcFreeGroupFoxBoundary_single

L86 ↗

FoxDifferential.zcFreeGroupFoxBoundary_single

Documentation

The completed Fox boundary sends a coordinate basis vector to the corresponding completed augmentation generator.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

theorem zcFreeGroupFoxBoundary_single (ψ : FreeGroup X →* H) (i : X) :
    zcFreeGroupFoxBoundary C ψ
        (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
      zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of i)

def

zcDifferentialToFreeFoxCoordinates

L99 ↗

FoxDifferential.zcDifferentialToFreeFoxCoordinates

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

def zcDifferentialToFreeFoxCoordinates (ψ : FreeGroup X →* H) :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCFreeFoxCoordinates C (X := X) (H := H)

theorem

zcDifferentialToFreeFoxCoordinates_universal

L110 ↗

FoxDifferential.zcDifferentialToFreeFoxCoordinates_universal

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
omit [Fintype X] in

Lean source · statement

theorem zcDifferentialToFreeFoxCoordinates_universal
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcDifferentialToFreeFoxCoordinates C ψ
        (zcUniversalDifferential C ψ w) =
      zcFreeGroupFoxDerivativeVector C ψ w

def

zcFreeFoxCoordinatesLinearMap

L121 ↗

FoxDifferential.zcFreeFoxCoordinatesLinearMap

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · full declaration

def zcFreeFoxCoordinatesLinearMap (ψ : FreeGroup X →* H) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModule C ψ where
  toFun v := ∑ x : X, v x • zcUniversalDifferential C ψ (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, RingHom.id_apply, smul_eq_mul, Finset.smul_sum, smul_smul]

theorem

zcFreeFoxCoordinatesLinearMap_single

L137 ↗

FoxDifferential.zcFreeFoxCoordinatesLinearMap_single

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

theorem zcFreeFoxCoordinatesLinearMap_single (ψ : FreeGroup X →* H) (x : X) :
    zcFreeFoxCoordinatesLinearMap C ψ
        (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
      zcUniversalDifferential C ψ (FreeGroup.of x)

theorem

zcFreeFoxCoordinatesLinearMap_derivativeVector

L156 ↗

FoxDifferential.zcFreeFoxCoordinatesLinearMap_derivativeVector

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

theorem zcFreeFoxCoordinatesLinearMap_derivativeVector
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcFreeFoxCoordinatesLinearMap C ψ
        (zcFreeGroupFoxDerivativeVector C ψ w) =
      zcUniversalDifferential C ψ w

theorem

zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap

L201 ↗

FoxDifferential.zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

theorem zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap
    (ψ : FreeGroup X →* H) :
    (zcDifferentialToFreeFoxCoordinates C ψ).comp
        (zcFreeFoxCoordinatesLinearMap C ψ) =
      LinearMap.id

theorem

zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates

L229 ↗

FoxDifferential.zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

theorem zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates
    (ψ : FreeGroup X →* H) :
    (zcFreeFoxCoordinatesLinearMap C ψ).comp
        (zcDifferentialToFreeFoxCoordinates C ψ) =
      LinearMap.id

def

zcFreeFoxCoordinatesLinearEquivDifferential

L249 ↗

FoxDifferential.zcFreeFoxCoordinatesLinearEquivDifferential

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]

Lean source · statement

def zcFreeFoxCoordinatesLinearEquivDifferential
    (ψ : FreeGroup X →* H) :
    ZCFreeFoxCoordinates C (X := X) (H := H) ≃ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModule C ψ

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — free group — coordinates

Declarations