The deck transformation group of the quotient map 𝕜 → AddCircle p

For a topological additive commutative group 𝕜, this file computes the deck transformations of the quotient map 𝕜 → AddCircle p. Since AddCircle p = 𝕜 ⧸ zmultiples p, it gives

deck ((↑) : 𝕜 → AddCircle p) ≃* Multiplicative (zmultiples p).

The forward inclusion is elementary. For the converse, a deck transformation φ keeps φ e - e inside the totally disconnected subgroup while varying continuously in e, so on a preconnected 𝕜 it is constant; that constant is φ 0, and φ is translation by it.

When the period subgroup is totally disconnected and p is not a torsion element (¬ IsOfFinAddOrder p), the translation subgroup is infinite cyclic, giving deck ((↑) : 𝕜 → AddCircle p) ≃* Multiplicative ℤ. In the standard real case, where AddCircle.isCoveringMap_coe supplies the covering hypothesis, this is the deck group of the universal cover ℝ → S¹, the algebraic input to the computation π₁(S¹) ≅ ℤ.

Main declarations

• TauCeti.Deck.addRightZMultiples: translation by an element of zmultiples p as a deck transformation of (↑) : 𝕜 → AddCircle p.
• TauCeti.Deck.isRegular_addCircleCoe: the projection (↑) : 𝕜 → AddCircle p has regular deck action.
• TauCeti.Deck.addCircleMulEquiv: the deck group of (↑) : 𝕜 → AddCircle p is Multiplicative (zmultiples p).
• TauCeti.Deck.addCircleMulEquivInt: for a totally disconnected period subgroup and a non-torsion period, the deck group is Multiplicative ℤ.

References

This consumes Mathlib's covering map AddCircle.isCoveringMap_coe and Mathlib's deck transformation group deck.

theorem TauCeti.Deck.mem_addCircleCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] {p : 𝕜} {φ : 𝕜 ≃ₜ 𝕜} : φ ∈ deck QuotientAddGroup.mk ↔ ∀ (e : 𝕜), φ e - e ∈ AddSubgroup.zmultiples p

A homeomorphism of 𝕜 is a deck transformation of (↑) : 𝕜 → AddCircle p exactly when it moves every point within the period subgroup zmultiples p.

def TauCeti.Deck.addRightZMultiples {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} (a : ↥(AddSubgroup.zmultiples p)) : ↥(deck QuotientAddGroup.mk)

Right translation by an element of zmultiples p, as a deck transformation of (↑) : 𝕜 → AddCircle p.

Equations

• TauCeti.Deck.addRightZMultiples a = ⟨Homeomorph.addRight ↑a, ⋯⟩

@[simp]

theorem TauCeti.Deck.addRightZMultiples_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} (a : ↥(AddSubgroup.zmultiples p)) (e : 𝕜) : ↑(addRightZMultiples a) e = e + ↑a

@[simp]

theorem TauCeti.Deck.addRightZMultiples_zero {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} : addRightZMultiples 0 = 1

@[simp]

theorem TauCeti.Deck.addRightZMultiples_add {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} (a b : ↥(AddSubgroup.zmultiples p)) : addRightZMultiples (a + b) = addRightZMultiples a * addRightZMultiples b

theorem TauCeti.Deck.addRightZMultiples_injective {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} : Function.Injective addRightZMultiples

theorem TauCeti.Deck.isRegular_addCircleCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} : IsRegular QuotientAddGroup.mk

The projection (↑) : 𝕜 → AddCircle p has regular deck action: it is surjective and its deck transformation group acts transitively on every fibre.

theorem deck.addCircleCoe_eq_add_apply_zero {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (φ : ↥(deck QuotientAddGroup.mk)) (e : 𝕜) : ↑φ e = e + ↑φ 0

On a preconnected domain with totally disconnected period subgroup, a deck transformation of (↑) : 𝕜 → AddCircle p is right translation by φ 0.

def TauCeti.Deck.addRightZMultiplesHom {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} : Multiplicative ↥(AddSubgroup.zmultiples p) →* ↥(deck QuotientAddGroup.mk)

Right translation by elements of the period subgroup, as a monoid homomorphism from the multiplicatively written zmultiples p to the deck transformation group of (↑) : 𝕜 → AddCircle p. This bundles addRightZMultiples.

Equations

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

theorem TauCeti.Deck.addRightZMultiplesHom_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} (a : Multiplicative ↥(AddSubgroup.zmultiples p)) : addRightZMultiplesHom a = addRightZMultiples (Multiplicative.toAdd a)

noncomputable def TauCeti.Deck.addCircleMulEquiv {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] : Multiplicative ↥(AddSubgroup.zmultiples p) ≃* ↥(deck QuotientAddGroup.mk)

The deck transformation group of (↑) : 𝕜 → AddCircle p on a preconnected domain with totally disconnected period subgroup is the group of translations by the period subgroup.

Equations

• TauCeti.Deck.addCircleMulEquiv = MulEquiv.ofBijective TauCeti.Deck.addRightZMultiplesHom ⋯

@[simp]

theorem TauCeti.Deck.addCircleMulEquiv_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (a : Multiplicative ↥(AddSubgroup.zmultiples p)) : addCircleMulEquiv a = addRightZMultiples (Multiplicative.toAdd a)

@[simp]

theorem deck.addCircleMulEquiv_symm_apply_coe {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (φ : ↥(deck QuotientAddGroup.mk)) : ↑(Multiplicative.toAdd (TauCeti.Deck.addCircleMulEquiv.symm φ)) = ↑φ 0

noncomputable def TauCeti.Deck.addCircleMulEquivInt {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hp : ¬IsOfFinAddOrder p) : Multiplicative ℤ ≃* ↥(deck QuotientAddGroup.mk)

For a non-torsion period, the deck transformation group of the quotient map (↑) : 𝕜 → AddCircle p on a preconnected domain with totally disconnected period subgroup is infinite cyclic: Multiplicative ℤ. In the standard real covering case this is the deck group of the universal cover ℝ → S¹.

Equations

• TauCeti.Deck.addCircleMulEquivInt hp = (AddEquiv.toMultiplicative (TauCeti.intEquivZMultiples hp)).trans TauCeti.Deck.addCircleMulEquiv

@[simp]

theorem TauCeti.Deck.addCircleMulEquivInt_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hp : ¬IsOfFinAddOrder p) (a : Multiplicative ℤ) (e : 𝕜) : ↑((addCircleMulEquivInt hp) a) e = e + Multiplicative.toAdd a • p

theorem TauCeti.Deck.addCircleMulEquivInt_symm_zsmul_apply_zero {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [PreconnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hp : ¬IsOfFinAddOrder p) (φ : ↥(deck QuotientAddGroup.mk)) : Multiplicative.toAdd ((addCircleMulEquivInt hp).symm φ) • p = ↑φ 0