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, names the resulting full subcategory TauCeti.FiniteCoveringSpace X, and gives it the same constructor API that TauCeti.CoveringSpace and TauCeti.ConnectedCoveringSpace carry.

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, proj, homMk, isoMk, forget, fullyFaithfulForget, isIso_iff_isHomeomorph_hom_left: the constructor API.
• TauCeti.hasFiniteFibers_of_finite_fiber: over a path-connected base, one finite fibre makes all fibres finite.

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.

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})

@[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.

@[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

• TauCeti.FiniteCoveringSpace X = (TauCeti.Over.isCoveringMap X ⊓ TauCeti.Over.hasFiniteFibers X).FullSubcategory

@[reducible, inline]

abbrev TauCeti.FiniteCoveringSpace.forget (X : TopCat) : CategoryTheory.Functor (FiniteCoveringSpace X) (CoveringSpace X)

The fully faithful inclusion of finite covering spaces into all covering spaces.

Equations

• TauCeti.FiniteCoveringSpace.forget X = CategoryTheory.ObjectProperty.ιOfLE ⋯

@[reducible, inline]

abbrev TauCeti.FiniteCoveringSpace.totalSpace (X : TopCat) : CategoryTheory.Functor (FiniteCoveringSpace X) TopCat

The functor taking a finite covering space to its total space.

Equations

• TauCeti.FiniteCoveringSpace.totalSpace X = (TauCeti.FiniteCoveringSpace.forget X).comp (TauCeti.CoveringSpace.totalSpace X)

@[instance_reducible]

instance TauCeti.FiniteCoveringSpace.instCoeOutTopCat {X : TopCat} : CoeOut (FiniteCoveringSpace X) TopCat

A finite covering space over X coerces to its total space.

Equations

• TauCeti.FiniteCoveringSpace.instCoeOutTopCat = { coe := fun (p : TauCeti.FiniteCoveringSpace X) => p.obj.left }

def TauCeti.FiniteCoveringSpace.mk {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (x : ↑X), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {x})) : FiniteCoveringSpace X

Construct a finite covering space from a covering map with finite fibres.

Equations

• TauCeti.FiniteCoveringSpace.mk p hp hfin = { obj := CategoryTheory.Over.mk p, property := ⋯ }

@[simp]

theorem TauCeti.FiniteCoveringSpace.mk_coe {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (x : ↑X), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {x})) : (mk p hp hfin).obj.left = E

@[reducible, inline]

abbrev TauCeti.FiniteCoveringSpace.proj {X : TopCat} (p : FiniteCoveringSpace X) : p.obj.left ⟶ X

The projection of a finite covering space to its base.

Equations

• p.proj = p.obj.hom

@[simp]

theorem TauCeti.FiniteCoveringSpace.forget_obj_coe {X : TopCat} (p : FiniteCoveringSpace X) : ((forget X).obj p).obj.left = p.obj.left

@[simp]

theorem TauCeti.FiniteCoveringSpace.forget_obj_proj {X : TopCat} (p : FiniteCoveringSpace X) : ((forget X).obj p).proj = p.proj

@[simp]

theorem TauCeti.FiniteCoveringSpace.forget_map_hom_left {X : TopCat} {p q : FiniteCoveringSpace X} (f : p ⟶ q) : CategoryTheory.Over.Hom.left ((forget X).map f).hom = CategoryTheory.Over.Hom.left f.hom

@[simp]

theorem TauCeti.FiniteCoveringSpace.mk_proj {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (x : ↑X), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {x})) : (mk p hp hfin).proj = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) p

theorem TauCeti.FiniteCoveringSpace.isCoveringMap_proj {X : TopCat} (p : FiniteCoveringSpace X) : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p.proj)

The projection from an object of FiniteCoveringSpace X is a covering map.

instance TauCeti.FiniteCoveringSpace.finite_fiber {X : TopCat} (p : FiniteCoveringSpace X) (x : ↑X) : Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x})

Every fibre of a finite covering space is finite.

def TauCeti.FiniteCoveringSpace.fullyFaithfulForget (X : TopCat) : (forget X).FullyFaithful

The inclusion FiniteCoveringSpace X ⥤ CoveringSpace X is fully faithful.

Equations

• TauCeti.FiniteCoveringSpace.fullyFaithfulForget X = CategoryTheory.ObjectProperty.fullyFaithfulιOfLE ⋯

@[simp]

theorem TauCeti.FiniteCoveringSpace.totalSpace_obj {X : TopCat} (p : FiniteCoveringSpace X) : (totalSpace X).obj p = p.obj.left

@[simp]

theorem TauCeti.FiniteCoveringSpace.totalSpace_map {X : TopCat} {p q : FiniteCoveringSpace X} (f : p ⟶ q) : (totalSpace X).map f = CategoryTheory.Over.Hom.left f.hom

theorem TauCeti.FiniteCoveringSpace.w {X : TopCat} {p q : FiniteCoveringSpace X} (f : p ⟶ q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom) q.proj = p.proj

A morphism of finite covering spaces commutes with the projections to the base.

theorem TauCeti.FiniteCoveringSpace.w_assoc {X : TopCat} {p q : FiniteCoveringSpace X} (f : p ⟶ q) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom) (CategoryTheory.CategoryStruct.comp q.proj h) = CategoryTheory.CategoryStruct.comp p.proj h

A morphism of finite covering spaces commutes with the projections to the base.

def TauCeti.FiniteCoveringSpace.homMk {X : TopCat} {p q : FiniteCoveringSpace X} (f : p.obj.left ⟶ q.obj.left) (w : CategoryTheory.CategoryStruct.comp f q.proj = p.proj := by cat_disch) : p ⟶ q

Construct a morphism of finite covering spaces from a continuous map over the base.

Equations

• TauCeti.FiniteCoveringSpace.homMk f w = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk f w)

@[simp]

theorem TauCeti.FiniteCoveringSpace.homMk_hom_left {X : TopCat} {p q : FiniteCoveringSpace X} (f : p.obj.left ⟶ q.obj.left) (w : CategoryTheory.CategoryStruct.comp f q.proj = p.proj) : CategoryTheory.Over.Hom.left (homMk f w).hom = f

def TauCeti.FiniteCoveringSpace.isoMk {X : TopCat} {p q : FiniteCoveringSpace X} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj := by cat_disch) : p ≅ q

Construct an isomorphism of finite covering spaces from an isomorphism of their total spaces over the base.

Equations

• TauCeti.FiniteCoveringSpace.isoMk e w = (TauCeti.Over.isCoveringMap X ⊓ TauCeti.Over.hasFiniteFibers X).isoMk (CategoryTheory.Over.isoMk e w)

@[simp]

theorem TauCeti.FiniteCoveringSpace.isoMk_hom_hom_left {X : TopCat} {p q : FiniteCoveringSpace X} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj) : CategoryTheory.Over.Hom.left (isoMk e w).hom.hom = e.hom

@[simp]

theorem TauCeti.FiniteCoveringSpace.isoMk_inv_hom_left {X : TopCat} {p q : FiniteCoveringSpace X} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj) : CategoryTheory.Over.Hom.left (isoMk e w).inv.hom = e.inv

theorem TauCeti.FiniteCoveringSpace.isIso_iff_isHomeomorph_hom_left {X : TopCat} {p q : FiniteCoveringSpace X} (f : p ⟶ q) : CategoryTheory.IsIso f ↔ IsHomeomorph ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom))

A map of finite covering spaces is an isomorphism exactly when its map of total spaces is a homeomorphism.

theorem TauCeti.hasFiniteFibers_of_finite_fiber {X : TopCat} [PathConnectedSpace ↑X] (p : CoveringSpace X) (x₀ : ↑X) (h : Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})) : Over.hasFiniteFibers X p.obj

Over a path-connected base one finite fibre makes a covering space finite.