Documentation

TauCeti.AlgebraicTopology.FundamentalGroup.WedgeSum

The fundamental group of a wedge sum #

Let (X i, x i) be path-connected pointed spaces, each base point x i having an open neighbourhood V i which deformation retracts onto x i (relative to x i). Then the fundamental group of the wedge sum ⋁ᵢ X i is the free product of the groups π₁(X i, x i): the homomorphism TauCeti.WedgeSum.fundamentalGroupLift out of the free product, induced by the inclusions of the summands, is an isomorphism.

This is the Seifert--van Kampen theorem for the family of open sets U i = X i ∨ ⋁_{j ≠ i} V j (TauCeti.vanKampenWideEquiv): any two of them meet in C = ⋁ⱼ V j, which contracts onto the wedge point, and each U i deformation retracts onto X i by contracting the other neighbourhoods V j.

For a family of circles Circle based at 1, where Circle ∖ {-1} contracts onto 1 along the chords to 1, the free product is a free product of copies of ℤ, so the fundamental group of a wedge of circles indexed by ι is the free group on ι (TauCeti.WedgeSum.circleFundamentalGroupMulEquiv), the generator i being the loop going once counterclockwise around the i-th circle.

Main declarations #

References #

source
noncomputable def TauCeti.WedgeSum.fundamentalGroupLift {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i) :
(Monoid.CoprodI fun (i : ι) => FundamentalGroup (X i) (x i)) →* FundamentalGroup (WedgeSum x) (base x)

The homomorphism from the free product of the fundamental groups of the summands to the fundamental group of the wedge sum, induced on each factor by the inclusion of the summand.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.WedgeSum.fundamentalGroupLift_of {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {i : ι} (g : FundamentalGroup (X i) (x i)) :
    (fundamentalGroupLift x) (Monoid.CoprodI.of g) = (FundamentalGroup.mapOfEq (incl x i) ⋯) g

    The open cover of the wedge sum #

    Fix open neighbourhoods V i ∋ x i with deformation retractions H i onto the base points. The open set U i of the cover is the wedge sum of the sets nbhd V i j, which are X i for j = i and V j otherwise.

    source
    theorem TauCeti.WedgeSum.fundamentalGroupLift_bijective {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} [∀ (i : ι), PathConnectedSpace (X i)] (hV : ∀ (i : ι), ∃ (V : Set (X i)), IsOpen V ∧ ∃ (hx : x i ∈ V), Nonempty ((ContinuousMap.id ↑V).HomotopyRel (ContinuousMap.const ↑V ⟨x i, hx⟩) {⟨x i, hx⟩})) :
    Function.Bijective ⇑(fundamentalGroupLift x)

    The fundamental group of a wedge sum is the free product of the fundamental groups of the summands. If every summand X i is path connected and its base point x i has an open neighbourhood V which deformation retracts onto x i, then the homomorphism from the free product of the groups π₁(X i, x i) to π₁(⋁ᵢ X i) induced by the inclusions of the summands is bijective.

    source
    noncomputable def TauCeti.WedgeSum.fundamentalGroupMulEquiv {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} [∀ (i : ι), PathConnectedSpace (X i)] (hV : ∀ (i : ι), ∃ (V : Set (X i)), IsOpen V ∧ ∃ (hx : x i ∈ V), Nonempty ((ContinuousMap.id ↑V).HomotopyRel (ContinuousMap.const ↑V ⟨x i, hx⟩) {⟨x i, hx⟩})) :
    (Monoid.CoprodI fun (i : ι) => FundamentalGroup (X i) (x i)) ≃* FundamentalGroup (WedgeSum x) (base x)

    The fundamental group of a wedge sum is the free product of the fundamental groups of the summands, under the hypotheses of TauCeti.WedgeSum.fundamentalGroupLift_bijective. Its underlying homomorphism is TauCeti.WedgeSum.fundamentalGroupLift.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.WedgeSum.fundamentalGroupMulEquiv_apply {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} [∀ (i : ι), PathConnectedSpace (X i)] (hV : ∀ (i : ι), ∃ (V : Set (X i)), IsOpen V ∧ ∃ (hx : x i ∈ V), Nonempty ((ContinuousMap.id ↑V).HomotopyRel (ContinuousMap.const ↑V ⟨x i, hx⟩) {⟨x i, hx⟩})) (g : Monoid.CoprodI fun (i : ι) => FundamentalGroup (X i) (x i)) :
      (fundamentalGroupMulEquiv hV) g = (fundamentalGroupLift x) g
      source
      @[simp]
      theorem TauCeti.WedgeSum.fundamentalGroupMulEquiv_symm_mapOfEq {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} [∀ (i : ι), PathConnectedSpace (X i)] (hV : ∀ (i : ι), ∃ (V : Set (X i)), IsOpen V ∧ ∃ (hx : x i ∈ V), Nonempty ((ContinuousMap.id ↑V).HomotopyRel (ContinuousMap.const ↑V ⟨x i, hx⟩) {⟨x i, hx⟩})) {i : ι} (g : FundamentalGroup (X i) (x i)) :
      (fundamentalGroupMulEquiv hV).symm ((FundamentalGroup.mapOfEq (incl x i) ⋯) g) = Monoid.CoprodI.of g

      The inverse of TauCeti.WedgeSum.fundamentalGroupMulEquiv sends the image of a loop in the i-th summand to the corresponding element of the i-th factor of the free product.

      A wedge of circles #

      source
      noncomputable def TauCeti.WedgeSum.circleFundamentalGroupMulEquiv (ι : Type u) :
      FundamentalGroup (WedgeSum fun (x : ι) => 1) (base fun (x : ι) => 1) ≃* FreeGroup ι

      The fundamental group of a wedge of circles is the free group on the circles. The generator i of the free group corresponds to the loop going once counterclockwise around the i-th circle (TauCeti.WedgeSum.circleFundamentalGroupMulEquiv_expLoop).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.WedgeSum.circleFundamentalGroupMulEquiv_expLoop {ι : Type u} (i : ι) :
        (circleFundamentalGroupMulEquiv ι) ((FundamentalGroup.mapOfEq (incl (fun (x : ι) => 1) i) ⋯) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk Circle.expLoop))) = FreeGroup.of i

        The loop going once counterclockwise around the i-th circle of a wedge of circles is the generator i of the free group.