Finite covering spaces form a Galois category

Let X be path connected, locally path connected and semilocally simply connected, and fix a basepoint x₀. This file proves that the finite covering spaces of X form a Galois category in the sense of SGA1, with fibre functor the fibre over x₀:

TauCeti.FiniteCoveringSpace.fiberFunctor x₀ : FiniteCoveringSpace X ⥤ FintypeCat.

This is the Galois-category lens on the classification of covering spaces, the third of the three routes the roadmap asks for; the fundamental-groupoid lens is TauCeti.CoveringSpace.monodromyEquivalence and the π₁(X, x₀)-set lens is TauCeti.CoveringSpace.fiberActionEquivalence.

Nothing here re-proves the axioms for covering spaces. The classification already identifies covering spaces of X with π₁(X, x₀)-sets, and that identification restricts to finite covers on one side and finite π₁(X, x₀)-sets on the other, because the fibre-action functor sends a cover to its fibre over x₀. Finiteness of all fibres is not an extra condition to carry across: over a path-connected base, one finite fibre forces the rest, which is TauCeti.hasFiniteFibers_of_finite_fiber. Mathlib proves that finite G-sets, in the form Action FintypeCat G, are a Galois category, and the axioms transport along an equivalence by TauCeti.preGaloisCategory_of_equivalence and TauCeti.fiberFunctor_comp_of_equivalence.

The resulting PreGaloisCategory and GaloisCategory instances are stated without reference to a basepoint, which is possible because both are propositions: the proof picks a point of the path-connected base and transports along the equivalence attached to it.

Main declarations

• TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor: the fibre over x₀ with its monodromy action, as a functor to finite π₁(X, x₀)-sets, with finiteFiberActionFunctor_obj_obj, finiteFiberActionFunctor_obj_obj_ρ_apply, finiteFiberActionFunctor_obj_obj_mulAction and finiteFiberActionFunctor_map_hom_hom computing it.
• TauCeti.FiniteCoveringSpace.finiteFiberActionEquivalence: finite covering spaces of X are equivalent to finite π₁(X, x₀)-sets.
• TauCeti.FiniteCoveringSpace.fiberActionFintypeCatEquivalence: the same equivalence, valued in Mathlib's Action FintypeCat.
• TauCeti.FiniteCoveringSpace.fiberFunctor: the fibre over x₀, as a functor to FintypeCat, with fiberFunctor_obj and fiberFunctor_map_hom computing it.
• TauCeti.FiniteCoveringSpace.instPreGaloisCategory and TauCeti.FiniteCoveringSpace.instGaloisCategory: the finite covering spaces of X form a Galois category.
• TauCeti.FiniteCoveringSpace.instFiberFunctor: the fibre over x₀ is a fibre functor.

References

This is the Galois-category lens named in Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md, which asks for the classification of covers to be phrased through Mathlib/CategoryTheory/Galois; see also SGA1, Exposé V, and Lenstra, Galois theory for schemes, Section 3. It consumes the π₁(X, x₀)-set classification of TauCeti.AlgebraicTopology.UniversalCover.Classification.FundamentalGroupAction.

noncomputable def TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor {X : TopCat} (x₀ : ↑X) : CategoryTheory.Functor (FiniteCoveringSpace X) (FiniteAction (FundamentalGroup (↑X) x₀))

The functor taking a finite covering space of X to the fibre over x₀, a finite set with the monodromy action of π₁(X, x₀).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_obj_obj {X : TopCat} (x₀ : ↑X) (p : FiniteCoveringSpace X) : ((finiteFiberActionFunctor x₀).obj p).obj = (CoveringSpace.fiberActionFunctor x₀).obj ((forget X).obj p)

theorem TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_obj_obj_V {X : TopCat} (x₀ : ↑X) (p : FiniteCoveringSpace X) : ((finiteFiberActionFunctor x₀).obj p).obj.V = ((CoveringSpace.fiberActionFunctor x₀).obj ((forget X).obj p)).V

The underlying type of the finite action attached to a finite cover is its fibre over the basepoint.

@[simp]

theorem TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_obj_obj_ρ_apply {X : TopCat} (x₀ : ↑X) (p : FiniteCoveringSpace X) (g : FundamentalGroup (↑X) x₀) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj p)) ⁻¹' {x₀})) : cast ⋯ ((CategoryTheory.ConcreteCategory.hom (((finiteFiberActionFunctor x₀).obj p).obj.ρ g)) (cast ⋯ e)) = ⋯.monodromy g e

A loop class acts on the fibre of a finite cover over x₀ by monodromy.

theorem TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_obj_obj_mulAction {X : TopCat} (x₀ : ↑X) (p : FiniteCoveringSpace X) : cast ⋯ ((finiteFiberActionFunctor x₀).obj p).obj.instMulAction = ⋯.fundamentalGroupMulAction x₀

The MulAction carried by the fibre of a finite cover over x₀ is Mathlib's monodromy action.

@[simp]

theorem TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_map_hom_hom {X : TopCat} (x₀ : ↑X) {p q : FiniteCoveringSpace X} (f : p ⟶ q) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj p)) ⁻¹' {x₀})) : cast ⋯ ((CategoryTheory.ConcreteCategory.hom ((finiteFiberActionFunctor x₀).map f).hom.hom) (cast ⋯ e)) = (CategoryTheory.ConcreteCategory.hom (TypeCat.ofHom (Function.fiberMap ⇑(TopCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) ⋯ x₀))) e

A map of finite covering spaces acts on the fibre over x₀ by restriction.

noncomputable def TauCeti.FiniteCoveringSpace.finiteFiberActionFunctorCompForgetIso {X : TopCat} (x₀ : ↑X) : (finiteFiberActionFunctor x₀).comp (FiniteAction.forget (FundamentalGroup (↑X) x₀)) ≅ (forget X).comp (CoveringSpace.fiberActionFunctor x₀)

The fibre-action functor of finite covers, followed by the inclusion of finite π₁(X, x₀)-sets into all of them, is the fibre-action functor of covers restricted to finite ones.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_faithful {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] : (finiteFiberActionFunctor x₀).Faithful

instance TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_full {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] : (finiteFiberActionFunctor x₀).Full

instance TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_essSurj {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : (finiteFiberActionFunctor x₀).EssSurj

Every finite π₁(X, x₀)-set is the fibre action of a finite covering space.

The cover realising it as a π₁(X, x₀)-set is one of the classification; its fibre over x₀ is finite because it is isomorphic to the given set, and then all of its fibres are finite because the base is path connected.

instance TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor_isEquivalence {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : (finiteFiberActionFunctor x₀).IsEquivalence

noncomputable def TauCeti.FiniteCoveringSpace.finiteFiberActionEquivalence {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : FiniteCoveringSpace X ≌ FiniteAction (FundamentalGroup (↑X) x₀)

Finite covering spaces of X are equivalent to finite π₁(X, x₀)-sets.

This is the restriction of TauCeti.CoveringSpace.fiberActionEquivalence to finite covers.

Equations

• TauCeti.FiniteCoveringSpace.finiteFiberActionEquivalence x₀ = (TauCeti.FiniteCoveringSpace.finiteFiberActionFunctor x₀).asEquivalence

@[simp]

theorem TauCeti.FiniteCoveringSpace.finiteFiberActionEquivalence_functor {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : (finiteFiberActionEquivalence x₀).functor = finiteFiberActionFunctor x₀

noncomputable def TauCeti.FiniteCoveringSpace.fiberActionFintypeCatEquivalence {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : FiniteCoveringSpace X ≌ Action FintypeCat (FundamentalGroup (↑X) x₀)

Finite covering spaces of X are equivalent to actions of π₁(X, x₀) on finite sets, in Mathlib's Action FintypeCat form.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteCoveringSpace.fiberActionFintypeCatEquivalence_functor {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : (fiberActionFintypeCatEquivalence x₀).functor = (finiteFiberActionFunctor x₀).comp (FiniteAction.toActionFintypeCat (FundamentalGroup (↑X) x₀))

noncomputable def TauCeti.FiniteCoveringSpace.fiberFunctor {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : CategoryTheory.Functor (FiniteCoveringSpace X) FintypeCat

The fibre of a finite covering space over x₀, as a functor to finite sets.

Equations

• TauCeti.FiniteCoveringSpace.fiberFunctor x₀ = (TauCeti.FiniteCoveringSpace.fiberActionFintypeCatEquivalence x₀).functor.comp (Action.forget FintypeCat (FundamentalGroup (↑X) x₀))

theorem TauCeti.FiniteCoveringSpace.fiberFunctor_eq {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : fiberFunctor x₀ = ((finiteFiberActionFunctor x₀).comp (FiniteAction.toActionFintypeCat (FundamentalGroup (↑X) x₀))).comp (Action.forget FintypeCat (FundamentalGroup (↑X) x₀))

@[simp]

theorem TauCeti.FiniteCoveringSpace.fiberFunctor_obj {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (p : FiniteCoveringSpace X) : ((fiberFunctor x₀).obj p).obj = ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj p)) ⁻¹' {x₀})

@[simp]

theorem TauCeti.FiniteCoveringSpace.fiberFunctor_map_hom {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] {p q : FiniteCoveringSpace X} (f : p ⟶ q) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj p)) ⁻¹' {x₀})) : cast ⋯ ((CategoryTheory.ConcreteCategory.hom ((fiberFunctor x₀).map f)) (cast ⋯ e)) = (CategoryTheory.ConcreteCategory.hom (TypeCat.ofHom (Function.fiberMap ⇑(TopCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) ⋯ x₀))) e

A map of finite covering spaces acts on the fibre over x₀ by restriction.

instance TauCeti.FiniteCoveringSpace.instPreGaloisCategory {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : CategoryTheory.PreGaloisCategory (FiniteCoveringSpace X)

The finite covering spaces of X satisfy the axioms (G1)–(G3) of a Galois category.

They are equivalent to the finite π₁(X, x₀)-sets, which Mathlib proves are a pre-Galois category. The statement does not mention a basepoint; the proof picks one.

instance TauCeti.FiniteCoveringSpace.instFiberFunctor {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : CategoryTheory.PreGaloisCategory.FiberFunctor (fiberFunctor x₀)

The fibre over x₀ is a fibre functor: it satisfies the axioms (G4)–(G6).

instance TauCeti.FiniteCoveringSpace.instGaloisCategory {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : CategoryTheory.GaloisCategory (FiniteCoveringSpace X)

The finite covering spaces of a path-connected, locally path-connected, semilocally simply connected space form a Galois category.