FoxBoundary.lean

def coefficientFoxBoundary (coeff : G →* R) (g : G) : R

theorem coefficientFoxBoundary_one (coeff : G →* R) :
    coefficientFoxBoundary coeff 1 = 0

theorem coefficientFoxBoundary_mul (coeff : G →* R) (g h : G) :
    coefficientFoxBoundary coeff (g * h) =
      coefficientFoxBoundary coeff g + coeff g • coefficientFoxBoundary coeff h

def coefficientFoxBoundaryCrossedHom (coeff : G →* R) : ScalarCrossedHom coeff R where
  toFun := coefficientFoxBoundary coeff
  map_mul' := coefficientFoxBoundary_mul coeff

theorem coefficientFoxBoundaryCrossedHom_apply (coeff : G →* R) (g : G) :
    coefficientFoxBoundaryCrossedHom coeff g = coeff g - 1

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]

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

theorem foxBoundaryMap_single (generatorBoundary : X → R) (x : X) :
    foxBoundaryMap generatorBoundary (Pi.single x (1 : R)) = generatorBoundary x

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 := by
  let delta : ScalarCrossedHom coeff R :=
    ScalarCrossedHom.mapLinear
      (freeCrossedHomWithCoeff
        (A := X → R) coeff (fun x : X => Pi.single x (1 : R)))
      (foxBoundaryMap generatorBoundary)
  have hdelta_generator :
      ∀ x : X, delta (FreeGroup.of x) = generatorBoundary x := by
    intro x
    simp only [delta, ScalarCrossedHom.mapLinear_apply, freeCrossedHomWithCoeff_of,
      foxBoundaryMap_single]
  have hdelta_eq :
      delta = freeCrossedHomWithCoeff (A := R) coeff generatorBoundary :=
    freeCrossedHomWithCoeff_unique
      (A := R) coeff generatorBoundary delta hdelta_generator
  have hboundary_eq :
      boundary = freeCrossedHomWithCoeff (A := R) coeff generatorBoundary :=
    freeCrossedHomWithCoeff_unique
      (A := R) coeff generatorBoundary boundary hgenerator
  change delta w = boundary w
  rw [hdelta_eq, hboundary_eq]

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

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)