The locally constant degree of a covering

The cardinality of the fibres of a covering map is locally constant, including over a disconnected base and at points with empty fibres. For finite fibres this is the number of sheets. This supplies the variable degree in the transfer formula for singular homology. For infinite fibres, Nat.card has its usual value zero; no finite-sheet interpretation is asserted in that case.

The construction uses Mathlib's IsEvenlyCovered.fiberHomeomorph. See Hatcher, Algebraic Topology, Sections 1.3 and 3.G, for covering degree and transfer.

theorem IsCoveringMap.isLocallyConstant_natCard_fiber {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsCoveringMap p) : IsLocallyConstant fun (b : B) => Nat.card ↑(p ⁻¹' {b})

Fibre cardinality is locally constant for a covering, without connectedness or surjectivity assumptions. Infinite fibres have Nat.card equal to zero.

noncomputable def IsCoveringMap.degree {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsCoveringMap p) : LocallyConstant B ℕ

The locally constant fibre cardinality of a covering. For a finite covering this is its number of sheets on each connected component of the base.

@[simp]

theorem IsCoveringMap.degree_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsCoveringMap p) (b : B) : hp.degree b = Nat.card ↑(p ⁻¹' {b})

The degree at a point is the cardinality of its fibre.