The fundamental group of the base of a regular cover and its deck group

For a covering map p : E → X with simply connected total space whose deck action is regular (p surjective, with deck p acting transitively on every fibre), the fundamental group of the base is anti-isomorphic to the deck transformation group:

FundamentalGroup X x ≃* (deck p)ᵐᵒᵖ.

The theorem is stated for an arbitrary regular cover with simply connected total space rather than only for the universal cover UniversalCover.proj x₀.

The ᵐᵒᵖ is genuine. The deck group acts on the total space on the left (deck.smul_eq_apply : φ • e = φ.1 e), while the monodromy of π₁(X, x) acts on each fibre on the right (monodromy (γ.trans γ') = monodromy γ' ∘ monodromy γ); choosing a basepoint lift e in the fibre and matching the deck element that realises a monodromy therefore reverses multiplication, so the natural isomorphism lands in (deck p)ᵐᵒᵖ.

The isomorphism is Mathlib's IsQuotientCoveringMap.fundamentalGroupEquiv, instantiated at the group deck p through Deck.IsRegular.isQuotientCoveringMap: a regular preconnected covering exhibits its base as the quotient of the total space by deck p, and for a simply connected total space Mathlib's quotient-covering machinery identifies the deck group with π₁ of the base. As a corollary, choosing a basepoint lift e in the fibre over x identifies π₁(X, x) with that fibre via monodromy.

Main declarations

• TauCeti.Deck.IsRegular.fundamentalGroupEquiv: the anti-isomorphism FundamentalGroup X x ≃* (deck p)ᵐᵒᵖ.
• TauCeti.Deck.IsRegular.fundamentalGroupEquiv_unop_apply: the deck element attached to γ moves the chosen lift e to monodromy γ e.
• TauCeti.Deck.IsRegular.fundamentalGroupEquiv_apply_eq_iff: characterizes equality with an arbitrary deck transformation by its value at the chosen lift.
• TauCeti.Deck.IsRegular.fundamentalGroupEquiv_symm_monodromy: characterizes the inverse equivalence by the monodromy translate of the chosen lift.
• TauCeti.Deck.IsRegular.fundamentalGroupEquiv_eq_one_iff: γ maps to the identity exactly when its monodromy fixes e.
• TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv: when the deck group is commutative, the opposite drops out and the fundamental group of the base is the deck group itself.

References

The comparison map is Mathlib's IsQuotientCoveringMap.fundamentalGroupEquiv (Junyan Xu, Mathlib/Topology/Homotopy/Lifting.lean); the quotient-covering presentation of a regular deck action is TauCeti.Deck.IsRegular.isQuotientCoveringMap.

noncomputable def TauCeti.Deck.IsRegular.fundamentalGroupEquiv {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : FundamentalGroup X x ≃* (↥(deck p))ᵐᵒᵖ

For a regular covering map p : E → X with simply connected total space, the fundamental group of the base is anti-isomorphic to the deck transformation group: FundamentalGroup X x ≃* (deck p)ᵐᵒᵖ. The ᵐᵒᵖ reflects that the deck group acts on the left while the monodromy of π₁ acts on the right; see the module docstring.

Equations

• hreg.fundamentalGroupEquiv hp e = ⋯.fundamentalGroupEquiv e

@[simp]

theorem TauCeti.Deck.IsRegular.fundamentalGroupEquiv_unop_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : ↑(MulOpposite.unop ((hreg.fundamentalGroupEquiv hp e) γ)) ↑e = ↑(hp.monodromy γ e)

The deck transformation attached to a loop class γ moves the chosen basepoint lift e along the monodromy of γ.

theorem TauCeti.Deck.IsRegular.fundamentalGroupEquiv_unop_smul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : MulOpposite.unop ((hreg.fundamentalGroupEquiv hp e) γ) • ↑e = ↑(hp.monodromy γ e)

Compatibility spelling of fundamentalGroupEquiv_unop_apply using the deck action.

theorem TauCeti.Deck.IsRegular.fundamentalGroupEquiv_apply_eq_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) (g : (↥(deck p))ᵐᵒᵖ) : (hreg.fundamentalGroupEquiv hp e) γ = g ↔ MulOpposite.unop g • ↑e = ↑(hp.monodromy γ e)

The fundamental group element γ corresponds to a deck transformation g exactly when g.unop moves the chosen lift e to the monodromy translate of e along γ.

theorem TauCeti.Deck.IsRegular.fundamentalGroupEquiv_symm_monodromy {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (g : (↥(deck p))ᵐᵒᵖ) : ↑(hp.monodromy ((hreg.fundamentalGroupEquiv hp e).symm g) e) = MulOpposite.unop g • ↑e

The fundamental group element corresponding to an opposite deck transformation is the unique loop class whose monodromy moves the chosen lift e by that deck transformation.

theorem TauCeti.Deck.IsRegular.fundamentalGroupEquiv_symm_op_monodromy {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (φ : ↥(deck p)) : ↑(hp.monodromy ((hreg.fundamentalGroupEquiv hp e).symm (MulOpposite.op φ)) e) = φ • ↑e

A deck p spelling of fundamentalGroupEquiv_symm_monodromy. The loop class corresponding to MulOpposite.op φ has monodromy action equal to φ at the chosen lift.

theorem TauCeti.Deck.IsRegular.fundamentalGroupEquiv_eq_one_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : (hreg.fundamentalGroupEquiv hp e) γ = 1 ↔ hp.monodromy γ e = e

A loop class γ maps to the identity deck transformation exactly when its monodromy fixes the chosen basepoint lift e.

noncomputable def TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (hcomm : ∀ (a b : ↥(deck p)), a * b = b * a) : FundamentalGroup X x ≃* ↥(deck p)

When the deck group of a regular covering map with simply connected total space is commutative, the fundamental group of the base is the deck group itself: the opposite in IsRegular.fundamentalGroupEquiv disappears because multiplication in the deck group commutes. This is the form in which the comparison computes fundamental groups from deck groups, e.g. π₁(S¹) ≅ ℤ (AddCircle.fundamentalGroupMulEquiv) and π₁(RPⁿ) ≅ ℤˣ (TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv).

Equations

• hreg.fundamentalGroupDeckEquiv hp e hcomm = (hreg.fundamentalGroupEquiv hp e).trans (TauCeti.MulOpposite.unopMulEquivOfComm hcomm)

@[simp]

theorem TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (hcomm : ∀ (a b : ↥(deck p)), a * b = b * a) (γ : FundamentalGroup X x) : (hreg.fundamentalGroupDeckEquiv hp e hcomm) γ = MulOpposite.unop ((hreg.fundamentalGroupEquiv hp e) γ)

The deck transformation assigned to a loop class γ, in the commutative-deck-group form of the comparison: it is the unopposite of IsRegular.fundamentalGroupEquiv γ.

theorem TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv_apply_eq_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (hcomm : ∀ (a b : ↥(deck p)), a * b = b * a) (γ : FundamentalGroup X x) (d : ↥(deck p)) : (hreg.fundamentalGroupDeckEquiv hp e hcomm) γ = d ↔ d • ↑e = ↑(hp.monodromy γ e)

A loop class corresponds to the deck transformation d, in the commutative-deck-group form of the comparison, exactly when d moves the chosen lift e to the monodromy translate of e along γ.

theorem TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv_symm_monodromy {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (hcomm : ∀ (a b : ↥(deck p)), a * b = b * a) (d : ↥(deck p)) : ↑(hp.monodromy ((hreg.fundamentalGroupDeckEquiv hp e hcomm).symm d) e) = d • ↑e

The inverse equivalence sends a deck transformation to the unique loop class whose monodromy moves the chosen lift by that transformation.

theorem TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv_eq_one_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (hcomm : ∀ (a b : ↥(deck p)), a * b = b * a) (γ : FundamentalGroup X x) : (hreg.fundamentalGroupDeckEquiv hp e hcomm) γ = 1 ↔ hp.monodromy γ e = e

A loop class maps to the identity deck transformation exactly when its monodromy fixes the chosen basepoint lift e.