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.
Path.exists_monotone_range_subpath_subset subdivides a path, by the Lebesgue number lemma on the
unit interval, so that each consecutive subpath lies in a member of a given family of sets. It is
used for the generation half of the groupoid van Kampen theorem in
AlgebraicTopology/FundamentalGroupoid/CoverGeneration.lean, and, repackaged over a
unitInterval.Partition as Path.exists_partition_with_property, for the tube construction in
Topology/Homotopy/TubeNeighborhood.lean. That construction also uses
unitInterval.exists_vertex_family, the path-connected vertex neighbourhoods of such a
subdivision; IsPathHomotopyTrivial, the property of a set that paths in it with common endpoints
are homotopic in the ambient space; and the pasting lemma
Path.Homotopic.trans_of_subpath_trans, which assembles homotopies over the segments of a
partition into a homotopy of the whole paths.
Path.trans_apply_of_le and Path.trans_apply_of_ge express a value of a concatenation as a
value of one of its two halves, and Path.subpath_apply_mem bounds the values of a subpath by the
values of the path on an interval containing its endpoints. They are used by the gluing
construction in AlgebraicTopology/FundamentalGroupoid/Glue.lean.
The path-homotopy quotient API also records that reversing twice is the identity and that the reverse of the constant class is constant.
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' := ⋯ }
Instances For
The underlying point of γ.codRestrict hmem at time t is just γ t, viewed in X.
Mapping γ.codRestrict hmem back along the subtype inclusion recovers γ.
Mapping a constant path gives the constant path at the image point.
The value of γ.trans δ at a parameter in the first half is a value of γ.
The value of γ.trans δ at a parameter in the second half is a value of δ.
A subpath of γ between two parameters of an interval that γ maps into V lies in V.
If the extended path stays inside U throughout [t₀, t₁], then the truncated subpath has
range in U.
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 ⋯ ⋯
Instances For
Every point on a path lies in the path component of its source.
A path whose source lies in a path component remains in that path component.
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.
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.
If every parameter s has some γ ⁻¹' U i as a neighbourhood, then γ can be subdivided
at finitely many monotone times, starting at 0 and ending at 1, so that the subpath between
any two consecutive times has range in some U i.
If every point on a path has an open neighborhood satisfying P, then there is a partition
0 = t₀ ≤ ⋯ ≤ tₙ = 1 such that each segment γ [tᵢ, tᵢ₊₁] lies in an open set satisfying
P.
Given open sets U i into which f maps the consecutive segments [t i, t (i + 1)] of a
monotone sequence in the unit interval, the path components of f (t j) in the intersections of
the adjacent U i are open, path-connected vertex sets, each contained in its adjacent U i.
Reversing a path-homotopy class twice recovers the original class.
The reverse of the constant path-homotopy class is the constant class.
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 := ⋯ }
A set of path-homotopy classes is open exactly when its preimage under quotient construction is open.
The concatenation identity Path.Homotopic.mk_subpath_trans_mk_subpath with endpoints
recast to given points. This cuts a path into pieces with prescribed, named endpoints.
A degenerate subpath represents the reflexivity class at its endpoint.
The full [0,1] subpath represents the original path, up to the endpoint casts inserted by
Path.subpath.
Composing on the left with a null-homotopic loop does not change the homotopy class.
Composing on the right with a null-homotopic loop does not change the homotopy class.
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.
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.
A loop whose conjugate by a path is null-homotopic is itself null-homotopic. This is the
path-homotopy analogue of a * b * a⁻¹ = 1 → b = 1.
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.
A loop that stays in a set whose inclusion is null-homotopic is itself null-homotopic in the ambient space.
Casting the reflexivity class at x along h : y = x gives the reflexivity class at y.
If trans γ (symm γ') = refl, then γ = γ'.
This is the quotient analogue of eq_of_div_eq_one : a / b = 1 → a = b.
A subset U of a topological space X is path-homotopy-trivial if any two paths
in X whose images lie in U and which share endpoints are homotopic in X.
This is the form of "U is simply connected" used in the universal-cover
construction: it is weaker than IsSimplyConnected U because the homotopy is not required
to lie inside U.
Equations
Instances For
The defining characterization of a path-homotopy-trivial set.
A loop in a path-homotopy-trivial set is nullhomotopic.
The pasting lemma. Let γ : Path x y and γ' : Path x' y', and let α j be "rung" paths
from γ (t j) to γ' (t j) at the vertices of a partition. If on each segment
γ|[tᵢ, tᵢ₊₁] · αᵢ₊₁ is homotopic to αᵢ · γ'|[tᵢ, tᵢ₊₁], then γ · αₙ is homotopic to
α₀ · γ'.