Fadell--Neuwirth exactness: the kernel is contained in the image
ProvedBraidsLinksMCG.fadellNeuwirth_ker_le_rangeThe hard inclusion of exactness at the middle term of the Fadell--Neuwirth sequence: a pure braid on strands which becomes trivial after forgetting the last strand comes from a loop of that last strand alone in the plane punctured at the other points.
In symbols, for the sequence
with the first map induced by the fibre inclusion and the second by the forgetful map , the claim is .
The opposite inclusion is elementary and is already proved: the composite is the constant map at the base configuration, since forgetting the last coordinate of returns whatever is. So the composite induces the trivial homomorphism, and the image of lies in the kernel of for purely formal reasons. All the content of exactness is in the direction stated here.
The classical proof uses the homotopy lifting property. Given a loop of configurations on points whose projection is null-homotopic, lift a null-homotopy of through the fibration . The lifted homotopy deforms into a loop lying entirely in a single fibre, and that fibre is the plane punctured at the fixed points, so the deformed loop is of a loop there.
This is where it is used that the Fadell--Neuwirth projection is a fibration. That input is not available from covering-space theory, which is what distinguishes this statement from the covering-space facts about the ordered-over-unordered projection.
import Mathlib import Definitions.Def_BraidsLinksMCG_ConfigSpace
namespace BraidsLinksMCG
theorem fadellNeuwirth_ker_le_range (n : ℕ) :
(FundamentalGroup.mapOfEq (configForget n) (configForget_base n)).ker ≤
(FundamentalGroup.mapOfEq (configIncl n) (configIncl_base n)).range := by sorry
end BraidsLinksMCG