English
From a loop in a reduced dimension, one can reconstruct the higher-dimensional loop via fromLoop, and toLoop then recovers the original.
Русский
Из петли меньшей размерности можно восстановить более высокую размерность петли через fromLoop, а затем toLoop восстанавливает исходное.
LaTeX
$$toLoop i (fromLoop i p) = p$$
Lean4
/-- Generalized loop from a loop by uncurrying $I → (I^{N\setminus\{j\}} → X)$ into $I^N → X$. -/
@[simps]
def fromLoop (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : Ω^ N X x :=
⟨(ContinuousMap.comp ⟨Subtype.val, by fun_prop⟩ p.toContinuousMap).uncurry.comp (Cube.splitAt i),
by
rintro y ⟨j, Hj⟩
simp only [ContinuousMap.comp_apply, ContinuousMap.coe_coe, funSplitAt_apply, ContinuousMap.uncurry_apply,
ContinuousMap.coe_mk, Function.uncurry_apply_pair]
obtain rfl | Hne := eq_or_ne j i
· rcases Hj with Hj | Hj <;> simp only [Hj, p.coe_toContinuousMap, p.source, p.target] <;> rfl
· exact GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩⟩
