English
A covering map induces an injection on the fundamental groupoid: distinct homotopy classes map to distinct lifted paths mapFn.
Русский
Покрывающая карта индуцирует инъекцию на фундаментальной группе; различные классы гомотопии отображаются в разные подъёмы путей mapFn.
LaTeX
$$$$\text{injective path mapFn}: E \to X \text{ on homotopy quotient}.$$$$
Lean4
/-- A covering map induces an injection on all Hom-sets of the fundamental groupoid,
in particular on the fundamental group. -/
theorem injective_path_homotopic_mapFn (e₀ e₁ : E) :
Function.Injective fun γ : Path.Homotopic.Quotient e₀ e₁ ↦ γ.mapFn ⟨p, cov.continuous⟩ :=
by
refine Quotient.ind₂ fun γ₀ γ₁ ↦ ?_
dsimp only
simp_rw [← Path.Homotopic.map_lift]
iterate 2 rw [Quotient.eq]
exact (cov.homotopicRel_iff_comp ⟨0, .inl rfl, γ₀.source.trans γ₁.source.symm⟩).mpr
