Fundamental groups of additive and complex circles

The covering (↑) : ℝ → AddCircle p is the universal cover of the circle: its total space ℝ is contractible, hence simply connected, and the cover is regular with deck group Multiplicative ℤ (the translations by the period subgroup, computed in TauCeti.Deck.addCircleMulEquivInt). The regular-cover comparison TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv then identifies the fundamental group of the base with the deck group itself (the opposite drops out because the deck group is commutative), giving

FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ

for any nonzero real period p. Specialising to the unit circle UnitAddCircle = ℝ ⧸ ℤ yields the classical π₁(S¹) ≅ ℤ.

For a nonzero real period T, AddCircle.homeomorphCircle identifies AddCircle T with Mathlib's complex unit circle Circle. Transporting the additive-circle computation across this homeomorphism gives FundamentalGroup Circle x ≃* Multiplicative ℤ at every basepoint.

The regularity input is elementary and holds for an arbitrary topological additive group: two points of 𝕜 with the same image under (↑) : 𝕜 → AddCircle p differ by an element of the period subgroup zmultiples p, and translation by that element is a deck transformation, so deck ((↑) : 𝕜 → AddCircle p) acts transitively on every fibre.

Main declarations

• AddCircle.fundamentalGroupMulEquivZMultiples: for a covering projection from a simply connected additive group, the fundamental group of AddCircle p is the period subgroup.
• AddCircle.fundamentalGroupMulEquivInt: for a covering projection from a simply connected additive group with non-torsion period, the fundamental group of AddCircle p is Multiplicative ℤ.
• AddCircle.fundamentalGroupMulEquiv: for a nonzero real period, the fundamental group of AddCircle p (based at any point with a chosen lift) is Multiplicative ℤ.
• AddCircle.fundamentalGroupMulEquivZero: the basepoint-0 specialisation, using the lift 0 : ℝ.
• UnitAddCircle.fundamentalGroupMulEquiv: π₁(S¹) ≅ ℤ for the unit circle.
• Circle.fundamentalGroupMulEquiv: π₁(Circle, x) ≃* Multiplicative ℤ.
• Circle.expLoop and Circle.fundamentalGroupMulEquiv_expLoop: the loop t ↦ exp(2πit), going once counterclockwise around the circle, is sent to the generator ofAdd 1.
• Circle.fundamentalGroupMulEquiv_fromPath: the class of a loop is sent to its degree Circle.degree, computed from angle lifts.
• Circle.fundamentalGroupMulEquiv_map_pow: the n-th power map of the circle acts on the fundamental group as multiplication by n.

References

It consumes Mathlib's AddCircle covering map (AddCircle.isCoveringMap_coe, Junyan Xu) and the contractibility of a real topological vector space, together with Tau Ceti's deck-transformation theory.

noncomputable def AddCircle.fundamentalGroupMulEquivZMultiples {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) : FundamentalGroup (AddCircle p) x ≃* Multiplicative ↥(AddSubgroup.zmultiples p)

For a covering projection (↑) : 𝕜 → AddCircle p from a simply connected preconnected topological additive commutative group with totally disconnected period subgroup, the fundamental group of AddCircle p is the multiplicative period subgroup.

Equations

• AddCircle.fundamentalGroupMulEquivZMultiples hcov e = (⋯.fundamentalGroupDeckEquiv hcov e ⋯).trans TauCeti.Deck.addCircleMulEquiv.symm

theorem AddCircle.fundamentalGroupMulEquivZMultiples_apply_eq_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (γ : FundamentalGroup (AddCircle p) x) (n : Multiplicative ↥(AddSubgroup.zmultiples p)) : (fundamentalGroupMulEquivZMultiples hcov e) γ = n ↔ ↑(hcov.monodromy γ e) = ↑e + ↑(Multiplicative.toAdd n)

Characterization of the period-subgroup element assigned by fundamentalGroupMulEquivZMultiples: a loop class maps to n exactly when its monodromy translate of the chosen lift differs by the element n.

@[simp]

theorem AddCircle.fundamentalGroupMulEquivZMultiples_symm_monodromy {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (n : Multiplicative ↥(AddSubgroup.zmultiples p)) : ↑(hcov.monodromy ((fundamentalGroupMulEquivZMultiples hcov e).symm n) e) = ↑e + ↑(Multiplicative.toAdd n)

The inverse of the period-subgroup equivalence sends n to the loop class whose monodromy translates the chosen lift by n.

theorem AddCircle.fundamentalGroupMulEquivZMultiples_eq_one_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (γ : FundamentalGroup (AddCircle p) x) : (fundamentalGroupMulEquivZMultiples hcov e) γ = 1 ↔ hcov.monodromy γ e = e

A loop class maps to 1 under the period-subgroup equivalence exactly when its monodromy fixes the chosen lift.

noncomputable def AddCircle.fundamentalGroupMulEquivInt {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) (hp : ¬IsOfFinAddOrder p) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) : FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ

For a covering projection (↑) : 𝕜 → AddCircle p from a simply connected preconnected topological additive commutative group with totally disconnected non-torsion period subgroup, the fundamental group of AddCircle p is infinite cyclic: FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ.

Equations

• AddCircle.fundamentalGroupMulEquivInt hcov hp e = (AddCircle.fundamentalGroupMulEquivZMultiples hcov e).trans (AddEquiv.toMultiplicative (TauCeti.intEquivZMultiples hp)).symm

theorem AddCircle.fundamentalGroupMulEquivInt_apply_eq_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) (hp : ¬IsOfFinAddOrder p) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (γ : FundamentalGroup (AddCircle p) x) (n : Multiplicative ℤ) : (fundamentalGroupMulEquivInt hcov hp e) γ = n ↔ ↑(hcov.monodromy γ e) = ↑e + Multiplicative.toAdd n • p

Characterization of the integer assigned by fundamentalGroupMulEquivInt: a loop class maps to n exactly when its monodromy translate of the chosen lift differs by n • p.

@[simp]

theorem AddCircle.fundamentalGroupMulEquivInt_symm_monodromy {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) (hp : ¬IsOfFinAddOrder p) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (n : Multiplicative ℤ) : ↑(hcov.monodromy ((fundamentalGroupMulEquivInt hcov hp e).symm n) e) = ↑e + Multiplicative.toAdd n • p

The inverse generic integer equivalence sends n to the loop class whose monodromy translates the chosen lift by n • p.

theorem AddCircle.fundamentalGroupMulEquivInt_eq_one_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] {p : 𝕜} [SimplyConnectedSpace 𝕜] [TotallyDisconnectedSpace ↥(AddSubgroup.zmultiples p)] (hcov : IsCoveringMap QuotientAddGroup.mk) (hp : ¬IsOfFinAddOrder p) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (γ : FundamentalGroup (AddCircle p) x) : (fundamentalGroupMulEquivInt hcov hp e) γ = 1 ↔ hcov.monodromy γ e = e

A loop class maps to 1 under the generic integer equivalence exactly when its monodromy fixes the chosen lift.

noncomputable def AddCircle.fundamentalGroupMulEquiv (p : ℝ) (hp : p ≠ 0) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) : FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ

For a nonzero real period p, the fundamental group of the circle AddCircle p, based at any point x with a chosen lift e : (↑) ⁻¹' {x}, is infinite cyclic: FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ.

Equations

• AddCircle.fundamentalGroupMulEquiv p hp e = AddCircle.fundamentalGroupMulEquivInt ⋯ ⋯ e

theorem AddCircle.fundamentalGroupMulEquiv_apply_eq_iff (p : ℝ) (hp : p ≠ 0) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (γ : FundamentalGroup (AddCircle p) x) (n : Multiplicative ℤ) : (fundamentalGroupMulEquiv p hp e) γ = n ↔ ↑(⋯.monodromy γ e) = ↑e + Multiplicative.toAdd n • p

Characterization of the integer assigned by fundamentalGroupMulEquiv: a loop class maps to n exactly when its monodromy translate of the chosen lift differs by n • p.

@[simp]

theorem AddCircle.fundamentalGroupMulEquiv_symm_monodromy (p : ℝ) (hp : p ≠ 0) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (n : Multiplicative ℤ) : ↑(⋯.monodromy ((fundamentalGroupMulEquiv p hp e).symm n) e) = ↑e + Multiplicative.toAdd n • p

The inverse equivalence sends n to the loop class whose monodromy translates the chosen lift by n • p.

theorem AddCircle.fundamentalGroupMulEquiv_eq_one_iff (p : ℝ) (hp : p ≠ 0) {x : AddCircle p} (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) (γ : FundamentalGroup (AddCircle p) x) : (fundamentalGroupMulEquiv p hp e) γ = 1 ↔ ⋯.monodromy γ e = e

A loop class maps to 1 under fundamentalGroupMulEquiv exactly when its monodromy fixes the chosen lift.

noncomputable def AddCircle.fundamentalGroupMulEquivZero (p : ℝ) (hp : p ≠ 0) : FundamentalGroup (AddCircle p) 0 ≃* Multiplicative ℤ

The fundamental group of the circle AddCircle p based at 0, with the lift 0 : ℝ, is Multiplicative ℤ.

Equations

• AddCircle.fundamentalGroupMulEquivZero p hp = AddCircle.fundamentalGroupMulEquiv p hp ⟨0, ⋯⟩

theorem AddCircle.fundamentalGroupMulEquivZero_apply_eq_iff (p : ℝ) (hp : p ≠ 0) (γ : FundamentalGroup (AddCircle p) 0) (n : Multiplicative ℤ) : (fundamentalGroupMulEquivZero p hp) γ = n ↔ ↑(⋯.monodromy γ ⟨0, ⋯⟩) = Multiplicative.toAdd n • p

Characterization of the integer assigned by the basepoint-0 specialization.

@[simp]

theorem AddCircle.fundamentalGroupMulEquivZero_apply (p : ℝ) (hp : p ≠ 0) (γ : FundamentalGroup (AddCircle p) 0) : (fundamentalGroupMulEquivZero p hp) γ = (fundamentalGroupMulEquiv p hp ⟨0, ⋯⟩) γ

@[simp]

theorem AddCircle.fundamentalGroupMulEquivZero_symm_apply (p : ℝ) (hp : p ≠ 0) (n : Multiplicative ℤ) : (fundamentalGroupMulEquivZero p hp).symm n = (fundamentalGroupMulEquiv p hp ⟨0, ⋯⟩).symm n

theorem AddCircle.fundamentalGroupMulEquivZero_symm_monodromy (p : ℝ) (hp : p ≠ 0) (n : Multiplicative ℤ) : ↑(⋯.monodromy ((fundamentalGroupMulEquivZero p hp).symm n) ⟨0, ⋯⟩) = Multiplicative.toAdd n • p

The inverse of the basepoint-0 specialization has monodromy translation n • p.

theorem AddCircle.fundamentalGroupMulEquivZero_eq_one_iff (p : ℝ) (hp : p ≠ 0) (γ : FundamentalGroup (AddCircle p) 0) : (fundamentalGroupMulEquivZero p hp) γ = 1 ↔ ⋯.monodromy γ ⟨0, ⋯⟩ = ⟨0, ⋯⟩

A loop class maps to 1 under the basepoint-0 specialization exactly when its monodromy fixes the zero lift.

noncomputable def UnitAddCircle.fundamentalGroupMulEquiv : FundamentalGroup UnitAddCircle 0 ≃* Multiplicative ℤ

The fundamental group of the unit circle S¹ = ℝ ⧸ ℤ is ℤ: FundamentalGroup UnitAddCircle 0 ≃* Multiplicative ℤ. This is the classical π₁(S¹) ≅ ℤ.

Equations

• UnitAddCircle.fundamentalGroupMulEquiv = AddCircle.fundamentalGroupMulEquivZero 1 UnitAddCircle.fundamentalGroupMulEquiv._proof_1✝

theorem UnitAddCircle.fundamentalGroupMulEquiv_apply_eq_iff (γ : FundamentalGroup UnitAddCircle 0) (n : Multiplicative ℤ) : fundamentalGroupMulEquiv γ = n ↔ ↑(⋯.monodromy γ ⟨0, fundamentalGroupMulEquiv_apply_eq_iff._proof_1⟩) = ↑(Multiplicative.toAdd n)

Characterization of the integer assigned by the unit-circle equivalence.

@[simp]

theorem UnitAddCircle.fundamentalGroupMulEquiv_symm_monodromy (n : Multiplicative ℤ) : ↑(⋯.monodromy (fundamentalGroupMulEquiv.symm n) ⟨0, fundamentalGroupMulEquiv_apply_eq_iff._proof_1⟩) = ↑(Multiplicative.toAdd n)

The inverse of the unit-circle equivalence has monodromy translation by n.

theorem UnitAddCircle.fundamentalGroupMulEquiv_eq_one_iff (γ : FundamentalGroup UnitAddCircle 0) : fundamentalGroupMulEquiv γ = 1 ↔ ⋯.monodromy γ ⟨0, fundamentalGroupMulEquiv_apply_eq_iff._proof_1⟩ = ⟨0, fundamentalGroupMulEquiv_apply_eq_iff._proof_1⟩

A unit-circle loop class maps to 1 exactly when its monodromy fixes the zero lift.

noncomputable def Circle.fundamentalGroupMulEquiv (x : Circle) : FundamentalGroup Circle x ≃* Multiplicative ℤ

The fundamental group of the complex unit circle Circle = {z : ℂ | ‖z‖ = 1}, based at x, is Multiplicative ℤ: π₁(S¹, x) ≅ ℤ. It is obtained by changing the basepoint to 1 : Circle, then transporting the additive-circle computation at 0 across AddCircle.homeomorphCircle : AddCircle (2 * π) ≃ₜ Circle.

Equations

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

theorem Circle.fundamentalGroupMulEquiv_def (x : Circle) : x.fundamentalGroupMulEquiv = (FundamentalGroup.fundamentalGroupMulEquivOfPathConnected x 1).trans ((TauCeti.FundamentalGroup.homeomorphMulEquivOfEq (AddCircle.homeomorphCircle ⋯).symm ⋯).trans (AddCircle.fundamentalGroupMulEquivZero (2 * Real.pi) ⋯))

fundamentalGroupMulEquiv factors as Mathlib's basepoint-change isomorphism FundamentalGroup Circle x ≃* FundamentalGroup Circle 1, followed by the canonical-basepoint computation transported from AddCircle (2 * π) along AddCircle.homeomorphCircle.

theorem Circle.fundamentalGroupMulEquiv_fromPath {x : Circle} (γ : Path x x) : x.fundamentalGroupMulEquiv (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)) = Multiplicative.ofAdd (degree γ)

The isomorphism π₁(S¹) ≃* ℤ is the degree. The class of a loop is sent to its degree Circle.degree, the number of full turns of any continuous angle lift.

noncomputable def Circle.expLoop : Path 1 1

The loop t ↦ exp(2πit) at 1, going once counterclockwise around the unit circle.

Equations

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

@[simp]

theorem Circle.expLoop_apply (t : ↑unitInterval) : expLoop t = exp (2 * Real.pi * ↑t)

@[simp]

theorem Circle.fundamentalGroupMulEquiv_expLoop : (fundamentalGroupMulEquiv 1) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk expLoop)) = Multiplicative.ofAdd 1

The counterclockwise loop generates π₁(S¹) positively. The isomorphism π₁(Circle, 1) ≃* Multiplicative ℤ sends the class of t ↦ exp(2πit) to ofAdd 1.

theorem Circle.fundamentalGroupMulEquiv_map_pow (n : ℕ) {x : Circle} (γ : FundamentalGroup Circle x) : ({ toFun := fun (x : Circle) => x ^ n, continuous_toFun := ⋯ } x).fundamentalGroupMulEquiv ((FundamentalGroup.map { toFun := fun (x : Circle) => x ^ n, continuous_toFun := ⋯ } x) γ) = x.fundamentalGroupMulEquiv γ ^ n

The n-th power map of the circle acts on π₁(S¹) ≅ ℤ as multiplication by n. The isomorphism fundamentalGroupMulEquiv sends the image of a loop class under z ↦ z ^ n to the n-th power of the image of the class.