Van Kampen for the circle covered by two arcs

This file checks the two-set van Kampen theorem for fundamental groupoids on a set of basepoints, TauCeti.isPushout_fundamentalGroupoidOn, on the simplest cover whose intersection is not path connected. The unit circle S¹ = sphere (0 : ℂ) 1 is covered by the two open arcs upper = S¹ ∖ {-i} and lower = S¹ ∖ {i}. Each arc is contractible, but their intersection S¹ ∖ {i, -i} has two path components, the right and the left open half circles, and 1 and -1 cannot be joined inside it (TauCeti.CircleArcs.not_joinedIn_one_neg_one). The based theorem TauCeti.isPushout_fundamentalGroup therefore does not apply with any basepoint, while the groupoid theorem applies with the two basepoints {1, -1}.

The pushout square on {1, -1} is computed as follows. The fundamental groupoids of the arcs on {1, -1} are indiscrete, since the arcs are simply connected, and that of the intersection is discrete. A group-valued consequence is that a functor out of the fundamental groupoid of S¹ on {1, -1} to a group K may send the classes of a path from 1 to -1 in upper and of one in lower to arbitrary elements of K (TauCeti.CircleArcs.lift), and is determined by these two values (TauCeti.CircleArcs.functor_ext).

Only after choosing the basepoint does the familiar based statement follow: if γ₊ runs from 1 to -1 in upper and γ₋ does so in lower, then the class of the loop γ₊ · γ₋⁻¹ generates π₁(S¹, 1) freely (TauCeti.CircleArcs.zpowersHom_bijective). Writing ℤ additively, the loop is sent to 1 by the ℤ-valued functor with values 0 on γ₊ and -1 on γ₋, which gives injectivity, and every loop is a power of it because conjugating by γ₊ retracts the groupoid onto π₁(S¹, 1) and that retraction agrees with the π₁(S¹, 1)-valued functor with values the identity on γ₊ and (γ₊ · γ₋⁻¹)⁻¹ on γ₋. The covering-space computation of the same group is Circle.fundamentalGroupMulEquiv.

Main declarations

• TauCeti.CircleArcs.upper, TauCeti.CircleArcs.lower, TauCeti.CircleArcs.basepoints: the two arcs and the two basepoints.
• TauCeti.CircleArcs.not_joinedIn_one_neg_one: the intersection of the arcs is not path connected.
• TauCeti.CircleArcs.isPushout: the van Kampen pushout square of the cover on {1, -1}.
• TauCeti.CircleArcs.lift, TauCeti.CircleArcs.lift_map_upper, TauCeti.CircleArcs.lift_map_lower, TauCeti.CircleArcs.functor_ext: the group-valued lift-and-uniqueness property for one arrow 1 ⟶ -1 in each arc.
• TauCeti.CircleArcs.zpowersHom_bijective: the based consequence, π₁(S¹, 1) ≅ ℤ generated by the loop through the two arcs.

References

• R. Brown, Topology and Groupoids, 3rd ed., Section 6.7 and Section 6.8 (the circle).
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 1.2.

The cover of the circle by two arcs

def TauCeti.CircleArcs.upper : Set ↑(Metric.sphere 0 1)

The unit circle with the point -i removed: an open arc containing the closed upper half circle.

Equations

• TauCeti.CircleArcs.upper = {z : ↑(Metric.sphere 0 1) | ↑z ≠ -Complex.I}

def TauCeti.CircleArcs.lower : Set ↑(Metric.sphere 0 1)

The unit circle with the point i removed: an open arc containing the closed lower half circle.

Equations

• TauCeti.CircleArcs.lower = {z : ↑(Metric.sphere 0 1) | ↑z ≠ Complex.I}

def TauCeti.CircleArcs.basepoints : Set ↑(Metric.sphere 0 1)

The two basepoints 1 and -1, one in each path component of upper ∩ lower.

Equations

• TauCeti.CircleArcs.basepoints = {1, -1}

@[simp]

theorem TauCeti.CircleArcs.mem_upper {z : ↑(Metric.sphere 0 1)} : z ∈ upper ↔ ↑z ≠ -Complex.I

@[simp]

theorem TauCeti.CircleArcs.mem_lower {z : ↑(Metric.sphere 0 1)} : z ∈ lower ↔ ↑z ≠ Complex.I

@[simp]

theorem TauCeti.CircleArcs.mem_basepoints {z : ↑(Metric.sphere 0 1)} : z ∈ basepoints ↔ z = 1 ∨ z = -1

theorem TauCeti.CircleArcs.isOpen_upper : IsOpen upper

theorem TauCeti.CircleArcs.isOpen_lower : IsOpen lower

theorem TauCeti.CircleArcs.upper_union_lower : upper ∪ lower = Set.univ

The two arcs cover the circle.

instance TauCeti.CircleArcs.contractibleSpace_upper : ContractibleSpace ↑upper

instance TauCeti.CircleArcs.contractibleSpace_lower : ContractibleSpace ↑lower

theorem TauCeti.CircleArcs.re_ne_zero_of_mem_inter {z : ↑(Metric.sphere 0 1)} (hz : z ∈ upper ∩ lower) : (↑z).re ≠ 0

A point of both arcs is not ±i, so its real part is nonzero.

theorem TauCeti.CircleArcs.not_joinedIn_one_neg_one : ¬JoinedIn (upper ∩ lower) 1 (-1)

The intersection of the two arcs is not path connected: 1 and -1 cannot be joined inside it.

theorem TauCeti.CircleArcs.isPushout : CategoryTheory.IsPushout (FundamentalGroupoidOn.map (ContinuousMap.inclusion ⋯) ⋯) (FundamentalGroupoidOn.map (ContinuousMap.inclusion ⋯) ⋯) (FundamentalGroupoidOn.map (ContinuousMap.subtypeVal upper) ⋯) (FundamentalGroupoidOn.map (ContinuousMap.subtypeVal lower) ⋯)

The van Kampen square of the circle covered by two arcs, on the basepoints {1, -1}. The intersection of the arcs has two path components, so a single basepoint would not do.

The fundamental groupoid on the two basepoints is free on the two arcs

@[reducible, inline]

noncomputable abbrev TauCeti.CircleArcs.one : FundamentalGroupoidOn basepoints

The basepoint 1, as an object of the fundamental groupoid of the circle on basepoints.

Equations

• TauCeti.CircleArcs.one = ⟨1, TauCeti.CircleArcs.one._proof_1⟩

@[reducible, inline]

noncomputable abbrev TauCeti.CircleArcs.negOne : FundamentalGroupoidOn basepoints

The basepoint -1, as an object of the fundamental groupoid of the circle on basepoints.

Equations

• TauCeti.CircleArcs.negOne = ⟨-1, TauCeti.CircleArcs.negOne._proof_1⟩

noncomputable def TauCeti.CircleArcs.lift {K : Type} [Group K] (kA kB : K) : CategoryTheory.Functor (FundamentalGroupoidOn basepoints) (CategoryTheory.SingleObj K)

The functor out of the fundamental groupoid of the circle on {1, -1} which sends the class of a path from 1 to -1 in upper to kA, and that of one in lower to kB. It exists by the van Kampen pushout TauCeti.CircleArcs.isPushout.

Equations

• TauCeti.CircleArcs.lift kA kB = TauCeti.CircleArcs.isPushout.desc (TauCeti.CircleArcs.arcFunctor✝ TauCeti.CircleArcs.upper kA) (TauCeti.CircleArcs.arcFunctor✝ TauCeti.CircleArcs.lower kB) ⋯

@[simp]

theorem TauCeti.CircleArcs.lift_map_upper {K : Type} [Group K] (kA kB : K) (γ : Path 1 (-1)) (hγ : ∀ (t : ↑unitInterval), γ t ∈ upper) : (lift kA kB).map (CategoryTheory.InducedCategory.homMk (Path.Homotopic.Quotient.mk γ)) = kA

TauCeti.CircleArcs.lift sends the class of a path from 1 to -1 in upper to kA.

@[simp]

theorem TauCeti.CircleArcs.lift_map_lower {K : Type} [Group K] (kA kB : K) (γ : Path 1 (-1)) (hγ : ∀ (t : ↑unitInterval), γ t ∈ lower) : (lift kA kB).map (CategoryTheory.InducedCategory.homMk (Path.Homotopic.Quotient.mk γ)) = kB

TauCeti.CircleArcs.lift sends the class of a path from 1 to -1 in lower to kB.

theorem TauCeti.CircleArcs.functor_ext {K : Type} [Group K] {F G : CategoryTheory.Functor (FundamentalGroupoidOn basepoints) (CategoryTheory.SingleObj K)} (γA : Path 1 (-1)) (hγA : ∀ (t : ↑unitInterval), γA t ∈ upper) (γB : Path 1 (-1)) (hγB : ∀ (t : ↑unitInterval), γB t ∈ lower) (hA : F.map (CategoryTheory.InducedCategory.homMk (Path.Homotopic.Quotient.mk γA)) = G.map (CategoryTheory.InducedCategory.homMk (Path.Homotopic.Quotient.mk γA))) (hB : F.map (CategoryTheory.InducedCategory.homMk (Path.Homotopic.Quotient.mk γB)) = G.map (CategoryTheory.InducedCategory.homMk (Path.Homotopic.Quotient.mk γB))) : F = G

A functor out of the fundamental groupoid of the circle on {1, -1} to a group is determined by its values on the class of a path from 1 to -1 in upper and on that of one in lower.

The based consequence

theorem TauCeti.CircleArcs.zpowersHom_bijective (γA : Path 1 (-1)) (hγA : ∀ (t : ↑unitInterval), γA t ∈ upper) (γB : Path 1 (-1)) (hγB : ∀ (t : ↑unitInterval), γB t ∈ lower) : Function.Bijective ⇑((zpowersHom (FundamentalGroup (↑(Metric.sphere 0 1)) 1)) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk (γA.trans γB.symm))))

The fundamental group of the circle, by van Kampen. If γA runs from 1 to -1 in upper and γB does so in lower, then n ↦ (γA · γB⁻¹)ⁿ is an isomorphism from ℤ onto π₁(S¹, 1).