Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Common.FoxBoundary
ProCGroups/FoxDifferential/Common/FoxBoundary

ProCGroups.FoxDifferential.Common.FoxBoundary

8 Theorems | 3 Definitions

The principal declarations in this module are:

  • coefficientFoxBoundary The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto \operatorname{coeff}(g)-1\). - coefficientFoxBoundaryCrossedHom The coefficient Fox boundary is a crossed differential. - coefficientFoxBoundary_one The coefficient Fox boundary sends the identity to zero. - coefficientFoxBoundary_mul Product rule for the coefficient Fox boundary \(g \mapsto \operatorname{coeff}(g)-1\).
import
Imported by

Declarations

Definition FoxDifferential.coefficientFoxBoundary 
def coefficientFoxBoundary (coeff : G →* R) (g : G) : R :=
  coeff g - 1

The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto \operatorname{coeff}(g)-1\).

Theorem FoxDifferential.coefficientFoxBoundary_one 
@[simp]
theorem coefficientFoxBoundary_one (coeff : G →* R) :
    coefficientFoxBoundary coeff 1 = 0

The coefficient Fox boundary sends the identity to zero.

Show Lean proof
Theorem FoxDifferential.coefficientFoxBoundary_mul 
theorem coefficientFoxBoundary_mul (coeff : G →* R) (g h : G) :
    coefficientFoxBoundary coeff (g * h) =
      coefficientFoxBoundary coeff g + coeff g • coefficientFoxBoundary coeff h

Product rule for the coefficient Fox boundary \(g \mapsto \operatorname{coeff}(g)-1\).

Show Lean proof
Definition FoxDifferential.coefficientFoxBoundaryCrossedHom 
def coefficientFoxBoundaryCrossedHom (coeff : G →* R) : ScalarCrossedHom coeff R where
  toFun := coefficientFoxBoundary coeff
  map_mul' := coefficientFoxBoundary_mul coeff

The coefficient Fox boundary is a crossed differential.

Theorem FoxDifferential.coefficientFoxBoundaryCrossedHom_apply 
@[simp]
theorem coefficientFoxBoundaryCrossedHom_apply (coeff : G →* R) (g : G) :
    coefficientFoxBoundaryCrossedHom coeff g = coeff g - 1

The coefficient boundary crossed homomorphism sends a group element to its coefficient minus one.

Show Lean proof
Definition FoxDifferential.foxBoundaryMap 
def foxBoundaryMap (generatorBoundary : X → R) : (X → R) →ₗ[R] R where
  toFun v := ∑ x : X, v x * generatorBoundary x
  map_add' v w := by
    simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
  map_smul' r v := by
    simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]

The finite Fox boundary map with prescribed generator boundary values sends a coordinate vector \(v : X \to R\) to \(\sum_x v(x)\,\mathrm{generatorBoundary}(x)\).

Theorem FoxDifferential.foxBoundaryMap_apply 
theorem foxBoundaryMap_apply (generatorBoundary : X → R) (v : X → R) :
    foxBoundaryMap generatorBoundary v =
      ∑ x : X, v x * generatorBoundary x

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

Show Lean proof
Theorem FoxDifferential.foxBoundaryMap_single 
@[simp]
theorem foxBoundaryMap_single (generatorBoundary : X → R) (x : X) :
    foxBoundaryMap generatorBoundary (Pi.single x (1 : R)) = generatorBoundary x

The finite Fox boundary map sends a coordinate basis vector to the corresponding generator boundary.

Show Lean proof
Theorem FoxDifferential.foxBoundaryMap_freeCrossedHomWithCoeff 
theorem foxBoundaryMap_freeCrossedHomWithCoeff
    (boundary : ScalarCrossedHom coeff R)
    (hgenerator : ∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
    (w : FreeGroup X) :
    foxBoundaryMap generatorBoundary
        (freeCrossedHomWithCoeff
          (A := X → R) coeff (fun x : X => Pi.single x (1 : R)) w) =
      boundary w

Boundary-map form of the generic free-group Fox formula: applying the Fox boundary map to the free crossed differential recovers the crossed differential with the prescribed generator values.

Show Lean proof
Theorem FoxDifferential.foxBoundaryMap_of_crossedHom 
theorem foxBoundaryMap_of_crossedHom
    (delta : ScalarCrossedHom coeff (X → R))
    (hdelta_generator :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
    (boundary : ScalarCrossedHom coeff R)
    (hboundary_generator :
      ∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
    (w : FreeGroup X) :
    foxBoundaryMap generatorBoundary (delta w) = boundary w

Conditional boundary-map form of the generic free-group Fox formula. Any crossed differential with standard coordinate values satisfies the same boundary formula as the canonical free crossed differential.

Show Lean proof
Theorem FoxDifferential.foxEulerFormula_of_crossedHom 
theorem foxEulerFormula_of_crossedHom
    (delta : ScalarCrossedHom coeff (X → R))
    (hdelta_generator :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
    (w : FreeGroup X) :
    coeff w - 1 =
      ∑ x : X, delta w x * (coeff (FreeGroup.of x) - 1)

Explicit finite-sum form of the generic Fox--Euler formula for any crossed differential with standard coordinate values: \(\mathrm{coeff}(w)-1=\sum_x \delta_x(w)(\mathrm{coeff}(x)-1)\).

Show Lean proof