English
Let i ∈ N. If the i-th loops of p and q are homotopic, then p and q are homotopic in GenLoop N X x. Concretely, a homotopy between toLoop i p and toLoop i q lifts to a homotopy between p and q.
Русский
Пусть i ∈ N. Если i-я петля p и q гомотопны, то сами p и q в GenLoop N X x тоже гомотопны. Конкретно, гомотопия между toLoop i p и toLoop i q поднимается до гомотопии между p и q.
LaTeX
$$$\\forall i:\\, N,\\ p,q:\\,(\\GenLoop N X x).Elem\\,\n\\; (toLoop i\ p)\\homotopic(toLoop i\\ q)\\Rightarrow p\\ homotopic\\ q$$$
Lean4
theorem homotopicFrom (i : N) {p q : Ω^ N X x} : (toLoop i p).Homotopic (toLoop i q) → Homotopic p q :=
by
refine Nonempty.map fun H => ⟨⟨homotopyFrom i H, ?_, ?_⟩, ?_⟩
pick_goal 3
· rintro t y ⟨j, jH⟩
erw [homotopyFrom_apply]
obtain rfl | h := eq_or_ne j i
· simp only [Prod.map_apply, id_eq, funSplitAt_apply, Function.uncurry_apply_pair]
rw [H.eq_fst]
exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]
· rw [p.2 _ ⟨j, jH⟩]; apply boundary; exact ⟨⟨j, h⟩, jH⟩
all_goals
intro
apply (homotopyFrom_apply _ _ _).trans
simp only [Prod.map_apply, id_eq, funSplitAt_apply, Function.uncurry_apply_pair,
ContinuousMap.HomotopyWith.apply_zero, ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap,
toLoop_apply_coe, ContinuousMap.curry_apply, ContinuousMap.comp_apply]
first
| apply congr_arg p
| apply congr_arg q
apply (Cube.splitAt i).left_inv
