Documentation

TauCeti.AlgebraicTopology.FundamentalGroup.HomotopyEquiv

The fundamental group is a homotopy invariant #

A homotopy equivalence induces an isomorphism of fundamental groups. This is read off from the corresponding statement for higher homotopy groups in dimension one, through Mathlib's HomotopyGroup.pi1MulEquivFundamentalGroup, rather than reproved: the free-homotopy trace argument is dimension independent, and π_ 1 is the fundamental group.

This strengthens TauCeti.FundamentalGroup.homeomorphMulEquiv, which covers the case of a homeomorphism, but the two are independent as API: the homeomorphism version has an explicit inverse and needs no finiteness or decidability instances, so it stays the tool of choice when a homeomorphism is what is available.

Main declarations #

source
noncomputable def ContinuousMap.HomotopyEquiv.fundamentalGroupMulEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (x : X) :
FundamentalGroup X x ≃* FundamentalGroup Y (e.toFun x)

A homotopy equivalence induces an isomorphism of fundamental groups.

Equations
Instances For
    source
    @[simp]
    theorem ContinuousMap.HomotopyEquiv.fundamentalGroupMulEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (x : X) (a : FundamentalGroup X x) :
    (e.fundamentalGroupMulEquiv x) a = HomotopyGroup.pi1MulEquivFundamentalGroup (HomotopyGroup.map e.toFun ⋯ (HomotopyGroup.pi1MulEquivFundamentalGroup.symm a))

    Read through π_ 1, the isomorphism induced by a homotopy equivalence e is the map that e.toFun induces on homotopy groups.

    source
    @[simp]
    theorem ContinuousMap.HomotopyEquiv.fundamentalGroupMulEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (x : X) (b : FundamentalGroup Y (e.toFun x)) :
    (e.fundamentalGroupMulEquiv x).symm b = HomotopyGroup.pi1MulEquivFundamentalGroup (TauCeti.homotopyGroupTransport (((Nonempty.some ⋯).evalAt x).cast ⋯ ⋯) (HomotopyGroup.map e.invFun ⋯ (HomotopyGroup.pi1MulEquivFundamentalGroup.symm b)))

    Read through π_ 1, the inverse of the isomorphism induced by a homotopy equivalence e is the map that e.invFun induces on homotopy groups, followed by base-point change along the trace of the round trip e.invFun ∘ e.toFun ≃ id.

    source
    @[simp]
    theorem ContinuousMap.HomotopyEquiv.fundamentalGroupMulEquiv_refl {X : Type u_1} [TopologicalSpace X] (x : X) :
    (refl X).fundamentalGroupMulEquiv x = MulEquiv.refl (FundamentalGroup X x)

    The identity homotopy equivalence induces the identity isomorphism of fundamental groups.

    source
    @[simp]
    theorem ContinuousMap.HomotopyEquiv.fundamentalGroupMulEquiv_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] (e : HomotopyEquiv X Y) (e' : HomotopyEquiv Y Z) (x : X) :
    (e.trans e').fundamentalGroupMulEquiv x = (e.fundamentalGroupMulEquiv x).trans (e'.fundamentalGroupMulEquiv (e.toFun x))

    The isomorphism of fundamental groups induced by a composite of homotopy equivalences is the composite of the induced isomorphisms.

    source
    theorem ContinuousMap.HomotopyEquiv.fundamentalGroup_map_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (x : X) :
    Function.Bijective ⇑(FundamentalGroup.map e.toFun x)

    The forward map of a homotopy equivalence is bijective on fundamental groups. Unlike ContinuousMap.HomotopyEquiv.fundamentalGroupMulEquiv, this is stated for Mathlib's FundamentalGroup.map of e.toFun, so it computes on loop classes by mapping representatives. It is the full faithfulness of Mathlib's equivalence of fundamental groupoids FundamentalGroupoidFunctor.equivOfHomotopyEquiv, read on endomorphisms of x.

    source
    theorem ContinuousMap.HomotopyEquiv.nonempty_fundamentalGroupMulEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PathConnectedSpace X] (e : HomotopyEquiv X Y) (x : X) (y : Y) :
    Nonempty (FundamentalGroup X x ≃* FundamentalGroup Y y)

    Over a path connected space, homotopy equivalence identifies the fundamental groups at any pair of base points, by composing with base-point change.