BoundaryCycles.lean

def foxAlgebraicStageBoundaryCycleSubmodule [Fintype X] :
    Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n)

theorem mem_foxAlgebraicStageBoundaryCycleSubmodule [Fintype X]
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {v : foxAlgebraicStageCoordinateVector (X := X) N n} :
    v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n ↔
      foxAlgebraicStageFoxBoundary (X := X) N n v = 0

def foxAlgebraicStageSourceKernelDerivativeSet :
    Set (foxAlgebraicStageCoordinateVector (X := X) N n)

def foxAlgebraicStageKernelWordDerivativeSet :
    Set (foxAlgebraicStageCoordinateVector (X := X) N n)

theorem foxAlgebraicStageCoefficient_eq_one_of_mem
    {w : FreeGroup X} (hw : w ∈ N) :
    foxAlgebraicStageCoefficient (X := X) N n w = 1

theorem foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel
    {q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n}
    (hq : foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q = 1

def foxAlgebraicStageSourceKernelDerivativeAddSubgroup :
    AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n) where
  carrier := foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n
  zero_mem' := by
    refine ⟨1, ?_, ?_⟩
    · simp only [map_one]
    · exact ScalarCrossedHom.map_one
        (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)
  add_mem' := by
    intro a b ha hb
    rcases ha with ⟨q, hq, hqa⟩
    rcases hb with ⟨r, hr, hrb⟩
    refine ⟨q * r, ?_, ?_⟩
    · rw [map_mul, hq, hr, one_mul]
    · rw [ScalarCrossedHom.map_mul
          (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)]
      rw [foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel (X := X) N n hq]
      simp only [hqa, hrb, one_smul]
  neg_mem' := by
    intro a ha
    rcases ha with ⟨q, hq, hqa⟩
    refine ⟨q⁻¹, ?_, ?_⟩
    · rw [map_inv, hq]
      simp only [inv_one]
    · rw [ScalarCrossedHom.map_inv
          (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)]
      have hcoeff :
          foxAlgebraicStageQuotientCoefficient (X := X) N n q⁻¹ = 1 := by
        apply foxAlgebraicStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
        rw [map_inv, hq]
        simp only [inv_one]
      rw [hcoeff]
      simp only [hqa, one_smul]

theorem foxAlgebraicStageSourceKernelDerivativeAddSubgroup_coe :
    ((foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n :
        AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n)) :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) =
      foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

theorem foxAlgebraicStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n =
      foxAlgebraicStageKernelWordDerivativeSet (X := X) N n

theorem foxAlgebraicStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule
    [Fintype X] :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n ⊆
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
        Set (foxAlgebraicStageCoordinateVector (X := X) N n))

def foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop

theorem foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_iff_words
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ⊆
        foxAlgebraicStageKernelWordDerivativeSet (X := X) N n

theorem foxAlgebraicStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n =
        (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n