The fundamental group is the automorphism group of the fibre functor

Let X be path connected, locally path connected and semilocally simply connected, and fix a basepoint x₀. Sending a covering space of X to its fibre over x₀ is a functor

TauCeti.CoveringSpace.fiberFunctor x₀ : CoveringSpace X ⥤ Type u,

and this file identifies its automorphism group:

TauCeti.CoveringSpace.autFiberFunctorMulEquiv x₀ : FundamentalGroup X x₀ ≃* Aut (fiberFunctor x₀).

A loop class acts on each fibre by monodromy, and autFiberFunctorMulEquiv_hom_app_apply records that the automorphism attached to it is exactly that action.

This is the fibre-functor reading of the classification. The classification itself is already available as an equivalence of categories with π₁(X, x₀)-sets, and the fibre functor is that equivalence followed by the forgetful functor to types, so the identification is Tannaka duality for G-sets, TauCeti.autCompForgetActionMulEquiv.

The statement is about all covering spaces of X, not just the finite ones, and this is what makes it clean. On the finite covers TauCeti.FiniteCoveringSpace.fiberFunctor is a fibre functor for a Galois category, and Mathlib's recognition interface there, CategoryTheory.PreGaloisCategory.IsFundamentalGroup, asks for a compact topological group, which a discrete π₁(X, x₀) is only when it is finite. Keeping all covers removes that restriction.

Main declarations

• TauCeti.CoveringSpace.fiberFunctor: the fibre over x₀, as a functor to types, with fiberFunctor_obj and fiberFunctor_map computing it.
• TauCeti.CoveringSpace.autFiberFunctorMulEquiv: the fundamental group of X at x₀ is the automorphism group of the fibre functor over x₀, with autFiberFunctorMulEquiv_hom_app_apply computing the automorphism attached to a loop class.
• TauCeti.CoveringSpace.endFiberFunctorMulEquiv: the same for natural endomorphisms of the fibre functor, which are therefore all invertible.
• TauCeti.CoveringSpace.existsUnique_monodromy_eq: every natural automorphism of the fibre functor is monodromy along a unique loop class.
• TauCeti.CoveringSpace.forall_monodromy_eq_self_iff_eq_one: a loop class acting trivially on every fibre is trivial.

References

• Hatcher, Algebraic Topology, Section 1.3, for the monodromy description of covers.
• Lenstra, Galois theory for schemes, Section 3, for the automorphism group of a fibre functor.

noncomputable def TauCeti.CoveringSpace.fiberFunctor {X : TopCat} (x₀ : ↑X) : CategoryTheory.Functor (CoveringSpace X) (Type u)

The functor taking a covering space of X to its fibre over x₀.

It is the fibre-action functor followed by the forgetful functor from π₁(X, x₀)-sets to types, and is @[expose]d so that the concrete fibre types in its public value lemmas are definitionally equal to the functor's values.

Equations

• TauCeti.CoveringSpace.fiberFunctor x₀ = (TauCeti.CoveringSpace.fiberActionFunctor x₀).comp (Action.forget (Type ?u.1) (FundamentalGroup (↑X) x₀))

@[simp]

theorem TauCeti.CoveringSpace.fiberFunctor_obj {X : TopCat} (x₀ : ↑X) (p : CoveringSpace X) : (fiberFunctor x₀).obj p = ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})

@[simp]

theorem TauCeti.CoveringSpace.fiberFunctor_map {X : TopCat} (x₀ : ↑X) {p q : CoveringSpace X} (f : p ⟶ q) : (fiberFunctor x₀).map f = TypeCat.ofHom (Function.fiberMap ⇑(TopCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) ⋯ x₀)

A map of covering spaces acts on the fibre over the basepoint by restriction.

noncomputable def TauCeti.CoveringSpace.endFiberFunctorMulEquiv {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : FundamentalGroup (↑X) x₀ ≃* CategoryTheory.End (fiberFunctor x₀)

The fundamental group of X at x₀ is the monoid of natural endomorphisms of the fibre functor over x₀. Since the fundamental group is a group, so is this endomorphism monoid: every natural endomorphism of the fibre functor is invertible.

Equations

• TauCeti.CoveringSpace.endFiberFunctorMulEquiv x₀ = TauCeti.endCompForgetActionMulEquiv (FundamentalGroup (↑X) x₀) (TauCeti.CoveringSpace.fiberActionFunctor x₀)

@[simp]

theorem TauCeti.CoveringSpace.endFiberFunctorMulEquiv_app_apply {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : FundamentalGroup (↑X) x₀) (p : CoveringSpace X) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})) : (CategoryTheory.ConcreteCategory.hom (((endFiberFunctorMulEquiv x₀) g).app p)) e = ⋯.monodromy g e

The natural endomorphism of the fibre functor attached to a loop class acts on each fibre by monodromy along that loop.

noncomputable def TauCeti.CoveringSpace.autFiberFunctorMulEquiv {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] : FundamentalGroup (↑X) x₀ ≃* CategoryTheory.Aut (fiberFunctor x₀)

The fundamental group of X at x₀ is the automorphism group of the fibre functor over x₀.

A loop class is sent to the natural automorphism acting on every fibre by monodromy; that this is a bijection onto all natural automorphisms is Tannaka duality for π₁(X, x₀)-sets, transported along the classification of covering spaces by π₁(X, x₀)-sets.

Equations

• TauCeti.CoveringSpace.autFiberFunctorMulEquiv x₀ = TauCeti.autCompForgetActionMulEquiv (FundamentalGroup (↑X) x₀) (TauCeti.CoveringSpace.fiberActionFunctor x₀)

@[simp]

theorem TauCeti.CoveringSpace.autFiberFunctorMulEquiv_hom_app_apply {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : FundamentalGroup (↑X) x₀) (p : CoveringSpace X) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})) : (CategoryTheory.ConcreteCategory.hom (((autFiberFunctorMulEquiv x₀) g).hom.app p)) e = ⋯.monodromy g e

The automorphism of the fibre functor attached to a loop class acts on each fibre by monodromy along that loop.

@[simp]

theorem TauCeti.CoveringSpace.autFiberFunctorMulEquiv_inv_app_apply {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : FundamentalGroup (↑X) x₀) (p : CoveringSpace X) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})) : (CategoryTheory.ConcreteCategory.hom (((autFiberFunctorMulEquiv x₀) g).inv.app p)) e = ⋯.monodromy g⁻¹ e

The inverse of the automorphism attached to a loop class is monodromy along the inverse loop class.

theorem TauCeti.CoveringSpace.existsUnique_monodromy_eq {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (η : CategoryTheory.Aut (fiberFunctor x₀)) : ∃! g : FundamentalGroup (↑X) x₀, ∀ (p : CoveringSpace X) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})), ⋯.monodromy g e = (CategoryTheory.ConcreteCategory.hom (η.hom.app p)) e

Every natural automorphism of the fibre functor is monodromy along a unique loop class.

theorem TauCeti.CoveringSpace.forall_monodromy_eq_self_iff_eq_one {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : FundamentalGroup (↑X) x₀) : (∀ (p : CoveringSpace X) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom p.proj) ⁻¹' {x₀})), ⋯.monodromy g e = e) ↔ g = 1

A loop class acting trivially by monodromy on the fibre of every covering space of X is trivial. This is the faithfulness condition that CategoryTheory.PreGaloisCategory.IsFundamentalGroup calls non_trivial'.