n-connected maps

A continuous map f : X → Y is n-connected if every point of Y is joined by a path to a point of the image of f, and the induced map π_k(X, x) → π_k(Y, f x) is injective for every k < n and surjective for every k ≤ n, at every point x : X. Equivalently, the pair formed by the mapping cylinder of f and its bottom face is n-connected (Hatcher, Algebraic Topology, Section 4.1). Weak homotopy equivalences are exactly the maps that are n-connected for every n.

n-connected maps are the range in which homotopy groups control homology: an n-connected map induces isomorphisms on singular homology below degree n and a surjection in degree n (ContinuousMap.IsNConnected.isIso_singularHomologyMap and ContinuousMap.IsNConnected.epi_singularHomologyMap, in TauCeti.AlgebraicTopology.Singular.Homotopy.ConnectedMap). For instance, the inclusion of the n-skeleton of a CW complex is n-connected (TauCeti.isNConnected_inclusion_skeletonLT).

This file defines the predicate on Mathlib's cubical homotopy groups and proves its closure properties: it depends only on the homotopy class of the map, it is preserved by composition, and composing on either side with a weak homotopy equivalence neither creates nor destroys it.

Main declarations

• ContinuousMap.IsNConnected: the predicate.
• ContinuousMap.IsNConnected.map_injective, ContinuousMap.IsNConnected.map_surjective: the conditions for homotopy groups indexed by any finite type of cube directions.
• ContinuousMap.isWeakHomotopyEquivalence_iff_forall_isNConnected: a map is a weak homotopy equivalence exactly when it is n-connected for every n.
• ContinuousMap.IsNConnected.of_homotopic, ContinuousMap.IsNConnected.comp: invariance under homotopy and closure under composition.
• ContinuousMap.IsWeakHomotopyEquivalence.isNConnected_iff_of_comp_eq: in a square g ∘ i = j ∘ f with f and g weak homotopy equivalences, i and j have the same connectivity.
• ContinuousMap.IsWeakHomotopyEquivalence.isNConnected_comp_iff, ContinuousMap.IsWeakHomotopyEquivalence.isNConnected_comp_iff': composing with a weak homotopy equivalence, on the left or on the right, does not change the connectivity.

References

• A. Hatcher, Algebraic Topology, Section 4.1, the discussion of n-connected maps and mapping cylinders.

structure ContinuousMap.IsNConnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (n : ℕ) : Prop

A continuous map f : X → Y is n-connected if every point of Y is joined by a path to a point of the image of f, and the induced map π_k(X, x) → π_k(Y, f x) is injective for every k < n and surjective for every k ≤ n, at every point x : X.

In degree 0, where π_0(X, x) is the set of path components of X, injectivity says that f is injective on path components.

• exists_joined (y : Y) : ∃ (x : X), Joined (f x) y

  Every point of the target is joined by a path to a point of the image.

• injective (k : ℕ) (hk : k < n) (x : X) : Function.Injective (HomotopyGroup.map f ⋯)

  The induced map π_k(X, x) → π_k(Y, f x) is injective for k < n.

• surjective (k : ℕ) (hk : k ≤ n) (x : X) : Function.Surjective (HomotopyGroup.map f ⋯)

  The induced map π_k(X, x) → π_k(Y, f x) is surjective for k ≤ n.

theorem ContinuousMap.IsNConnected.map_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (hf : f.IsNConnected n) (N : Type u_4) [Finite N] (hN : Nat.card N < n) (x : X) : Function.Injective (HomotopyGroup.map f ⋯)

An n-connected map induces an injection on the homotopy group indexed by any finite type of fewer than n cube directions.

theorem ContinuousMap.IsNConnected.map_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (hf : f.IsNConnected n) (N : Type u_4) [Finite N] (hN : Nat.card N ≤ n) (x : X) : Function.Surjective (HomotopyGroup.map f ⋯)

An n-connected map induces a surjection on the homotopy group indexed by any finite type of at most n cube directions.

theorem ContinuousMap.IsNConnected.mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (hf : f.IsNConnected n) {m : ℕ} (hmn : m ≤ n) : f.IsNConnected m

An n-connected map is m-connected for every m ≤ n.

theorem ContinuousMap.IsNConnected.of_homotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} {f₀ f₁ : C(X, Y)} (hf : f₀.IsNConnected n) (h : f₀.Homotopic f₁) : f₁.IsNConnected n

A map homotopic to an n-connected map is n-connected.

theorem ContinuousMap.IsNConnected.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {g : C(Y, Z)} {n : ℕ} (hg : g.IsNConnected n) (hf : f.IsNConnected n) : (g.comp f).IsNConnected n

A composite of n-connected maps is n-connected.

theorem ContinuousMap.IsWeakHomotopyEquivalence.isNConnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : f.IsWeakHomotopyEquivalence) (n : ℕ) : f.IsNConnected n

A weak homotopy equivalence is n-connected for every n.

theorem ContinuousMap.IsWeakHomotopyEquivalence.isNConnected_iff_of_comp_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} {i : C(X, X')} {j : C(Y, Y')} (hf : f.IsWeakHomotopyEquivalence) (hg : g.IsWeakHomotopyEquivalence) (hi : g.comp i = j.comp f) : j.IsNConnected n ↔ i.IsNConnected n

In a square g ∘ i = j ∘ f whose maps f and g are weak homotopy equivalences, j is n-connected exactly when i is.

theorem ContinuousMap.IsWeakHomotopyEquivalence.isNConnected_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {g : C(Y, Z)} {n : ℕ} (hg : g.IsWeakHomotopyEquivalence) : (g.comp f).IsNConnected n ↔ f.IsNConnected n

Composing on the left with a weak homotopy equivalence does not change connectivity. If g is a weak homotopy equivalence, then g ∘ f is n-connected exactly when f is.

theorem ContinuousMap.IsWeakHomotopyEquivalence.isNConnected_comp_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {g : C(Y, Z)} {n : ℕ} (hf : f.IsWeakHomotopyEquivalence) : (g.comp f).IsNConnected n ↔ g.IsNConnected n

Composing on the right with a weak homotopy equivalence does not change connectivity. If f is a weak homotopy equivalence, then g ∘ f is n-connected exactly when g is.

theorem ContinuousMap.isWeakHomotopyEquivalence_iff_forall_isNConnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} : f.IsWeakHomotopyEquivalence ↔ ∀ (n : ℕ), f.IsNConnected n

A map is a weak homotopy equivalence exactly when it is n-connected for every n.