The short exact sequence of the pure link-homotopy classes (Proposition 3.8)

import Mathlib
import Definitions.Def_HGL_alg
import Definitions.Def_HGL_tor

namespace HGL

/-!  Milestone 6 (Proposition 3.8): the short exact sequence from the pure
link-homotopy classes to the full class group and onto the symmetric
group. The permutation map of the class group is surjective - every
permutation is realized by a braid - and its kernel is exactly the set of
classes of pure braids, so the sequence of Proposition 3.8 is exact. -/
theorem pure_sequence_exact {n g : ℕ} {B S Cl : Type*} [Group B] [Monoid S] [Group Cl]
    (W : LinkHomotopyWorld n g B S Cl) :
    (∀ p : Equiv.Perm (Fin n), ∃ c : Cl, W.permCl c = p) ∧
    (∀ c : Cl, W.permCl c = 1 ↔ ∃ b : B, W.perm b = 1 ∧ W.cls (W.incl b) = c) := by sorry

end HGL