The fundamental group is a homeomorphism invariant

Mathlib records the homomorphism FundamentalGroup.map induced by a continuous map and the variant FundamentalGroup.mapOfEq that adjusts the target basepoint along an equality, but it stops short of packaging a homeomorphism as an isomorphism of fundamental groups. This file supplies that: a homeomorphism e : X ≃ₜ Y induces a group isomorphism π₁(X, x) ≃* π₁(Y, e x), and more generally π₁(X, x) ≃* π₁(Y, y) whenever e x = y.

The forward map is FundamentalGroup.mapOfEq of e; the inverse is FundamentalGroup.mapOfEq of e.symm. The two round trips are the composition law mapOfEq_comp (the induced maps of two continuous maps compose to the induced map of their composite) applied to e.symm ∘ e = id and e ∘ e.symm = id, together with mapOfEq_id (the induced map of the identity is the identity). Both auxiliary lemmas are proved once here from Mathlib's FundamentalGroup.mapOfEq_apply and the Path.Homotopic.Quotient transport lemmas (map_comp, map_cast, cast_cast), and are useful on their own.

Transporting a fundamental-group computation across a homeomorphism is the group-level input the universal-covers roadmap needs for its Stage 4 applications: for example the fundamental group of the unit circle Circle ⊆ ℂ, obtained from the additive-circle computation through Mathlib's AddCircle.homeomorphCircle, and later π₁(ℝPⁿ). This mirrors the way TauCeti.FundamentalGroup.prodMulEquiv supplied the product formula the torus computation needs.

Main declarations

• TauCeti.FundamentalGroup.mapOfEq_comp: mapOfEq g hg (mapOfEq f hf p) = mapOfEq (g.comp f) _ p.
• TauCeti.FundamentalGroup.mapOfEq_id: mapOfEq (ContinuousMap.id X) h = id.
• TauCeti.FundamentalGroup.homeomorphMulEquivOfEq: π₁(X, x) ≃* π₁(Y, y) from e : X ≃ₜ Y with e x = y.
• TauCeti.FundamentalGroup.homeomorphMulEquiv: π₁(X, x) ≃* π₁(Y, e x).

theorem TauCeti.FundamentalGroup.mapOfEq_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {y : Y} {z : Z} (g : C(Y, Z)) (f : C(X, Y)) (hf : f x = y) (hg : g y = z) (p : FundamentalGroup X x) : (FundamentalGroup.mapOfEq g hg) ((FundamentalGroup.mapOfEq f hf) p) = (FundamentalGroup.mapOfEq (g.comp f) ⋯) p

The maps induced on fundamental groups by two continuous maps compose to the map induced by their composite: mapOfEq g hg (mapOfEq f hf p) = mapOfEq (g.comp f) _ p.

@[simp]

theorem TauCeti.FundamentalGroup.mapOfEq_id {X : Type u_1} [TopologicalSpace X] {x : X} (h : (ContinuousMap.id X) x = x) (p : FundamentalGroup X x) : (FundamentalGroup.mapOfEq (ContinuousMap.id X) h) p = p

The map induced on fundamental groups by the identity continuous map is the identity.

theorem TauCeti.FundamentalGroup.mapOfEq_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f₁ f₂ : C(X, Y)} (hfe : f₁ = f₂) (h₁ : f₁ x = y) (h₂ : f₂ x = y) (p : FundamentalGroup X x) : (FundamentalGroup.mapOfEq f₁ h₁) p = (FundamentalGroup.mapOfEq f₂ h₂) p

The induced map mapOfEq depends only on the underlying continuous map, not on the chosen proof of the basepoint equation: two equal continuous maps induce the same map.

theorem TauCeti.FundamentalGroup.mapOfEq_mapOfEq_of_comp_eq_id {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (g : C(Y, X)) (f : C(X, Y)) (hf : f x = y) (hg : g y = x) (hgf : g.comp f = ContinuousMap.id X) (p : FundamentalGroup X x) : (FundamentalGroup.mapOfEq g hg) ((FundamentalGroup.mapOfEq f hf) p) = p

If g ∘ f is the identity, then the induced map of g undoes the induced map of f.

noncomputable def TauCeti.FundamentalGroup.homeomorphMulEquivOfEq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (e : X ≃ₜ Y) (h : e x = y) : FundamentalGroup X x ≃* FundamentalGroup Y y

A homeomorphism e : X ≃ₜ Y carrying x to y induces an isomorphism of fundamental groups π₁(X, x) ≃* π₁(Y, y). The forward map is FundamentalGroup.mapOfEq of e; the inverse is FundamentalGroup.mapOfEq of e.symm.

Equations

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

@[simp]

theorem TauCeti.FundamentalGroup.homeomorphMulEquivOfEq_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (e : X ≃ₜ Y) (h : e x = y) (p : FundamentalGroup X x) : (homeomorphMulEquivOfEq e h) p = (FundamentalGroup.mapOfEq { toFun := ⇑e, continuous_toFun := ⋯ } h) p

@[simp]

theorem TauCeti.FundamentalGroup.homeomorphMulEquivOfEq_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (e : X ≃ₜ Y) (h : e x = y) (q : FundamentalGroup Y y) : (homeomorphMulEquivOfEq e h).symm q = (FundamentalGroup.mapOfEq { toFun := ⇑e.symm, continuous_toFun := ⋯ } ⋯) q

noncomputable def TauCeti.FundamentalGroup.homeomorphMulEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) : FundamentalGroup X x ≃* FundamentalGroup Y (e x)

A homeomorphism e : X ≃ₜ Y induces an isomorphism of fundamental groups π₁(X, x) ≃* π₁(Y, e x).

Equations

• TauCeti.FundamentalGroup.homeomorphMulEquiv e x = TauCeti.FundamentalGroup.homeomorphMulEquivOfEq e ⋯

@[simp]

theorem TauCeti.FundamentalGroup.homeomorphMulEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) (p : FundamentalGroup X x) : (homeomorphMulEquiv e x) p = (FundamentalGroup.mapOfEq { toFun := ⇑e, continuous_toFun := ⋯ } ⋯) p

@[simp]

theorem TauCeti.FundamentalGroup.homeomorphMulEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (x : X) (q : FundamentalGroup Y (e x)) : (homeomorphMulEquiv e x).symm q = (FundamentalGroup.mapOfEq { toFun := ⇑e.symm, continuous_toFun := ⋯ } ⋯) q