Proposition 1.31 (first part): $p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0)$ is injective

Read-back of Hatcher.coverHom_injective.

theorem coverHom_injective {E X : Type*} [TopologicalSpace E] [TopologicalSpace X]
    {p : E → X} (hp : IsCoveringMap p) {e₀ : E} {x₀ : X} (he : p e₀ = x₀) :
    Function.Injective (coverHom p hp.continuous he)

Setting and binders

• E X : Type* — two types, each in its own (implicit) universe variable; no relation between the universes is required.
• [TopologicalSpace E] [TopologicalSpace X] — arbitrary topologies. Nothing else is assumed about the spaces: not Hausdorff, not (path-/locally path-)connected, not nonempty (though E is forced nonempty by e₀, see below).
• {p : E → X} — an arbitrary function, implicit (inferred from hp).
• (hp : IsCoveringMap p) — Mathlib's covering-map predicate: for every $x\in X$, IsEvenlyCovered p x (p ⁻¹' {x}), i.e. the fibre $p^{-1}(x)$ (as a subtype) has the discrete topology, and there is an open set $U\ni x$ with $p^{-1}(U)$ open and a homeomorphism $H:p^{-1}(U)\cong U\times p^{-1}(x)$ satisfying $\mathrm{pr}_1(H(z))=p(z)$ for all $z\in p^{-1}(U)$. Surjectivity is not part of the definition; a point $x$ with empty fibre is "evenly covered" by $U\times\emptyset=\emptyset$, which forces $p^{-1}(U)=\emptyset$. Mathlib proves IsCoveringMap.continuous : Continuous p, which is what hp.continuous supplies to coverHom.
• {e₀ : E} {x₀ : X} — implicit basepoints (inferred from he).
• (he : p e₀ = x₀) — the basepoint of E maps to the basepoint of X.
• coverHom p hp.continuous he : FundamentalGroup E e₀ →* FundamentalGroup X x₀ unfolds to FundamentalGroup.mapOfEq ⟨p, hp.continuous⟩ he, which acts on a class ⟦γ⟧ (with γ : Path e₀ e₀) by

the loop $p\circ\gamma:[0,1]\to X$ based at $p(e_0)$ being re-typed as a loop at $x_0$ via he (Path.cast). Here FundamentalGroup E e₀ is Mathlib's $\pi_1(E,e_0)$: path-homotopy classes (homotopy rel $\{0,1\}$) of loops at $e_0$, with p * q = q.trans p.

Hypotheses

Only hp : IsCoveringMap p and he : p e₀ = x₀. There is no hypothesis on connectedness, local path-connectedness, or surjectivity.

Conclusion

Function.Injective (coverHom p hp.continuous he), i.e. for all $a,b\in\pi_1(E,e_0)$,

Unpacked to representatives: if $\gamma,\gamma':[0,1]\to E$ are loops at $e_0$ and $p\circ\gamma$ is homotopic rel endpoints in $X$ to $p\circ\gamma'$, then $\gamma$ is homotopic rel endpoints in $E$ to $\gamma'$. Equivalently (since coverHom is a group homomorphism), $\ker p_*$ is trivial: any loop $\gamma$ at $e_0$ with $p\circ\gamma$ null-homotopic in $X$ is null-homotopic in $E$.

In words: the homomorphism $p_*:\pi_1(E,e_0)\to\pi_1(X,x_0)$ induced by a covering map is injective.

Remarks

• Textbook match. This is Hatcher, Proposition 1.31(a): "The map $p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0)$ induced by a covering space $p:(\tilde X,\tilde x_0)\to(X,x_0)$ is injective." Hatcher's proof uses only the homotopy lifting property, which holds for covering maps without any connectedness assumptions, so the absence of connectedness hypotheses here is consistent with the textbook. Hatcher's definition of covering space does not require surjectivity either (he remarks in §1.3 that this is a matter of convention), so Mathlib's non-surjective IsCoveringMap is not a departure for this statement.
• Not vacuous. The presence of e₀ : E guarantees $E\neq\emptyset$ and that the fibre over $x_0$ is nonempty; both fundamental groups are genuine groups (nonempty, containing at least the identity class). The statement has content whenever $\pi_1(E,e_0)$ is nontrivial, and is a real theorem (requires homotopy lifting) rather than a definitional triviality.
• Non-surjective p. Points of $X$ outside the image of p play no role: $\pi_1(X,x_0)$ is computed in all of $X$, but injectivity concerns only loops that are images of loops in $E$. The statement is therefore exactly as strong as the textbook one; no weaker.
• Group-law orientation. Mathlib's FundamentalGroup multiplication is reversed relative to Hatcher (p * q = q.trans p), but injectivity of a map is insensitive to this.
• Universe. E and X may live in different universes; no constraint is imposed. (This differs from the CoveringSpace structure in the definition file, which forces E : Type u for X : Type u, but the theorem is stated for bare p, not for a CoveringSpace bundle.)
• What a reader might expect but is absent. Nothing essential. A textbook would typically also state part (b) of Prop 1.31 (description of the image subgroup), which is the separate theorem mem_coverSubgroup_iff. The theorem does not identify the image, only injectivity.
• Discrete-fibre subtlety. Mathlib's definition puts DiscreteTopology (p ⁻¹' {x}) on the fibre with the subspace topology; a homeomorphism $p^{-1}(U)\cong U\times p^{-1}(x)$ over $U$ is then the usual "disjoint union of sheets" condition. This coincides with Hatcher's definition (each point has an open neighbourhood $U$ whose preimage is a disjoint union of open sets each mapped homeomorphically onto $U$).
• The statement is a theorem with proof sorry in the audited file; the read-back concerns only the statement.