Documentation

TauCeti.AlgebraicTopology.FundamentalGroup.Homeomorph

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 #

source
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.

source
@[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.

source
@[simp]
theorem TauCeti.FundamentalGroup.mapOfEq_rfl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} (f : C(X, Y)) :
FundamentalGroup.mapOfEq f ⋯ = FundamentalGroup.map f x

Transporting the target basepoint along the reflexivity proof does nothing: mapOfEq f rfl is Mathlib's FundamentalGroup.map f x.

This is the comparison needed whenever a statement phrased with a general basepoint equation f x = y is applied to a lifting criterion phrased at the basepoint f x itself.

source
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.

source
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.

source
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.
Instances For
    source
    @[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
    source
    @[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
    source
    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
    Instances For
      source
      @[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
      source
      @[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