TargetMap.lean

theorem foxAlgebraicStageSemidirectMap_left
    (y : FoxAlgebraicStageSemidirect (X := X) N n) :
    (foxAlgebraicStageSemidirectMap (X := X) hNM n y).left =
      fun i : X => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (y.left i) :=
  rfl

theorem foxAlgebraicStageSemidirectMap_right
    (y : FoxAlgebraicStageSemidirect (X := X) N n) :
    (foxAlgebraicStageSemidirectMap (X := X) hNM n y).right =
      foxAlgebraicStageTargetQuotientMap (X := X) hNM y.right

theorem foxAlgebraicStageFoxBoundary_targetMap
    [Fintype X]
    (v : foxAlgebraicStageCoordinateVector (X := X) N n) :
    foxAlgebraicStageFoxBoundary (X := X) M n
        (fun i : X => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (v i)) =
      foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (foxAlgebraicStageFoxBoundary (X := X) N n v) := by
  rw [foxAlgebraicStageFoxBoundary_apply, foxAlgebraicStageFoxBoundary_apply, map_sum]
  apply Finset.sum_congr rfl
  intro i _
  rw [map_mul, map_sub, foxAlgebraicStageTargetGroupAlgebraMap_of, map_one]

theorem foxAlgebraicStageBoundaryCycleSubmodule_targetMap_mem
    [Fintype X]
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n) :
    (fun i : X => foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n (v i)) ∈
      foxAlgebraicStageBoundaryCycleSubmodule (X := X) M n := by
  rw [mem_foxAlgebraicStageBoundaryCycleSubmodule]
  rw [foxAlgebraicStageFoxBoundary_targetMap (X := X) hNM n v]
  rw [mem_foxAlgebraicStageBoundaryCycleSubmodule] at hv
  rw [hv]
  exact map_zero _

theorem foxAlgebraicStageSemidirectMap_mem_boundaryCycleSet
    [Fintype X]
    {y : FoxAlgebraicStageSemidirect (X := X) N n}
    (hy : y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) M n

theorem foxAlgebraicStageSemidirectMap_kernelWordPoint
    (w : FreeGroup X) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n
        (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) M n w

theorem foxAlgebraicStageSemidirectMap_sourceKernelPoint
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSemidirectMap (X := X) hNM n
        (foxAlgebraicStageSemidirectSourceKernelPoint (X := X) N n q) =
      foxAlgebraicStageSemidirectSourceKernelPoint (X := X) M n
        (foxAlgebraicStageSourceQuotientMap (X := X) hNM n q)

theorem foxAlgebraicStageSemidirectMap_kernelWordDerivativeSet_subset :
    (fun y : FoxAlgebraicStageSemidirect (X := X) N n =>
        foxAlgebraicStageSemidirectMap (X := X) hNM n y) ''
      foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
        foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) M n := by
  intro y hy
  rcases hy with ⟨z, hz, rfl⟩
  rcases hz with ⟨w, hwN, hzw⟩
  refine ⟨w, hNM hwN, ?_⟩
  rw [← hzw]
  exact (foxAlgebraicStageSemidirectMap_kernelWordPoint (X := X) hNM n w).symm

theorem foxAlgebraicStageSemidirectMap_sourceKernelDerivativeSet_subset :
    (fun y : FoxAlgebraicStageSemidirect (X := X) N n =>
        foxAlgebraicStageSemidirectMap (X := X) hNM n y) ''
      foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
        foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) M n := by
  rw [foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) N n,
    foxAlgebraicStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) M n]
  exact foxAlgebraicStageSemidirectMap_kernelWordDerivativeSet_subset (X := X) hNM n