Reconstructing a connected cover from a fundamental-group action

Let A be a π₁(X, x₀)-set and choose a : A. The stabilizer of a is a subgroup of the fundamental group, so the universal-cover quotient by that stabilizer is a connected covering space of X. Its fibre over x₀ is equivariantly equivalent to the orbit of a, hence to A itself when the action is transitive.

This is the object-level reconstruction in the classification of connected covers by transitive fundamental-group actions. The construction deliberately reuses the cover attached to a subgroup and orbit-stabilizer: no second topology on a reconstructed total space is introduced. A later step can extend the equivariant equivalence on the base fibre to a natural isomorphism of fundamental-groupoid actions and assemble the categorical equivalence.

Main declarations

• TauCeti.UniversalCover.stabilizerCover: the connected covering space obtained by quotienting the universal cover by the stabilizer of a point in a fundamental-group action.
• TauCeti.UniversalCover.stabilizerCoverBasepointFiber: the distinguished point of its fibre over x₀.
• TauCeti.UniversalCover.stabilizerCoverFiberEquivOrbit: the fibre of that cover over x₀ is equivalent to the orbit of a, and TauCeti.UniversalCover.stabilizerCoverFiberEquivOrbit_apply_monodromy shows this equivalence intertwines covering-space monodromy with the given fundamental-group action.
• TauCeti.UniversalCover.transitiveActionFiberEquiv and TauCeti.UniversalCover.transitiveActionFiberEquiv_apply_monodromy: for a transitive action the same fibre is equivariantly equivalent to the whole π₁(X, x₀)-set.

References

This is the reconstruction step in the alternative transitive-action formulation of Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md. It is the standard stabilizer construction for the equivalence between connected covering spaces and transitive fundamental-group sets; see Hatcher, Algebraic Topology, Section 1.3. The proof uses Mathlib's orbit-stabilizer equivalence and Tau Ceti's universal-cover quotient associated to a subgroup.

noncomputable def TauCeti.UniversalCover.stabilizerCover {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (a : A) : ConnectedCoveringSpace ↧X

The connected covering space attached to a point a of a π₁(X, x₀)-set: it is the universal cover modulo the stabilizer of a.

Its fibre over x₀ is the orbit of a, so for a transitive action it is the cover reconstructed from the action.

Equations

• TauCeti.UniversalCover.stabilizerCover x0 a = TauCeti.UniversalCover.subgroupCover x0 (MulAction.stabilizer (FundamentalGroup X x0) a)

theorem TauCeti.UniversalCover.stabilizerCover_def {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (a : A) : stabilizerCover x0 a = subgroupCover x0 (MulAction.stabilizer (FundamentalGroup X x0) a)

The stabilizer cover is the subgroup cover associated to the stabilizer of a.

noncomputable def TauCeti.UniversalCover.stabilizerCoverBasepointFiber {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (a : A) : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (stabilizerCover x0 a))) ⁻¹' {x0})

The distinguished point of the fibre over x₀ of the cover reconstructed from a: the class of the constant path at the basepoint.

Equations

• TauCeti.UniversalCover.stabilizerCoverBasepointFiber x0 a = TauCeti.UniversalCover.subgroupCoverBasepointFiber x0 (MulAction.stabilizer (FundamentalGroup X x0) a)

The fibre as an orbit

The equivalence and its equivariance are first proved for the underlying quotient projection, which carries the instances the orbit-stabilizer API needs, and are then transported to the bundled cover along subgroupCoverFiberEquivSubgroupQuotient.

noncomputable def TauCeti.UniversalCover.stabilizerCoverFiberEquivOrbit {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (a : A) : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (stabilizerCover x0 a))) ⁻¹' {x0}) ≃ ↑(MulAction.orbit (FundamentalGroup X x0) a)

The fibre over x₀ of the cover reconstructed from a is equivalent to the orbit of a.

Under this equivalence the distinguished point of the fibre corresponds to a, by stabilizerCoverFiberEquivOrbit_apply_basepoint; the equivariance statement is stabilizerCoverFiberEquivOrbit_apply_monodromy.

Equations

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

@[simp]

theorem TauCeti.UniversalCover.stabilizerCoverFiberEquivOrbit_apply_basepoint {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (a : A) : (stabilizerCoverFiberEquivOrbit x0 a) (stabilizerCoverBasepointFiber x0 a) = ⟨a, ⋯⟩

The fibre equivalence sends the distinguished point of the fibre to a.

@[simp]

theorem TauCeti.UniversalCover.stabilizerCoverFiberEquivOrbit_apply_monodromy {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (a : A) (g : FundamentalGroup X x0) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (stabilizerCover x0 a))) ⁻¹' {x0})) : (stabilizerCoverFiberEquivOrbit x0 a) (⋯.monodromy g e) = g • (stabilizerCoverFiberEquivOrbit x0 a) e

The fibre equivalence is equivariant: monodromy of the reconstructed cover agrees with the given action of the fundamental group on the orbit of a.

Transitive actions

noncomputable def TauCeti.UniversalCover.transitiveActionFiberEquiv {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] [MulAction.IsPretransitive (FundamentalGroup X x0) A] (a : A) : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (stabilizerCover x0 a))) ⁻¹' {x0}) ≃ A

For a transitive action, the fibre over x₀ of the cover reconstructed from a is equivalent to the whole π₁(X, x₀)-set, the orbit of a being everything.

Under this equivalence the distinguished point of the fibre corresponds to a, by transitiveActionFiberEquiv_apply_basepoint.

Equations

• TauCeti.UniversalCover.transitiveActionFiberEquiv x0 a = (TauCeti.UniversalCover.stabilizerCoverFiberEquivOrbit x0 a).trans (Equiv.subtypeUnivEquiv ⋯)

@[simp]

theorem TauCeti.UniversalCover.transitiveActionFiberEquiv_apply_basepoint {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] [MulAction.IsPretransitive (FundamentalGroup X x0) A] (a : A) : (transitiveActionFiberEquiv x0 a) (stabilizerCoverBasepointFiber x0 a) = a

The fibre equivalence of a transitive action sends the distinguished point of the fibre to a.

@[simp]

theorem TauCeti.UniversalCover.transitiveActionFiberEquiv_apply_monodromy {X : Type u} [TopologicalSpace X] (x0 : X) {A : Type v} [MulAction (FundamentalGroup X x0) A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] [MulAction.IsPretransitive (FundamentalGroup X x0) A] (a : A) (g : FundamentalGroup X x0) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (stabilizerCover x0 a))) ⁻¹' {x0})) : (transitiveActionFiberEquiv x0 a) (⋯.monodromy g e) = g • (transitiveActionFiberEquiv x0 a) e

The fibre equivalence of a transitive action is equivariant: monodromy of the reconstructed cover agrees with the given action of the fundamental group on A.