Documentation

TauCeti.AlgebraicTopology.UniversalCover.Classification.ActionCover

The covering space attached to a fundamental-group set #

Let X be path connected, locally path connected and semilocally simply connected, and let A be a set with an action of π₁(X, x₀). The universal cover UniversalCover x₀ is the total space of a quotient covering map for π₁(X, x₀), so the balanced product

ActionCover x₀ A = UniversalCover x₀ ×_{π₁(X, x₀)} A

is a covering space of X by TauCeti.BalancedProduct.isCoveringMap_proj, and its fibre over x₀ is A.

The action is arbitrary: it is neither assumed transitive nor nonempty, so the resulting cover is in general disconnected. That is the point. The transitive case is already available as the quotient of the universal cover by a stabiliser (TauCeti.UniversalCover.stabilizerCover), and a connected cover is exactly what such a quotient produces; a general action needs the disjoint union of one such quotient per orbit, which is what the balanced product provides in one step.

The fibre identification is equivariant. The map e ↦ ⟦(e, a)⟧ from the universal cover is a map of covering spaces over X, and monodromy is functorial in such maps, so monodromy on the fibre of ActionCover x₀ A is computed by monodromy on the fibre of the universal cover, which is the fundamental-group action by TauCeti.UniversalCover.monodromy_basepointLift. Because that action prepends the inverse loop class, the inverse cancels against the exchange ⟦(g • e, a)⟧ = ⟦(e, g⁻¹ • a)⟧ and no ᵐᵒᵖ appears here.

Main declarations #

References #

This is the object half of the essential surjectivity of monodromy on all covering spaces, the disconnected case of TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 8, which asks for covers to be classified by functors out of the fundamental groupoid. It consumes the based-path universal cover adapted from Kim Morrison's mathlib4#38292 and Mathlib's quotient-covering-map interface due to Junyan Xu.

source
@[reducible, inline]
abbrev TauCeti.UniversalCover.ActionCover {X : Type u} [TopologicalSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] :
Type u

The total space of the covering space attached to a π₁(X, x₀)-set A: the balanced product of the universal cover with A.

Equations
Instances For
    source
    noncomputable def TauCeti.UniversalCover.actionCoverProj {X : Type u} [TopologicalSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] :
    ActionCover x₀ A → X

    The projection of the cover attached to A down to the base.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.UniversalCover.actionCoverProj_mk {X : Type u} [TopologicalSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] (e : UniversalCover x₀) (a : A) :
      actionCoverProj x₀ A (BalancedProduct.mk (FundamentalGroup X x₀) e a) = e.proj
      source
      theorem TauCeti.UniversalCover.continuous_actionCoverProj {X : Type u} [TopologicalSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] :
      Continuous (actionCoverProj x₀ A)
      source
      theorem TauCeti.UniversalCover.isCoveringMap_actionCoverProj {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] :
      IsCoveringMap (actionCoverProj x₀ A)

      The cover attached to a π₁(X, x₀)-set is a covering space of X.

      source
      noncomputable def TauCeti.UniversalCover.actionCoveringSpace {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] :
      CoveringSpace ↧X

      The cover attached to a π₁(X, x₀)-set, bundled as a covering space over X.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.UniversalCover.actionCoveringSpace_coe {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] :
        (actionCoveringSpace x₀ A).obj.left = ↧(ActionCover x₀ A)

        The total space of the bundled cover attached to A is ActionCover x₀ A.

        source
        theorem TauCeti.UniversalCover.actionCoveringSpace_proj {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] :
        (actionCoveringSpace x₀ A).proj = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (TopCat.ofHom { toFun := actionCoverProj x₀ A, continuous_toFun := ⋯ })

        The projection of the bundled cover attached to A is actionCoverProj.

        source
        noncomputable def TauCeti.UniversalCover.actionCoverFiberEquiv {X : Type u} [TopologicalSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] :
        A ≃ ↑(actionCoverProj x₀ A ⁻¹' {x₀})

        The fibre of the cover attached to A over x₀ is A. A point of A labels the class of the pair it forms with the constant-path point of the universal cover.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.UniversalCover.actionCoverFiberEquiv_apply_coe {X : Type u} [TopologicalSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] (a : A) :
          ↑((actionCoverFiberEquiv x₀ A) a) = BalancedProduct.mk (FundamentalGroup X x₀) (↑(basepointLift x₀)) a
          source
          @[simp]
          theorem TauCeti.UniversalCover.monodromy_actionCoverFiberEquiv {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] (g : FundamentalGroup X x₀) (a : A) :
          ⋯.monodromy g ((actionCoverFiberEquiv x₀ A) a) = (actionCoverFiberEquiv x₀ A) (g • a)

          The fibre identification is equivariant: the monodromy of a loop class on the fibre of the cover attached to A is the action of that loop class on A.

          source
          noncomputable def TauCeti.UniversalCover.actionCoveringSpaceFiberEquiv {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] :
          ↑(⇑(CategoryTheory.ConcreteCategory.hom (actionCoveringSpace x₀ A).proj) ⁻¹' {x₀}) ≃ A

          The fibre of the bundled cover attached to A over x₀ is A.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.UniversalCover.actionCoveringSpaceFiberEquiv_apply_monodromy {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (A : Type u) [MulAction (FundamentalGroup X x₀) A] [TopologicalSpace A] [DiscreteTopology A] (g : FundamentalGroup X x₀) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (actionCoveringSpace x₀ A).proj) ⁻¹' {x₀})) :
            (actionCoveringSpaceFiberEquiv x₀ A) (⋯.monodromy g e) = g • (actionCoveringSpaceFiberEquiv x₀ A) e

            The bundled fibre identification is equivariant: monodromy on the fibre of the cover attached to A agrees with the given action of the fundamental group on A.