Documentation

TauCeti.AlgebraicTopology.UniversalCover.Classification.ProfiniteFiberFunctor

The profinite fundamental group of the finite-cover fibre functor #

Let X be path connected, locally path connected and semilocally simply connected, and fix a basepoint x₀. Finite covering spaces of X form a Galois category with fibre functor TauCeti.FiniteCoveringSpace.fiberFunctor x₀. Its fundamental group is the profinite completion of π₁(X, x₀).

The result transports the corresponding statement for finite π₁(X, x₀)-sets along TauCeti.FiniteCoveringSpace.fiberActionFintypeCatEquivalence. Thus the action on a finite cover's fibre is the unique continuous extension of monodromy from the ordinary fundamental group. Mathlib's Galois-category recognition theorem then identifies this profinite completion with the natural automorphism group of the fibre functor, as both a group and a topological space.

Main declarations #

The profinite-completion action is constructed in TauCeti.CategoryTheory.Action.ProfiniteCompletion from Mathlib's universal property.

source
@[instance_reducible]
noncomputable instance TauCeti.FiniteCoveringSpace.instProfiniteCompletionMulAction {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (p : FiniteCoveringSpace X) :
MulAction (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop) ((fiberFunctor x₀).obj p).obj

The profinite completion of π₁(X, x₀) acts on the fibre of every finite covering space. This is the continuous extension of the monodromy action.

Equations
  • One or more equations did not get rendered due to their size.
source
instance TauCeti.FiniteCoveringSpace.instProfiniteCompletionIsFundamentalGroup {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
CategoryTheory.PreGaloisCategory.IsFundamentalGroup (fiberFunctor x₀) ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop

The profinite completion of π₁(X, x₀) is a fundamental group of the finite-cover fibre functor.

source
@[simp]
theorem TauCeti.FiniteCoveringSpace.profiniteCompletion_etaFn_smul {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : FundamentalGroup (↑X) x₀) (p : FiniteCoveringSpace X) (e : ((fiberFunctor x₀).obj p).obj) :
ProfiniteGrp.ProfiniteCompletion.etaFn (↧(FundamentalGroup (↑X) x₀)) g • e = (CategoryTheory.ConcreteCategory.hom (((fiberActionFintypeCatEquivalence x₀).functor.obj p).ρ g)) e

The profinite-completion action restricts along the canonical map from π₁(X, x₀) to the classified finite action. Through finiteFiberActionFunctor_obj_obj_ρ_apply, the right-hand side is monodromy on the fibre of p.

source
noncomputable def TauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop ≃* CategoryTheory.Aut (fiberFunctor x₀)

The profinite completion of π₁(X, x₀) is the automorphism group of the finite-cover fibre functor.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv_hom_app_apply {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop) (p : FiniteCoveringSpace X) (e : ((fiberFunctor x₀).obj p).obj) :
    (CategoryTheory.ConcreteCategory.hom (((profiniteCompletionAutFiberFunctorMulEquiv x₀) g).hom.app p)) e = g • e

    The automorphism attached to an element of the profinite completion acts on every finite fibre by the canonical extended action.

    source
    @[simp]
    theorem TauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv_inv_app_apply {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop) (p : FiniteCoveringSpace X) (e : ((fiberFunctor x₀).obj p).obj) :
    (CategoryTheory.ConcreteCategory.hom (((profiniteCompletionAutFiberFunctorMulEquiv x₀) g).inv.app p)) e = g⁻¹ • e

    The inverse of the automorphism attached to an element of the profinite completion acts by the inverse element on every finite fibre.

    source
    theorem TauCeti.FiniteCoveringSpace.existsUnique_profiniteCompletion_smul_eq {X : TopCat} {x₀ : ↑X} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (η : CategoryTheory.Aut (fiberFunctor x₀)) :
    ∃! g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop, ∀ (p : FiniteCoveringSpace X) (e : ((fiberFunctor x₀).obj p).obj), g • e = (CategoryTheory.ConcreteCategory.hom (η.hom.app p)) e

    Every natural automorphism of the finite-cover fibre functor is induced on every fibre by a unique element of the profinite completion of π₁(X, x₀).

    source
    theorem TauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv_isHomeomorph {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
    IsHomeomorph ⇑(profiniteCompletionAutFiberFunctorMulEquiv x₀)

    The equivalence between the profinite completion and fibre-functor automorphisms is a homeomorphism for their canonical topologies.