Proposition 1.32: the number of sheets equals the index of $p_*\pi_1(\tilde X,\tilde x_0)$

Read-back of Hatcher.fiber_equiv_cosets.

theorem fiber_equiv_cosets {E X : Type*} [TopologicalSpace E] [TopologicalSpace X]
    [PathConnectedSpace E] [PathConnectedSpace X]
    {p : E → X} (hp : IsCoveringMap p) {e₀ : E} {x₀ : X} (he : p e₀ = x₀) :
    Nonempty (p ⁻¹' {x₀} ≃ FundamentalGroup X x₀ ⧸ coverSubgroup p hp.continuous he)

Setting and binders

• E X : Type* — two types in independent universes (Type u_1, Type u_2). There is no requirement that total space and base live in the same universe.
• [TopologicalSpace E] [TopologicalSpace X] — arbitrary topologies; no separation, compactness, or local-connectedness axioms.
• [PathConnectedSpace E] and [PathConnectedSpace X] — Mathlib's class has two fields: nonempty : Nonempty _ and joined : ∀ x y, Joined x y, where Joined x y := Nonempty (Path x y). So each of $E$ and $X$ is nonempty and any two of its points are the endpoints of some continuous path $[0,1]\to$ space.
• {p : E → X} — a bare function (implicit; determined by hp).
• hp : IsCoveringMap p — Mathlib's definition: ∀ x, IsEvenlyCovered p x (p ⁻¹' {x}), and IsEvenlyCovered p x I is

Here $I = p^{-1}(\{x\})$ with the subspace topology. Thus: every point of $X$ has an open neighbourhood $U$ over which $p$ is a trivial bundle with discrete fibre $p^{-1}(x)$. Mathlib does not require $p$ to be surjective: the fibre may be empty (then $p^{-1}(U)=\emptyset$ for some open $U\ni x$). IsCoveringMap p implies Continuous p, which is what hp.continuous supplies to coverSubgroup.

• {e₀ : E} {x₀ : X} and he : p e₀ = x₀ — a chosen basepoint in $E$ and its image. In particular the fibre over $x_0$ is nonempty (it contains $e_0$).

Definitions from the bundle that occur:

• coverHom p hp he : FundamentalGroup E e₀ →* FundamentalGroup X x₀ is FundamentalGroup.mapOfEq ⟨p, hp⟩ he. FundamentalGroup X x is (an abbreviation for) End (FundamentalGroupoid.mk x), i.e. the group of homotopy-rel-endpoints classes of loops at $x$, $\pi_1(X,x)$. mapOfEq f h is map f x (push-forward of loop classes along $f$) composed with the group isomorphism $\pi_1(X, f e_0)\cong\pi_1(X,x_0)$ induced by the equality h : f e₀ = x₀ (eqToIso … .conj). Mathematically this is just $p_*:\pi_1(E,e_0)\to\pi_1(X,x_0)$.
• coverSubgroup p hp he : Subgroup (FundamentalGroup X x₀) is (coverHom p hp he).range, i.e. the image subgroup $H := p_*\big(\pi_1(E,e_0)\big)\le \pi_1(X,x_0)$.

Hypotheses

1. $E$ and $X$ are nonempty path-connected topological spaces.
2. $p : E\to X$ is a covering map in Mathlib's sense (local triviality with discrete fibres; surjectivity not assumed).
3. $p(e_0)=x_0$.

Conclusion

Nonempty (p ⁻¹' {x₀} ≃ FundamentalGroup X x₀ ⧸ coverSubgroup p hp.continuous he).

• p ⁻¹' {x₀} is coerced to the subtype $\{e : E \mid p(e)=x_0\}$, the fibre over $x_0$ (as a bare type; its topology is irrelevant here).
• FundamentalGroup X x₀ ⧸ coverSubgroup … is Mathlib's HasQuotient for a group by a Subgroup: the quotient of $\pi_1(X,x_0)$ by QuotientGroup.leftRel H, where leftRel H a b ↔ a⁻¹ * b ∈ H. So it is the set of left cosets $\{ gH : g\in\pi_1(X,x_0)\}$ — a plain type, with no group structure asserted ($H$ is not assumed normal) and no topology.
• ≃ is Equiv: a bijection with two-sided inverse. Nonempty (_ ≃ _) is the proposition "there exists some bijection".

In words: there exists a bijection between the fibre $p^{-1}(x_0)$ and the set of left cosets $\pi_1(X,x_0)/p_*\pi_1(E,e_0)$. Equivalently (cardinality form) the number of sheets over $x_0$ equals the index $[\pi_1(X,x_0) : p_*\pi_1(E,e_0)]$, as cardinals.

Remarks

• Compared with Hatcher, Prop. 1.32. Hatcher's hypotheses are exactly "$p:(\tilde X,\tilde x_0)\to(X,x_0)$ a covering space with $\tilde X$ and $X$ path-connected", and his conclusion is that the number of sheets equals the index of $p_*\pi_1(\tilde X,\tilde x_0)$ in $\pi_1(X,x_0)$. The Lean statement matches these hypotheses. No local path-connectedness of $X$ is assumed, consistent with Hatcher.
• Only existence of a bijection is asserted. Hatcher's proof produces the specific bijection $\Phi : H[\gamma]\mapsto \tilde\gamma(1)$ (endpoint of the lift of $\gamma$ starting at $\tilde x_0$). The Lean statement does not name or characterise the bijection; it is a pure cardinality statement. A reader wanting "the canonical bijection" gets strictly less.
• Surjectivity of $p$ is not assumed but follows. Since Mathlib covering maps are open, and the set of points with empty fibre is open (an empty fibre over $x$ yields an open $U\ni x$ with $p^{-1}(U)=\emptyset$), the image of $p$ is clopen; it is nonempty (contains $x_0$) and $X$ is connected, so $p$ is onto. So no weakening arises from the missing surjectivity hypothesis in this theorem.
• Nonempty-ness. Both PathConnectedSpace instances force $E,X\neq\emptyset$; independently the fibre over $x_0$ contains $e_0$ and the coset space contains the class of $1$. So neither side is empty and the statement is not vacuous.
• Trivial instances. If $E = X$ and $p=\mathrm{id}$, the fibre is a singleton and $H=\pi_1(X,x_0)$ gives one coset: consistent. If $E$ is simply connected, $H=1$ and the statement says $|p^{-1}(x_0)| = |\pi_1(X,x_0)|$ (as cardinals).
• Group-law convention. End in Mathlib multiplies by f * g = g ≫ f, so the group law on FundamentalGroup is reverse concatenation relative to some textbooks. This does not affect the image subgroup as a set nor the coset count.
• Universes. The fibre lives in Type u_1 and the coset type in Type u_2; Equiv between different universes is allowed, so no universe restriction is imposed.
• Nothing is said about the fibre over other points $x\neq x_0$ (though by connectedness of $X$ all fibres have the same cardinality; this is not part of the statement).