Module

Derivative.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Derivative

30 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

ZCFreeFoxCoordinates

Completed Fox-coordinate vectors with coefficients in \(\mathbb{Z}_C\llbracket H\rrbracket\).

zcFreeGroupFoxDerivativeVector

Completed free-group Fox derivative vector, with coefficients pushed forward along \(\psi:\mathrm{FreeGroup}(X)\to H\).

zcFreeGroupFoxDerivativeVector_one

The completed free-group derivative vector sends the identity word to zero.

zcFreeGroupFoxDerivativeVector_of

The completed free-group derivative vector sends a free generator to the corresponding coordinate basis vector.

Imports2

Imported by2

abbrev

ZCFreeFoxCoordinates

L42 ↗

FoxDifferential.ZCFreeFoxCoordinates

Documentation

Completed Fox-coordinate vectors with coefficients in \(\mathbb{Z}_C\llbracket H\rrbracket\).

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · statement

abbrev ZCFreeFoxCoordinates : Type (max u v)

def

zcFreeGroupFoxDerivativeVector

L49 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector

Documentation

Completed free-group Fox derivative vector, with coefficients pushed forward along \(\psi:\mathrm{FreeGroup}(X)\to H\).

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcFreeGroupFoxDerivativeVector (ψ : FreeGroup X →* H) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H))

def

zcFreeGroupFoxDerivative

L58 ↗

FoxDifferential.zcFreeGroupFoxDerivative

Documentation

A coordinate of the completed free-group Fox derivative.

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcFreeGroupFoxDerivative (ψ : FreeGroup X →* H) (i : X) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedGroupAlgebra C H)

theorem

zcFreeGroupFoxDerivativeVector_one

L68 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_one

Documentation

The completed free-group derivative vector sends the identity word to zero.

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_one (ψ : FreeGroup X →* H) :
    zcFreeGroupFoxDerivativeVector C ψ (1 : FreeGroup X) = 0

theorem

zcFreeGroupFoxDerivativeVector_of

L77 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_of

Documentation

The completed free-group derivative vector sends a free generator to the corresponding coordinate basis 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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_of (ψ : FreeGroup X →* H) (x : X) :
    zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x) =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

theorem

zcCrossedDifferential_comp_zcFreeGroupFoxDerivative

L95 ↗

FoxDifferential.zcCrossedDifferential_comp_zcFreeGroupFoxDerivative

Documentation

Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) abstract Fox chain rule for an arbitrary crossed differential.

Source context 11 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 AbstractChainRule
variable {Y : Type u}
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [Fintype X]

Lean source · statement

theorem zcCrossedDifferential_comp_zcFreeGroupFoxDerivative
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (w : FreeGroup X) :
    delta (φ w) =
      ∑ x : X,
        zcFreeGroupFoxDerivative C (ψ.comp φ) x w •
          delta (φ (FreeGroup.of x))

def

zcFreeGroupHomFoxJacobian

L128 ↗

FoxDifferential.zcFreeGroupHomFoxJacobian

Documentation

Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian of a homomorphism of free groups.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

def zcFreeGroupHomFoxJacobian
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → ZCCompletedGroupAlgebra C H

theorem

zcFreeGroupHomFoxJacobian_apply

L140 ↗

FoxDifferential.zcFreeGroupHomFoxJacobian_apply

Documentation

The completed Fox-Jacobian of a free-group homomorphism is evaluated by taking the completed Fox derivative vector of the image of a generator.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobian_apply
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (x : X) (y : Y) :
    zcFreeGroupHomFoxJacobian C ψ φ x y =
      zcFreeGroupFoxDerivative C ψ y (φ (FreeGroup.of x))

def

zcFreeGroupHomFoxJacobianMatrix

L148 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianMatrix

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian is packaged as a matrix.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

def zcFreeGroupHomFoxJacobianMatrix
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    Matrix X Y (ZCCompletedGroupAlgebra C H)

theorem

zcFreeGroupHomFoxJacobianMatrix_apply

L160 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianMatrix_apply

Documentation

The matrix evaluation is componentwise the completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobianMatrix_apply
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (x : X) (y : Y) :
    zcFreeGroupHomFoxJacobianMatrix C ψ φ x y =
      zcFreeGroupHomFoxJacobian C ψ φ x y

def

zcFreeGroupHomFoxJacobianLinearMap

L171 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianLinearMap

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian is bundled into a finite linear map on 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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

def zcFreeGroupHomFoxJacobianLinearMap
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCFreeFoxCoordinates C (X := Y) (H := H)

theorem

zcFreeGroupHomFoxJacobianLinearMap_apply

L185 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianLinearMap_apply

Documentation

Evaluation formula for the completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobianLinearMap_apply
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) (y : Y) :
    zcFreeGroupHomFoxJacobianLinearMap C ψ φ v y =
      ∑ x : X, v x * zcFreeGroupHomFoxJacobian C ψ φ x y

theorem

zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul

L198 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map is row-vector multiplication by its matrix.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeGroupHomFoxJacobianLinearMap C ψ φ v =
      Matrix.vecMul v (zcFreeGroupHomFoxJacobianMatrix C ψ φ)

theorem

zcFreeGroupHomFoxJacobian_id

L212 ↗

FoxDifferential.zcFreeGroupHomFoxJacobian_id

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian of the identity homomorphism is the identity family.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupHomFoxJacobian_id (ψ : FreeGroup X →* H) :
    zcFreeGroupHomFoxJacobian C ψ (MonoidHom.id (FreeGroup X)) =
      foxJacobianId (R := ZCCompletedGroupAlgebra C H) (X := X)

theorem

zcFreeGroupHomFoxJacobianMatrix_id

L224 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianMatrix_id

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian matrix of the identity homomorphism is the identity matrix.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupHomFoxJacobianMatrix_id (ψ : FreeGroup X →* H) :
    zcFreeGroupHomFoxJacobianMatrix C ψ (MonoidHom.id (FreeGroup X)) =
      (1 : Matrix X X (ZCCompletedGroupAlgebra C H))

theorem

zcFreeGroupHomFoxJacobianLinearMap_id

L236 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianLinearMap_id

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map of the identity homomorphism is the identity.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupHomFoxJacobianLinearMap_id
    [Fintype X] (ψ : FreeGroup X →* H) :
    zcFreeGroupHomFoxJacobianLinearMap C ψ (MonoidHom.id (FreeGroup X)) =
      (LinearMap.id :
        ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
          ZCFreeFoxCoordinates C (X := X) (H := H))

theorem

zcFreeGroupFoxDerivativeVector_comp_linearMap

L247 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_comp_linearMap

Documentation

Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in vector form.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_comp_linearMap
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C ψ (φ w) =
      zcFreeGroupHomFoxJacobianLinearMap C ψ φ
        (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)

theorem

zcFreeGroupFoxDerivativeVector_comp_apply

L265 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_comp_apply

Documentation

Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in component form.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_comp_apply
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) (y : Y) :
    zcFreeGroupFoxDerivativeVector C ψ (φ w) y =
      ∑ x : X,
        zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w x *
          zcFreeGroupHomFoxJacobian C ψ φ x y

theorem

zcFreeGroupFoxDerivative_comp

L279 ↗

FoxDifferential.zcFreeGroupFoxDerivative_comp

Documentation

Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule, component form for named derivative coordinates.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupFoxDerivative_comp
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) (y : Y) :
    zcFreeGroupFoxDerivative C ψ y (φ w) =
      ∑ x : X,
        zcFreeGroupFoxDerivative C (ψ.comp φ) x w *
          zcFreeGroupHomFoxJacobian C ψ φ x y

theorem

zcFreeGroupFoxDerivativeVector_comp_matrix

L290 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_comp_matrix

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in matrix form.

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 Jacobian
variable {Y : Type u} [DecidableEq Y]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_comp_matrix
    [Fintype X]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C ψ (φ w) =
      Matrix.vecMul
        (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)
        (zcFreeGroupHomFoxJacobianMatrix C ψ φ)

theorem

zcFreeGroupHomFoxJacobian_comp_apply

L309 ↗

FoxDifferential.zcFreeGroupHomFoxJacobian_comp_apply

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed componentwise.

Source context 11 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 Jacobian
variable {Y : Type u} [DecidableEq Y]
variable {Z : Type u} [DecidableEq Z]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobian_comp_apply
    [Fintype Y]
    (ψ : FreeGroup Z →* H)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
    (x : X) (z : Z) :
    zcFreeGroupHomFoxJacobian C ψ (φ.comp χ) x z =
      ∑ y : Y,
        zcFreeGroupHomFoxJacobian C (ψ.comp φ) χ x y *
          zcFreeGroupHomFoxJacobian C ψ φ y z

theorem

zcFreeGroupHomFoxJacobianLinearMap_comp

L332 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianLinearMap_comp

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed in linear-map form.

Source context 11 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 Jacobian
variable {Y : Type u} [DecidableEq Y]
variable {Z : Type u} [DecidableEq Z]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobianLinearMap_comp
    [Fintype X] [Fintype Y]
    (ψ : FreeGroup Z →* H)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    (zcFreeGroupHomFoxJacobianLinearMap C ψ φ).comp
        (zcFreeGroupHomFoxJacobianLinearMap C (ψ.comp φ) χ) =
      zcFreeGroupHomFoxJacobianLinearMap C ψ (φ.comp χ)

theorem

zcFreeGroupHomFoxJacobianMatrix_comp

L353 ↗

FoxDifferential.zcFreeGroupHomFoxJacobianMatrix_comp

Documentation

The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed in matrix form.

Source context 11 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 Jacobian
variable {Y : Type u} [DecidableEq Y]
variable {Z : Type u} [DecidableEq Z]
omit [DecidableEq X] in

Lean source · statement

theorem zcFreeGroupHomFoxJacobianMatrix_comp
    [Fintype Y]
    (ψ : FreeGroup Z →* H)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    zcFreeGroupHomFoxJacobianMatrix C ψ (φ.comp χ) =
      zcFreeGroupHomFoxJacobianMatrix C (ψ.comp φ) χ *
        zcFreeGroupHomFoxJacobianMatrix C ψ φ

theorem

zcFreeGroupFoxDerivativeVector_unique

L370 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_unique

Documentation

Uniqueness of the completed free-group derivative vector among crossed differentials with standard coordinate values on free generators.

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_unique
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    delta = zcFreeGroupFoxDerivativeVector C ψ

theorem

existsUnique_zcFreeGroupFoxDerivativeVector

L385 ↗

FoxDifferential.existsUnique_zcFreeGroupFoxDerivativeVector

Documentation

Existence and uniqueness theorem for the completed free-group 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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem existsUnique_zcFreeGroupFoxDerivativeVector
    (ψ : FreeGroup X →* H) :
    ∃! delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
        (ZCFreeFoxCoordinates C (X := X) (H := H)),
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)

def

zcFreeGroupFoxDerivativeVectorLinearMap

L399 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVectorLinearMap

Documentation

The linear map from the completed universal module representing the completed 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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

zcFreeGroupFoxDerivativeVectorLinearMap_universal

L413 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVectorLinearMap_universal

Documentation

The representing linear map evaluates on the universal differential as the completed 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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVectorLinearMap_universal
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVectorLinearMap C ψ
        (zcUniversalDifferential C ψ w) =
      zcFreeGroupFoxDerivativeVector C ψ w

theorem

zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero

L427 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero

Documentation

If the universal completed differential of a word vanishes, then its completed free Fox derivative vector vanishes.

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
    (ψ : FreeGroup X →* H) {w : FreeGroup X}
    (hw : zcUniversalDifferential C ψ w = 0) :
    zcFreeGroupFoxDerivativeVector C ψ w = 0

theorem

zcFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero

L436 ↗

FoxDifferential.zcFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero

Documentation

The vanishing criterion for the completed Fox derivative vector holds componentwise.

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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero
    (ψ : FreeGroup X →* H) (i : X) {w : FreeGroup X}
    (hw : zcUniversalDifferential C ψ w = 0) :
    zcFreeGroupFoxDerivative C ψ i w = 0

theorem

existsUnique_zcFreeGroupFoxDerivativeVectorLinearMap

L446 ↗

FoxDifferential.existsUnique_zcFreeGroupFoxDerivativeVectorLinearMap

Documentation

Existence and uniqueness of the linear map representing the completed 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 (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem existsUnique_zcFreeGroupFoxDerivativeVectorLinearMap
    (ψ : FreeGroup X →* H) :
    ∃! f :
        ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
          ZCFreeFoxCoordinates C (X := X) (H := H),
      ∀ w : FreeGroup X,
        f (zcUniversalDifferential C ψ w) =
          zcFreeGroupFoxDerivativeVector C ψ w

Module documentation

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

Declarations