Path homotopy helpers

Small path and path-homotopy lemmas, mostly for the universal-cover construction. The quotient subpath identities are adapted from Kim Morrison's Mathlib universal-cover drafts, especially #31576 and #38292, following the earlier Tau Ceti work in #42.

Path.exists_homotopy_forall_mem_of_isSimplyConnected is not from that source: it records that SimplyConnectedSpace.paths_homotopic, applied in a subspace ↥V, yields a homotopy in the ambient space whose intermediate paths all stay in V. Analytic continuation consumes it in Analysis/Complex/Conformal/GlobalBranch.lean.

Path.homotopic_of_continuous_square is likewise adapted from Kim Morrison's #38292. It is used by AlgebraicTopology/UniversalCover/BasedPath.lean, where it previously lived privately, and by AlgebraicTopology/Sphere/Puncture.lean. The lemma Path.Homotopic.refl_of_forall_mem_of_nullhomotopic is not from #38292; it was factored out of AlgebraicTopology/SemilocallySimplyConnected/Basic.lean.

def Path.codRestrict {X : Type u_1} [TopologicalSpace X] {s : Set X} {x y : ↑s} (γ : Path ↑x ↑y) (hmem : ∀ (t : ↑unitInterval), γ t ∈ s) : Path x y

Restrict a path whose image lies in a subset to a path in the corresponding subtype. The source and target are the given subtype endpoints, and coercing the restricted path back to X recovers the original path pointwise.

Equations

• γ.codRestrict hmem = { toFun := Set.codRestrict (⇑γ) s hmem, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.codRestrict_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} {x y : ↑s} (γ : Path ↑x ↑y) (hmem : ∀ (t : ↑unitInterval), γ t ∈ s) (t : ↑unitInterval) : ↑((γ.codRestrict hmem) t) = γ t

The underlying point of γ.codRestrict hmem at time t is just γ t, viewed in X.

@[simp]

theorem Path.map_codRestrict {X : Type u_1} [TopologicalSpace X] {s : Set X} {x y : ↑s} (γ : Path ↑x ↑y) (hmem : ∀ (t : ↑unitInterval), γ t ∈ s) : (γ.codRestrict hmem).map ⋯ = γ

Mapping γ.codRestrict hmem back along the subtype inclusion recovers γ.

@[simp]

theorem Path.map_refl {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (a : X) : (refl a).map hf = refl (f a)

Mapping a constant path gives the constant path at the image point.

theorem Path.truncateOfLE_range_subset {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} (h : t₀ ≤ t₁) {U : Set X} (hU : Set.Icc t₀ t₁ ⊆ ⇑γ.extend ⁻¹' U) : Set.range ⇑(γ.truncateOfLE h) ⊆ U

If the extended path stays inside U throughout [t₀, t₁], then the truncated subpath has range in U.

noncomputable def Path.initialSegmentFamily {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t : ↑unitInterval) : Path a (γ t)

The family of initial segments of γ : Path a b: at parameter t : I, the path s ↦ γ.extend (min s t) from a to γ t (initialSegmentFamily_apply). At t = 0 this is the constant path at a (initialSegmentFamily_zero); at t = 1 it is γ itself, up to a trivial right-endpoint cast (initialSegmentFamily_one). The property consumers actually need is joint continuity in (t, s), recorded as continuous_initialSegmentFamily_uncurry.

Equations

• γ.initialSegmentFamily t = (γ.truncate 0 ↑t).cast ⋯ ⋯

theorem Path.mem_pathComponent {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t : ↑unitInterval) : γ t ∈ pathComponent a

Every point on a path lies in the path component of its source.

theorem Path.mem_pathComponent_of_mem {X : Type u_1} [TopologicalSpace X] {a b x₀ : X} (γ : Path a b) (ha : a ∈ pathComponent x₀) (t : ↑unitInterval) : γ t ∈ pathComponent x₀

A path whose source lies in a path component remains in that path component.

theorem Path.continuous_initialSegmentFamily_uncurry {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : Continuous ↿γ.initialSegmentFamily

@[simp]

theorem Path.initialSegmentFamily_zero {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : γ.initialSegmentFamily 0 = (refl a).cast ⋯ ⋯

@[simp]

theorem Path.initialSegmentFamily_one {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : γ.initialSegmentFamily 1 = γ.cast ⋯ ⋯

theorem Path.exists_homotopy_forall_mem_of_isSimplyConnected {X : Type u_1} [TopologicalSpace X] {V : Set X} (hV : IsSimplyConnected V) {a b : X} {p q : Path a b} (hp : ∀ (t : ↑unitInterval), p t ∈ V) (hq : ∀ (t : ↑unitInterval), q t ∈ V) : ∃ (K : p.Homotopy q), ∀ (t x : ↑unitInterval), K (t, x) ∈ V

Two paths with the same endpoints in a simply connected set are homotopic inside it. For p and q running in V between the same two points of V, there is a homotopy from p to q every intermediate path of which again lies in V.

The homotopy is stated in the ambient space rather than in ↥V, with membership in V as a separate conclusion: that is the form consumers want, and it spares them transporting along the subtype.

theorem Path.homotopic_of_continuous_square {X : Type u_1} [TopologicalSpace X] {a b : X} {p q : Path a b} (K : ↑unitInterval × ↑unitInterval → X) (hK_cont : Continuous K) (hK_zero : ∀ (s : ↑unitInterval), K (0, s) = p s) (hK_one : ∀ (s : ↑unitInterval), K (1, s) = q s) (hK_left : ∀ (t : ↑unitInterval), K (t, 0) = a) (hK_right : ∀ (t : ↑unitInterval), K (t, 1) = b) : p.Homotopic q

A square with prescribed edges is a path homotopy. A continuous map on I × I that restricts to p at t = 0 and to q at t = 1, and is constant along each of the edges s = 0 and s = 1, exhibits p and q as homotopic paths.

@[instance_reducible]

instance Path.Homotopic.Quotient.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] (x₀ x : X) : TopologicalSpace (Homotopic.Quotient x₀ x)

The quotient topology on path-homotopy classes. This instance is load-bearing: Path.Homotopic.Quotient is a def over Quotient, and instance search does not unfold it to find the generic TopologicalSpace (Quotient _).

Equations

• Path.Homotopic.Quotient.instTopologicalSpace x₀ x = { IsOpen := Path.Homotopic.Quotient.instTopologicalSpace._aux_1 x₀ x, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem Path.Homotopic.Quotient.isOpen_iff_preimage_mk {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} {S : Set (Homotopic.Quotient x₀ x₁)} : IsOpen S ↔ IsOpen (mk ⁻¹' S)

A set of path-homotopy classes is open exactly when its preimage under quotient construction is open.

@[simp]

theorem Path.Homotopic.Quotient.subpath_trans {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) (a b c : ↑unitInterval) : (mk (p.subpath a b)).trans (mk (p.subpath b c)) = mk (p.subpath a c)

In the path-homotopy quotient, concatenating adjacent subpaths of p gives the larger subpath from the first endpoint to the last endpoint.

theorem Path.Homotopic.Quotient.subpath_self {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) (a : ↑unitInterval) : mk (p.subpath a a) = refl (p a)

A degenerate subpath represents the reflexivity class at its endpoint.

theorem Path.Homotopic.Quotient.subpath_zero_one {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) : mk (p.subpath 0 1) = (mk p).cast ⋯ ⋯

The full [0,1] subpath represents the original path, up to the endpoint casts inserted by Path.subpath.

theorem Path.Homotopic.trans_left_of_nullhomotopic {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} {γ₀ : Path x₀ x₀} {γ₁ : Path x₀ x₁} (hγ₀ : γ₀.Homotopic (Path.refl x₀)) : (γ₀.trans γ₁).Homotopic γ₁

Composing on the left with a null-homotopic loop does not change the homotopy class.

theorem Path.Homotopic.trans_right_of_nullhomotopic {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} {γ₀ : Path x₀ x₁} {γ₁ : Path x₁ x₁} (hγ₁ : γ₁.Homotopic (Path.refl x₁)) : (γ₀.trans γ₁).Homotopic γ₀

Composing on the right with a null-homotopic loop does not change the homotopy class.

theorem Path.Homotopic.of_trans_symm {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} {γ γ' : Path x₀ x₁} (h : (γ.trans γ'.symm).Homotopic (Path.refl x₀)) : γ.Homotopic γ'

If γ.trans γ'.symm is nullhomotopic, then γ and γ' are homotopic. This is the path-homotopy analogue of a * b⁻¹ = 1 → a = b.

theorem Path.Homotopic.trans_right_cancel {X : Type u_1} [TopologicalSpace X] {x₀ x₁ x₂ : X} {γ δ : Path x₀ x₁} {e : Path x₁ x₂} (h : (γ.trans e).Homotopic (δ.trans e)) : γ.Homotopic δ

Right cancellation in the fundamental groupoid: if γ.trans e and δ.trans e are homotopic, then γ and δ are homotopic. This is the path-homotopy analogue of a * c = b * c → a = b.

theorem Path.Homotopic.trans_left_cancel {X : Type u_1} [TopologicalSpace X] {x₀ x₁ x₂ : X} {e : Path x₀ x₁} {γ δ : Path x₁ x₂} (h : (e.trans γ).Homotopic (e.trans δ)) : γ.Homotopic δ

Left cancellation in the fundamental groupoid: if e.trans γ and e.trans δ are homotopic, then γ and δ are homotopic. This is the path-homotopy analogue of c * a = c * b → a = b.

theorem Path.Homotopic.map_nullhomotopic_of_nullhomotopic {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} (hf : f.Nullhomotopic) {a : X} (γ : Path a a) : (γ.map ⋯).Homotopic (Path.refl (f a))

The image of a based loop under a null-homotopic continuous map is null-homotopic in the target: a map homotopic to a constant collapses every loop to the constant loop.

theorem Path.Homotopic.refl_of_forall_mem_of_nullhomotopic {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : { toFun := Subtype.val, continuous_toFun := ⋯ }.Nullhomotopic) {x : X} (γ : Path x x) (hγ : ∀ (t : ↑unitInterval), γ t ∈ s) : γ.Homotopic (Path.refl x)

A loop that stays in a set whose inclusion is null-homotopic is itself null-homotopic in the ambient space.

@[simp]

theorem Path.Homotopic.Quotient.refl_cast {X : Type u_1} [TopologicalSpace X] {x y : X} (h : y = x) : (refl x).cast h h = refl y

Casting the reflexivity class at x along h : y = x gives the reflexivity class at y.

theorem Path.Homotopic.Quotient.eq_of_trans_symm {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} {γ γ' : Homotopic.Quotient x₀ x₁} (h : γ.trans γ'.symm = refl x₀) : γ = γ'

If trans γ (symm γ') = refl, then γ = γ'. This is the quotient analogue of eq_of_div_eq_one : a / b = 1 → a = b.