Finite covering spaces #

A covering space is finite when all of its fibres are finite. This file records that condition as a property of an object of TopCat / X and names the resulting full subcategory TauCeti.FiniteCoveringSpace X, as an instance of TauCeti.CoveringSpace.FullSubcategory.

That general type carries the shared API, which is used here rather than restated; its docstring says how to name its members from a subcategory. What this file adds is the finiteness property, the constructor family and the inclusion functor — which are given again because they pin P down to finiteness — and TauCeti.FiniteCoveringSpace.finite_fiber, recording finiteness of every fibre as an instance.

Finiteness of all fibres is one condition rather than infinitely many as soon as the base is path connected: monodromy along a path is a bijection between the fibres over its endpoints, so the fibres over any two points of a path component are in bijection. That is TauCeti.coveringFiberEquiv, from TauCeti.Topology.Homotopy.Monodromy.Basic, and TauCeti.hasFiniteFibers_of_finite_fiber is the resulting one-point criterion.

Finite covers are the covering-space side of the Galois-category picture: the fibre over a basepoint is a finite set with an action of π₁, and it is only for finite covers that the fibre functor lands in FintypeCat.

Main declarations #

TauCeti.Over.hasFiniteFibers and TauCeti.Over.hasFiniteFibers_iff: the property of an object of TopCat / X that all fibres of its structure morphism are finite, and its membership lemma.
TauCeti.FiniteCoveringSpace: finite covering spaces over X.
TauCeti.FiniteCoveringSpace.mk, mk_coe, mk_proj, forget_obj_mk and forget: the constructor, its computation lemmas and the inclusion into all covering spaces. The rest of the API is TauCeti.CoveringSpace.FullSubcategory's.
TauCeti.FiniteCoveringSpace.finite_fiber: every fibre of a finite covering space is finite.
TauCeti.hasFiniteFibers_of_finite_fiber: over a path-connected base, one finite fibre makes all fibres finite.

source

theorem TauCeti.finite_fiber_of_finite_fiber {E : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [PathConnectedSpace X] (hp : IsCoveringMap p) {x₀ : X} (h : Finite ↑(p ⁻¹' {x₀})) (x : X) :

Finite ↑(p ⁻¹' {x})

Over a path-connected base, a covering map with one finite fibre has all fibres finite.

source

def TauCeti.Over.hasFiniteFibers (X : TopCat) :

CategoryTheory.ObjectProperty (CategoryTheory.Over X)

The property of an object of TopCat / X that all fibres of its structure morphism are finite.

Equations

TauCeti.Over.hasFiniteFibers X p = ∀ (x : ↑X), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p.hom) ⁻¹' {x})

Instances For

source

@[simp]

theorem TauCeti.Over.hasFiniteFibers_iff {X : TopCat} {p : CategoryTheory.Over X} :

hasFiniteFibers X p ↔ ∀ (x : ↑X), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p.hom) ⁻¹' {x})

Membership in the finite-fibre property of objects of TopCat / X.

source

@[reducible, inline]

abbrev TauCeti.FiniteCoveringSpace (X : TopCat) :

Type (u + 1)

The category of finite covering spaces over X: covering maps to X all of whose fibres are finite, and continuous maps commuting with the projections to X.

Equations