BoundarySubgroups.lean

def foxAlgebraicStageSemidirectBoundaryCycleSubgroup [Fintype X] :
    Subgroup (FoxAlgebraicStageSemidirect (X := X) N n) where
  carrier := foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n
  one_mem' := by
    constructor
    · simp only [FoxAlgebraicStageSemidirect.one_right]
    · exact (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).zero_mem
  mul_mem' := by
    intro y z hy hz
    rcases hy with ⟨hyright, hyleft⟩
    rcases hz with ⟨hzright, hzleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.mul_right, hyright, hzright, mul_one]
    · rw [FoxAlgebraicStageSemidirect.mul_left, hyright]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).add_mem hyleft hzleft
  inv_mem' := by
    intro y hy
    rcases hy with ⟨hyright, hyleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.inv_right, hyright, inv_one]
    · rw [FoxAlgebraicStageSemidirect.inv_left, hyright, inv_one]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).neg_mem hyleft

theorem foxAlgebraicStageSemidirectBoundaryCycleSubgroup_coe [Fintype X] :
    ((foxAlgebraicStageSemidirectBoundaryCycleSubgroup (X := X) N n :
        Subgroup (FoxAlgebraicStageSemidirect (X := X) N n)) :
          Set (FoxAlgebraicStageSemidirect (X := X) N n)) =
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSet_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {y : FoxAlgebraicStageSemidirect (X := X) N n} :
    y ∈ foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n ↔
      y.right = 1 ∧
        y.left ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

def foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup :
    Subgroup (FoxAlgebraicStageSemidirect (X := X) N n) where
  carrier :=
    { y | y.right = 1 ∧
        y.left ∈ foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n }
  one_mem' := by
    exact ⟨rfl, (foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n).zero_mem⟩
  mul_mem' := by
    intro y z hy hz
    rcases hy with ⟨hyright, hyleft⟩
    rcases hz with ⟨hzright, hzleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.mul_right, hyright, hzright, mul_one]
    · rw [FoxAlgebraicStageSemidirect.mul_left, hyright]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact
        (foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n).add_mem hyleft hzleft
  inv_mem' := by
    intro y hy
    rcases hy with ⟨hyright, hyleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.inv_right, hyright, inv_one]
    · rw [FoxAlgebraicStageSemidirect.inv_left, hyright, inv_one]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact (foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n).neg_mem hyleft

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup_coe :
    ((foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
        Subgroup (FoxAlgebraicStageSemidirect (X := X) N n)) :
          Set (FoxAlgebraicStageSemidirect (X := X) N n)) =
      foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup_le_boundaryCycleSubgroup
    [Fintype X] :
    foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ≤
      foxAlgebraicStageSemidirectBoundaryCycleSubgroup (X := X) N n

theorem foxAlgebraicStageSemiBoundaryCycleSubgroup_le_sourceKernelDerivSubgroup_iff_coord
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageSemidirectBoundaryCycleSubgroup (X := X) N n ≤
        foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n