ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary

9 Theorems | 1 Definition

The principal declarations in this module are:

relativeFreeGroupFoxBoundary The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\). - relativeFreeGroupFoxBoundary_apply The relative free-group Fox boundary is evaluated on canonical generators and then extended linearly to the coordinate module. - relativeFreeGroupFoxBoundary_single The relative Fox boundary sends a coordinate basis vector to the corresponding augmentation generator. - toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap Composing the universal boundary with the coordinate-to-differential map gives the pushed-forward Fox boundary.

imports

Imported by

Definition FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary

def relativeFreeGroupFoxBoundary :
    RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] GroupRing H :=
  { toFun := fun a =>
      ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))
    map_add' := by
      intro a b
      simp only [Pi.add_apply, augmentationGenerator_eq_groupRingBoundary, add_mul,
          Finset.sum_add_distrib]
    map_smul' := by
      intro r a
      simp only [Pi.smul_apply, smul_eq_mul, augmentationGenerator_eq_groupRingBoundary, mul_assoc,
  RingHom.id_apply, Finset.mul_sum]}

The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\).

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_apply

omit [DecidableEq X] in
theorem relativeFreeGroupFoxBoundary_apply
    (a : RelativeFreeFoxCoordinates (H := H) X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ a =
      ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))

The relative free-group Fox boundary is evaluated on canonical generators and then extended linearly to the coordinate module.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_single

@[simp]
theorem relativeFreeGroupFoxBoundary_single (x : X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ
        (Pi.single x (1 : GroupRing H)) =
      augmentationGenerator H (ψ (FreeGroup.of x))

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap

omit [DecidableEq X] in
theorem toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap :
    (toGroupRing ψ).comp
        (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
      relativeFreeGroupFoxBoundary (H := H) X ψ

Composing the universal boundary with the coordinate-to-differential map gives the pushed-forward Fox boundary.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula

theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))

Relative Fox fundamental formula, also known as the Fox--Euler formula: \(\psi(w) - 1 = \sum_x (\partial w/\partial x) (\psi(x) - 1)\).

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_derivative

theorem relativeFreeGroupFoxBoundary_derivative (w : FreeGroup X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ
        (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
      groupRingBoundary ψ w

Fox boundary form of the relative Fox fundamental formula.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_of_crossedHom

theorem relativeFreeGroupFoxBoundary_of_crossedHom
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ (delta w) = groupRingBoundary ψ w

Conditional relative Fox boundary formula. Any differential map on a free group with the standard coordinate values satisfies the relative Fox boundary formula.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom

theorem relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X, delta w x * augmentationGenerator H (ψ (FreeGroup.of x))

Conditional relative Fox fundamental formula. The Fox-Euler sum computed from any differential map with standard coordinate values is \([\psi(w)]-1\).

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_euler_formula_of_crossedHom

theorem relativeFreeGroupFoxDerivative_euler_formula_of_crossedHom
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
      ∑ x : X, delta w x * augmentationGenerator H (ψ (FreeGroup.of x))

Explicit \(\psi(w)-1\) version of the conditional relative Fox-Euler formula.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_euler_formula

theorem relativeFreeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))

Explicit \(\psi(w)-1\) version of the relative Fox--Euler formula.

Show Lean proof

ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary

Declarations