Path homotopy helpers

Small path and path-homotopy quotient lemmas used by 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.

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 γ.

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.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 ⋯ ⋯

@[implicit_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.

@[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.