The inclusion-induced homomorphism descends to the link-homotopy quotients
DisprovedESL.f_hat_welldefinedThe homomorphism induced by the inclusion of the disk into the surface descends to the link-homotopy quotients: there is an induced homomorphism from the link-homotopy classes of pure braids of the disk to the link-homotopy classes of pure braids of the surface, carrying the class of a pure braid of the disk to the class of its image. The descent is possible because the inclusion carries link-homotopically trivial braids of the disk to link-homotopically trivial braids of the surface.
import Mathlib import Definitions.Def_ESL_alg import Definitions.Def_ESL_tor
namespace ESL
/-! Milestone 3: the homomorphism f_n descends to the link-homotopy
quotients. Since f_n carries the trivial pure braids of the disk into the
trivial pure braids of the surface, there is an induced homomorphism
f-hat carrying the class of a pure braid of the disk to the class of its
image, making the square commute. -/
theorem f_hat_welldefined {n : ℕ} {PB_D PB_M HhatD HhatM Pi : Type*}
[Group PB_D] [Group PB_M] [Group HhatD] [Group HhatM] [Group Pi]
(W : StringLinkExactWorld n PB_D PB_M HhatD HhatM Pi) :
∃ fhat : HhatD →* HhatM, ∀ x : PB_D, fhat (W.qD x) = W.qM (W.f x) := by sorry
end ESL
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in the world of the exact sequence, there exists a homomorphism from the link-homotopy quotient of the disk pure braid group to the link-homotopy quotient of the surface pure braid group such that the class of a disk braid is carried to the class of its image under the inclusion-induced homomorphism. Hypotheses: the world is given; no further hypotheses appear.