Read-back of the definition bundle Def_Hatcher_Covering (namespace Hatcher)

Everything below is a literal transcription of what the Lean declarations assert, with the relevant Mathlib definitions unpacked. The whole file is inside noncomputable section and namespace Hatcher; one universe variable u is declared.

Mathlib background used throughout

• Path x y (for x y : X, X a topological space) is a continuous map $\gamma : [0,1] \to X$ (domain unitInterval, the subtype $\{t \in \mathbb{R} \mid 0 \le t \le 1\}$) with $\gamma(0)=x$, $\gamma(1)=y$. γ t is function application after coercion.
• Path.Homotopic γ γ' is Nonempty (γ.Homotopy γ'), and Path.Homotopy is ContinuousMap.HomotopyRel γ γ' {0,1}: a continuous $H:[0,1]\times[0,1]\to X$ with $H(0,\cdot)=\gamma$, $H(1,\cdot)=\gamma'$ and $H(s,t)=\gamma(t)$ for $t\in\{0,1\}$. So it is homotopy relative to the endpoints (a homotopy of paths in the textbook sense), taking place in the ambient space $X$.
• Path.Homotopic.Quotient x y is Quotient (Path.Homotopic.setoid x y), the set of path-homotopy classes of paths from $x$ to $y$.
• FundamentalGroup X x is the abbreviation End (FundamentalGroupoid.mk x). Since the Hom-sets of FundamentalGroupoid X are Path.Homotopic.Quotient x.as y.as and composition is Path.Homotopic.Quotient.trans, the underlying set is exactly $\pi_1(X,x)$ = path-homotopy classes of loops at $x$. The group law is the endomorphism-monoid law, p * q = q ≫ p, i.e. p * q = q.trans p (Mathlib's FundamentalGroup.mul_def): "$p\cdot q$" traverses $q$ first and then $p$. This is the opposite of Hatcher's convention $[f][g]=[f\cdot g]$ (traverse $f$ first). The two groups are anti-isomorphic, hence isomorphic via $g\mapsto g^{-1}$; images/subgroups/normality are unaffected as sets, but any statement involving specific products must be read with the reversed order. 1 = ⟦Path.refl x⟧, p⁻¹ = p.symm.
• FundamentalGroup.mapOfEq (f : C(X,Y)) (h : f x = y) : π₁(X,x) →* π₁(Y,y) satisfies (Mathlib's mapOfEq_apply) mapOfEq f h p = (Path.Homotopic.Quotient.map p f).cast h.symm h.symm, i.e. $[\gamma]\mapsto [f\circ\gamma]$, with the endpoints of $f\circ\gamma$ (which are $f(x)$) re-labelled as $y$ using $h$. It is the induced homomorphism $f_*$.
• IsCoveringMap p (Mathlib, Topology/Covering/Basic.lean) is ∀ x, IsEvenlyCovered p x (p ⁻¹' {x}), where IsEvenlyCovered f x I is DiscreteTopology I ∧ ∃ U : Set X, x ∈ U ∧ IsOpen U ∧ IsOpen (f ⁻¹' U) ∧ ∃ H : f ⁻¹' U ≃ₜ U × I, ∀ z, (H z).1.1 = f z. So: every $x\in X$ has an open neighbourhood $U$ such that $p^{-1}(U)$ is open and there is a homeomorphism $p^{-1}(U)\cong U\times p^{-1}(x)$ over $U$, with $p^{-1}(x)$ discrete. Surjectivity is not required; the fibre $p^{-1}(x)$ may be empty (Mathlib's own file comment says so explicitly), in which case $p^{-1}(U)=\emptyset$. Such a p is automatically continuous (IsCoveringMap.continuous). No connectedness, Hausdorffness, or local-connectedness is imposed on $E$ or $X$.
• nhds x (𝓝 x) is the neighbourhood filter; U ∈ nhds x means there is an open $t$ with $x\in t\subseteq U$ (mem_nhds_iff). U itself need not be open.
• Group structure on E ≃ₜ E (Topology/Homeomorph/Defs.lean): mul f g := g.trans f, so (f * g) e = f (g e) (ordinary composition, f applied last); 1 = Homeomorph.refl E; f⁻¹ = f.symm.
• MonoidHom.range φ is the subgroup with carrier Set.range φ; y ∈ φ.range ↔ ∃ x, φ x = y.
• MulAction.orbitRel G α is the setoid with a ≈ b ↔ a ∈ MulAction.orbit G b, i.e. $\exists g,\ g\cdot b=a$. MulAction.orbitRel.Quotient G α is the abbreviation Quotient (orbitRel G α). If α has a topology, the instance instTopologicalSpaceQuotient gives Quotient s the topology coinduced by Quotient.mk', i.e. the quotient topology ($V$ open iff its preimage is open).

---

1. IsSemilocallySimplyConnected

variable (X : Type*) [TopologicalSpace X]
def IsSemilocallySimplyConnected : Prop :=
  ∀ x : X, ∃ U ∈ nhds x, ∀ γ : Path x x, (∀ t, γ t ∈ U) → γ.Homotopic (Path.refl x)

Parameters. X : Type* (its own universe variable, explicit argument), [TopologicalSpace X].

Assertion. For every point $x\in X$ there is a set $U$ that is a neighbourhood of $x$ (contains an open set containing $x$; $U$ need not be open) such that every loop $\gamma:[0,1]\to X$ based at $x$ whose image lies entirely in $U$ (i.e. $\gamma(t)\in U$ for all $t\in[0,1]$) is path-homotopic in $X$ (rel endpoints) to the constant loop at $x$.

Remarks.

• Only loops based at $x$ lying in $U$ are tested, not loops based at other points of $U$. This matches Hatcher's definition (each $x$ has a neighbourhood $U$ with $\pi_1(U,x)\to\pi_1(X,x)$ trivial), because $\pi_1(U,x)$ is exactly loops at $x$ in $U$ modulo homotopy in $U$, and "the induced map is trivial" means each such loop is null-homotopic in $X$.
• The non-openness of $U$ is harmless: if $U$ works then any subset of $U$ containing $x$ works, so one may shrink to an open set. The condition is equivalent to the textbook one.
• For an empty X the statement is vacuously true.

2. coverHom

variable {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] (p : E → X)
def coverHom (hp : Continuous p) {e₀ : E} {x₀ : X} (he : p e₀ = x₀) :
    FundamentalGroup E e₀ →* FundamentalGroup X x₀ :=
  FundamentalGroup.mapOfEq ⟨p, hp⟩ he

Parameters. Topological spaces E, X (separate Type* universes), an arbitrary function p : E → X (explicit), a proof hp that p is continuous, implicit points e₀ : E, x₀ : X, and he : p e₀ = x₀.

Object defined. The group homomorphism $p_*:\pi_1(E,e_0)\to\pi_1(X,x_0)$, $[\gamma]\mapsto[p\circ\gamma]$ (endpoints relabelled from $p(e_0)$ to $x_0$ via he). No covering hypothesis: it is the induced map of any continuous map.

3. coverSubgroup

def coverSubgroup (hp : Continuous p) {e₀ : E} {x₀ : X} (he : p e₀ = x₀) :
    Subgroup (FundamentalGroup X x₀) := (coverHom p hp he).range

Object defined. The subgroup $p_*\pi_1(E,e_0)\le\pi_1(X,x_0)$, i.e. $\{g \mid \exists h\in\pi_1(E,e_0),\ p_*h=g\}$. Same parameters as coverHom. Again defined for any continuous p, not only coverings.

4. deckGroup

def deckGroup : Subgroup (E ≃ₜ E) where
  carrier := {f | ∀ e, p (f e) = p e}
  ...

Parameters. E, X topological spaces, p : E → X an arbitrary function (explicit; no continuity or covering hypothesis).

Object defined. The subgroup of the group of self-homeomorphisms $E\cong E$ consisting of those $f$ with $p\circ f=p$. Group operation: (f * g) e = f (g e) (composition, g first), identity Homeomorph.refl, inverse f.symm. The mul_mem', one_mem', inv_mem' fields check closure under these.

Remarks. This is the standard deck-transformation group $G(\tilde X)$ of Hatcher §1.3, extended verbatim to any map. It uses the full homeomorphism group, so members are automatically continuous with continuous inverse.

5. IsNormalCover

def IsNormalCover : Prop := ∀ e e' : E, p e = p e' → ∃ f ∈ deckGroup p, f e = e'

Assertion. For every pair $e,e'\in E$ with $p(e)=p(e')$ there is a deck transformation $f$ (self-homeomorphism with $p\circ f=p$) with $f(e)=e'$: the deck group acts transitively on every fibre.

Remarks. Exactly Hatcher's definition of a normal covering ("for each $x$ and each pair of lifts $\tilde x,\tilde x'$ there is a deck transformation taking $\tilde x$ to $\tilde x'$"). However p here is any function; no hypothesis that it is a covering or that $E$ is connected. Vacuously true when E is empty.

6. CoveringSpace

variable (X : Type u) [TopologicalSpace X]
structure CoveringSpace where
    E : Type u
  [topE : TopologicalSpace E]
    p : E → X
  isCoveringMap : IsCoveringMap p
attribute [instance] CoveringSpace.topE

Object defined. A structure bundling a type E in the same universe u as X (a genuine restriction compared to the Type* sections; e.g. no Type (u+1) total spaces), a topology on E (registered as an instance), a map p : E → X, and a proof that p is a covering map in Mathlib's sense (locally trivial with discrete fibres, fibres possibly empty, p not necessarily surjective, E not necessarily nonempty or connected).

7. PointedCover

structure PointedCover (x₀ : X) extends CoveringSpace X where
    e₀ : E
  p_e₀ : p e₀ = x₀

Object defined. A CoveringSpace X together with a point e₀ : E and a proof $p(e_0)=x_0$. Since e₀ exists, E is nonempty and the fibre over $x_0$ is nonempty.

8. IsIsomorphic

variable {X}
def IsIsomorphic (C₁ C₂ : CoveringSpace X) : Prop :=
  ∃ f : C₁.E ≃ₜ C₂.E, ∀ e, C₂.p (f e) = C₁.p e

Assertion. There is a homeomorphism $f:E_1\to E_2$ with $p_2\circ f=p_1$. This is Hatcher's isomorphism of covering spaces (of the same base $X$, unpointed).

9. PointedCover.subgroup

def PointedCover.subgroup {x₀ : X} (C : PointedCover X x₀) : Subgroup (FundamentalGroup X x₀) :=
  coverSubgroup C.p C.isCoveringMap.continuous C.p_e₀

Object defined. The subgroup $p_*\pi_1(E,e_0)\le\pi_1(X,x_0)$ attached to a pointed cover; continuity of p is derived from the covering hypothesis. This is the "induced subgroup" $H=p_*\pi_1(\tilde X,\tilde x_0)$ of Hatcher Thm 1.38.

10. IsPointedIsomorphic

def IsPointedIsomorphic {x₀ : X} (C₁ C₂ : PointedCover X x₀) : Prop :=
  ∃ f : C₁.E ≃ₜ C₂.E, (∀ e, C₂.p (f e) = C₁.p e) ∧ f C₁.e₀ = C₂.e₀

Assertion. There is a homeomorphism $f:E_1\to E_2$ with $p_2\circ f=p_1$ and $f(e_{0,1})=e_{0,2}$: basepoint-preserving isomorphism of covering spaces.

11. IsCoveringSpaceAction

variable (G : Type*) [Group G] (Y : Type*) [TopologicalSpace Y] [MulAction G Y]
def IsCoveringSpaceAction : Prop :=
  (∀ g : G, Continuous fun y : Y => g • y) ∧
    ∀ y : Y, ∃ U ∈ nhds y, ∀ g : G, ((fun z => g • z) '' U ∩ U).Nonempty → g = 1

Parameters. A group G (no topology on G), a topological space Y, and a (left) group action G on Y (MulAction: 1 • y = y, (g h) • y = g • (h • y)).

Assertion. (i) For every $g$, the map $y\mapsto g\cdot y$ is continuous (hence, having continuous inverse $y \mapsto g^{-1}\cdot y$, a homeomorphism). (ii) Every $y\in Y$ has a neighbourhood $U$ (in nhds y, not necessarily open) such that for every $g\in G$, if $g\cdot U\cap U\neq\emptyset$ then $g=1$. (Because '' has precedence 80 and ∩ has 70, the expression is ((g • ·) '' U) ∩ U.)

Remarks. Hatcher's condition (§1.3, "covering space action") is: each $y$ has a neighbourhood $U$ with $g_1(U)\cap g_2(U)\neq\emptyset\Rightarrow g_1=g_2$. Applying $g_2^{-1}$ shows this is equivalent to (ii). Non-openness of $U$ is harmless (shrinking $U$ preserves the property). The condition forces the action to be free. It is vacuously satisfied by the empty space.

12. OrbitSpace

abbrev OrbitSpace : Type _ := MulAction.orbitRel.Quotient G Y

Object defined. The quotient set $Y/G$ of Y by the orbit relation $y\sim y' \iff \exists g,\ g\cdot y'=y$, equipped (through the Quotient instance) with the quotient topology coinduced by the projection. As an abbrev it unfolds transparently, so all Quotient API and instances apply.

13. orbitProj

def orbitProj : Y → OrbitSpace G Y := Quotient.mk _

Object defined. The canonical projection $Y\to Y/G$, $y\mapsto[y]$ (the setoid argument is inferred as orbitRel G Y).

14. continuous_orbitProj

theorem continuous_orbitProj : Continuous (orbitProj G Y) := continuous_quotient_mk'

Assertion. The projection $Y\to Y/G$ is continuous. This is immediate from the definition of the quotient (coinduced) topology; it carries no content beyond that, and does not assert that the projection is open or a covering map.

---

Global remarks

• Universes. Sections SpaceProperties, CoveringMap, GroupActions use Type* (independent universe variables for each type). Section Classification fixes X : Type u and forces E : Type u in CoveringSpace; FundamentalGroup X x₀ : Type u as well.
• What is not assumed anywhere. No definition requires $X$ or $E$ to be path-connected, locally path-connected, nonempty, Hausdorff, or that p be surjective. The Mathlib IsCoveringMap permits empty fibres. The deckGroup/IsNormalCover/coverHom/coverSubgroup definitions do not even require p to be a covering (only continuity, where needed). Consequently theorems about these notions need to import the appropriate hypotheses explicitly, and a textbook reader should check each theorem for them.
• Group-law orientation. FundamentalGroup multiplication is p * q = q.trans p, reversed relative to Hatcher. This does not change which subsets are subgroups, images, kernels, or normal subgroups, but it does change the reading of any explicit product or conjugation formula.