English
The 0th homotopy group is in bijection with ZerothHomotopy, via the isEmpty-indexed equivalence.
Русский
0-ая гомотопия группы биективно эквивалентна ZerothHomotopy через изоморфизм с пустым индексом.
LaTeX
$$$\\mathrm{pi0EquivZerothHomotopy} : \\pi_0 X x \\simeq ZerothHomotopy X$$$
Lean4
/-- The homotopy group at `x` indexed by a singleton is in bijection with the fundamental group,
i.e. the loops based at `x` up to homotopy. -/
def homotopyGroupEquivFundamentalGroupOfUnique (N) [Unique N] : HomotopyGroup N X x ≃ FundamentalGroup X x :=
by
refine Equiv.trans ?_ (CategoryTheory.Groupoid.isoEquivHom _ _).symm
refine Quotient.congr (genLoopEquivOfUnique N) ?_
intro a₁ a₂; constructor <;> rintro ⟨H⟩
·
exact
⟨{ toFun := fun tx => H (tx.fst, fun _ => tx.snd)
map_zero_left := fun _ => H.apply_zero _
map_one_left := fun _ => H.apply_one _
prop' := fun t y iH => H.prop' _ _ ⟨default, iH⟩ }⟩
refine ⟨⟨⟨⟨fun tx => H (tx.fst, tx.snd default), H.continuous.comp ?_⟩, fun y => ?_, fun y => ?_⟩, ?_⟩⟩
· fun_prop
· exact (H.apply_zero _).trans (congr_arg a₁ (eq_const_of_unique y).symm)
· exact (H.apply_one _).trans (congr_arg a₂ (eq_const_of_unique y).symm)
· rintro t y ⟨i, iH⟩
cases Unique.eq_default i
exact (H.eq_fst _ iH).trans (congr_arg a₁ (eq_const_of_unique y).symm)
