Basic results on fundamental groupoids and fundamental groups

This file records a basic connectedness result for fundamental groupoids and when a map induced on fundamental groups is trivial: a characterization of trivial range loop by loop, and the basic consequences of triviality of the source fundamental group.

TauCeti.FundamentalGroup.map_range_eq_bot_iff was extracted from the proof of semilocallySimplyConnectedAt_iff_range_eq_bot in TauCeti/AlgebraicTopology/SemilocallySimplyConnected/On.lean, which is adapted from the Mathlib drafts #31449, #31576, and #38292 by Kim Morrison, for Stage 0.1 of the TauCetiRoadmap/UniversalCovers roadmap.

Main declarations

• FundamentalGroupoid.nonempty_hom: the fundamental groupoid of a path-connected space is connected.
• TauCeti.FundamentalGroup.map_range_eq_bot_iff: the induced map has trivial range exactly when every loop at the basepoint becomes nullhomotopic in the target.
• TauCeti.FundamentalGroup.map_range_eq_bot_of_subsingleton: if the source fundamental group is subsingleton, the range of any induced map from it is trivial.
• TauCeti.FundamentalGroup.map_range_le_of_subsingleton: if the source fundamental group is subsingleton, any induced-map range lies in any target subgroup.
• TauCeti.FundamentalGroup.map_range_le_of_simplyConnectedSpace: a simply connected domain has induced-map range contained in any target subgroup.
• TauCeti.FundamentalGroup.mapOfEq_range_eq_bot_of_subsingleton: the same triviality for the basepoint-transported induced map FundamentalGroup.mapOfEq.

theorem FundamentalGroupoid.nonempty_hom {Y : Type u_1} [TopologicalSpace Y] [PathConnectedSpace Y] (x y : FundamentalGroupoid Y) : Nonempty (x ⟶ y)

In the fundamental groupoid of a path-connected space every object receives a morphism from every other one, so the groupoid is connected.

theorem TauCeti.FundamentalGroup.map_fromPath {X : Type u_2} [TopologicalSpace X] {Y : Type u_4} [TopologicalSpace Y] (f : C(X, Y)) (base : X) (q : Path base base) : (FundamentalGroup.map f base) (FundamentalGroup.fromPath ⟦q⟧) = FundamentalGroup.fromPath ⟦q.map ⋯⟧

Mapping a loop class represented by a path is represented by mapping that path.

theorem TauCeti.FundamentalGroup.map_range_eq_bot_iff {X : Type u_2} [TopologicalSpace X] {Y : Type u_4} [TopologicalSpace Y] (f : C(X, Y)) (base : X) : (FundamentalGroup.map f base).range = ⊥ ↔ ∀ (γ : Path base base), (γ.map ⋯).Homotopic (Path.refl (f base))

The induced map is trivial exactly loop by loop. The map on fundamental groups induced by f has trivial range if and only if every loop at the basepoint becomes nullhomotopic after applying f.

@[simp]

theorem TauCeti.FundamentalGroup.map_range_eq_bot_of_subsingleton {X : Type u_2} [TopologicalSpace X] {A : Type u_3} [TopologicalSpace A] {a₀ : A} [Subsingleton (FundamentalGroup A a₀)] (f : C(A, X)) : (FundamentalGroup.map f a₀).range = ⊥

If the source fundamental group is subsingleton, the range of any induced map from it is trivial.

theorem TauCeti.FundamentalGroup.map_range_eq_bot_of_simplyConnectedSpace {X : Type u_2} [TopologicalSpace X] {A : Type u_3} [TopologicalSpace A] [SimplyConnectedSpace A] (f : C(A, X)) (a₀ : A) : (FundamentalGroup.map f a₀).range = ⊥

A simply connected domain has trivial induced fundamental-group range.

theorem TauCeti.FundamentalGroup.map_range_le_of_subsingleton {X : Type u_2} [TopologicalSpace X] {A : Type u_3} [TopologicalSpace A] {a₀ : A} [Subsingleton (FundamentalGroup A a₀)] (f : C(A, X)) (H : Subgroup (FundamentalGroup X (f a₀))) : (FundamentalGroup.map f a₀).range ≤ H

If the source fundamental group is subsingleton, its induced-map range lies in any target subgroup.

@[simp]

theorem TauCeti.FundamentalGroup.mapOfEq_range_eq_bot_of_subsingleton {X : Type u_2} [TopologicalSpace X] {A : Type u_3} [TopologicalSpace A] {a₀ : A} [Subsingleton (FundamentalGroup A a₀)] (f : C(A, X)) {x : X} (h : f a₀ = x) : (FundamentalGroup.mapOfEq f h).range = ⊥

If the source fundamental group is subsingleton, the range of the induced map transported to a prescribed target basepoint is trivial.

theorem TauCeti.FundamentalGroup.map_range_le_of_simplyConnectedSpace {X : Type u_2} [TopologicalSpace X] {A : Type u_3} [TopologicalSpace A] [SimplyConnectedSpace A] (f : C(A, X)) (a₀ : A) (H : Subgroup (FundamentalGroup X (f a₀))) : (FundamentalGroup.map f a₀).range ≤ H

A simply connected domain has induced fundamental-group range contained in any target subgroup.