Deck transformations as the opposite fundamental group

For a regular covering map p : E → X with simply connected total space, the existing comparison

Deck.IsRegular.fundamentalGroupEquiv : FundamentalGroup X x ≃* (deck p)ᵐᵒᵖ

pins the convention: monodromy acts on the right, whereas deck transformations act on the left. This file packages the equivalent deck-to-fundamental-group form

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

and records its pointwise characterizations, for cover-classification arguments that pass between deck transformations, loop classes, and fibre points.

Main declarations

• TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv: the deck group is isomorphic to the opposite fundamental group.
• TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_unop_monodromy: the loop class attached to a deck transformation has monodromy equal to that deck transformation on the chosen lift.
• TauCeti.Deck.IsRegular.deckEquivFiber_eq_fundamentalGroupEquivFiber: the deck-to-fibre equivalence and monodromy-to-fibre equivalence agree under this comparison.

References

This is a formal consequence of TauCeti.Deck.IsRegular.fundamentalGroupEquiv, which in turn uses Junyan Xu's IsQuotientCoveringMap.fundamentalGroupEquiv from Mathlib.Topology.Homotopy.Lifting.

noncomputable def TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv {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) ≃* (FundamentalGroup X x)ᵐᵒᵖ

For a regular covering map p : E → X with simply connected total space, the deck group is isomorphic to the opposite of the fundamental group of the base: deck p ≃* (FundamentalGroup X x)ᵐᵒᵖ.

The opposite is the same convention as in fundamentalGroupEquiv: deck transformations act on the left, while fundamental-group monodromy acts on the right.

Equations

• hreg.deckFundamentalGroupEquiv hp e = (MulEquiv.opOp ↥(deck p)).trans (MulEquiv.op (hreg.fundamentalGroupEquiv hp e).symm)

@[simp]

theorem TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_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})) (φ : ↥(deck p)) : (hreg.deckFundamentalGroupEquiv hp e) φ = MulOpposite.op ((hreg.fundamentalGroupEquiv hp e).symm (MulOpposite.op φ))

The deck-to-fundamental-group equivalence sends a deck transformation to the opposite of the loop class corresponding to the opposite deck transformation under fundamentalGroupEquiv.

@[simp]

theorem TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_symm_op {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.deckFundamentalGroupEquiv hp e).symm (MulOpposite.op γ) = MulOpposite.unop ((hreg.fundamentalGroupEquiv hp e) γ)

The inverse deck-to-fundamental-group equivalence sends op γ to the deck transformation corresponding to γ under fundamentalGroupEquiv.

theorem TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_unop_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 (MulOpposite.unop ((hreg.deckFundamentalGroupEquiv hp e) φ)) e) = φ • ↑e

The loop class attached to a deck transformation has monodromy equal to that deck transformation on the chosen lift.

theorem TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_apply_eq_op_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})) (φ : ↥(deck p)) (γ : FundamentalGroup X x) : (hreg.deckFundamentalGroupEquiv hp e) φ = MulOpposite.op γ ↔ ↑(hp.monodromy γ e) = φ • ↑e

A deck transformation corresponds to a loop class exactly when that loop class's monodromy moves the chosen lift by the deck transformation.

theorem TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_symm_op_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) (φ : ↥(deck p)) : (hreg.deckFundamentalGroupEquiv hp e).symm (MulOpposite.op γ) = φ ↔ ↑(hp.monodromy γ e) = φ • ↑e

The inverse comparison is characterized by the same monodromy formula.

theorem TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv_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})) (φ : ↥(deck p)) : (hreg.deckFundamentalGroupEquiv hp e) φ = 1 ↔ φ • ↑e = ↑e

A deck transformation maps to the identity loop class exactly when it fixes the chosen lift.

theorem TauCeti.Deck.IsRegular.deckEquivFiber_eq_fundamentalGroupEquivFiber {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)) : (deckEquivFiber hp hreg e) φ = (hp.fundamentalGroupEquivFiber e) (MulOpposite.unop ((hreg.deckFundamentalGroupEquiv hp e) φ))

Under the deck-to-fundamental-group comparison, the deck-to-fibre equivalence for a regular cover agrees with the monodromy equivalence from π₁ to the same fibre.