Homotopy

Results named in Tau Ceti's TauCeti.Topology.Homotopy modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

DefinitionAlexander's lemma#

A homeomorphism of the closed unit ball fixing the unit sphere is joined to the identity through homeomorphisms of the ball fixing the sphere.

Homeomorph.alexanderIsotopyClosedBall.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1))
  (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) :
  TauCeti.AmbientIsotopy ↑(Metric.closedBall 0 1)
Lean

Formalized in Tau Ceti as Homeomorph.alexanderIsotopyClosedBall.

Sources
LeanHomeomorph.alexanderIsotopyClosedBall

TheoremDold's local-to-global homotopy lifting theorem#

Let p : E → B be a map and (U i)_{i ∈ ι} a numerable cover of B, witnessed by a partition of unity ρ : PartitionOfUnity ι B with support (ρ i) ⊆ U i for every i. If each restriction p ⁻¹' U i → U i has the homotopy lifting property with respect to every open subset of A, then p has the homotopy lifting property with respect to A.

TauCeti.HasHomotopyLiftingProperty.of_partitionOfUnity.{w, u, v, u_1} {ι : Type u_1} {E : Type u}
  {B : Type v} {A : Type w} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace A]
  {p : E → B} {U : ι → Set B} (ρ : PartitionOfUnity ι B)
  (hρ : ∀ (i : ι), Function.support ⇑(ρ i) ⊆ U i)
  (hlift :
    ∀ (i : ι) (W : Set A),
      IsOpen W →
        TauCeti.HasHomotopyLiftingProperty (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯) ↑W) :
  TauCeti.HasHomotopyLiftingProperty p A
Lean

Formalized in Tau Ceti as TauCeti.HasHomotopyLiftingProperty.of_partitionOfUnity.

Sources
LeanTauCeti.HasHomotopyLiftingProperty.of_partitionOfUnity
Used by 1
Used byDold's local-to-global theorem for Hurewicz fibrations

TheoremDold's local-to-global theorem for Hurewicz fibrations#

A continuous map p : E → B whose restrictions p ⁻¹' U i → U i over a numerable cover (U i)_{i ∈ ι} of B (witnessed by a partition of unity ρ with support (ρ i) ⊆ U i) are Hurewicz fibrations is itself a Hurewicz fibration.

TauCeti.isHurewiczFibration_of_partitionOfUnity.{w, u, v, u_1} {ι : Type u_1} {E : Type u}
  {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : Continuous p)
  {U : ι → Set B} (ρ : PartitionOfUnity ι B) (hρ : ∀ (i : ι), Function.support ⇑(ρ i) ⊆ U i)
  (hpU : ∀ (i : ι), TauCeti.IsHurewiczFibration (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯)) :
  TauCeti.IsHurewiczFibration p
Lean

Formalized in Tau Ceti as TauCeti.isHurewiczFibration_of_partitionOfUnity.

Sources
LeanTauCeti.isHurewiczFibration_of_partitionOfUnity
Uses 1
Proof usesDold's local-to-global homotopy lifting theorem

TheoremStrøm's product theorem#

if closed subsets A ⊆ X and B ⊆ Y have the homotopy extension property, then so does A × Y ∪ X × B ⊆ X × Y.

TauCeti.HasHomotopyExtensionProperty.prod_univ_union_univ_prod.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A : Set X} {B : Set Y}
  (hA : TauCeti.HasHomotopyExtensionProperty A) (hA' : IsClosed A)
  (hB : TauCeti.HasHomotopyExtensionProperty B) (hB' : IsClosed B) :
  TauCeti.HasHomotopyExtensionProperty (A ×ˢ Set.univ ∪ Set.univ ×ˢ B)
Lean

Formalized in Tau Ceti as TauCeti.HasHomotopyExtensionProperty.prod_univ_union_univ_prod.

Sources
LeanTauCeti.HasHomotopyExtensionProperty.prod_univ_union_univ_prod
Uses 1
Proof usesStrøm's theorem

DefinitionStrøm's theorem#

A retraction r of the cylinder I × X onto {0} × X ∪ I × A, for a closed subset A, gives NDR data for A: the deformation is the second coordinate of r, and the control function is x ↦ ⨆ t, t - (r (t, x)).1, the largest amount by which r lowers a point of the cylinder over x.

TauCeti.NDRPair.ofRetraction.{u} {X : Type u} [TopologicalSpace X] {A : Set X}
  {r : C(↑unitInterval × X, ↑unitInterval × X)}
  (hr : ∀ (p : ↑unitInterval × X), r p ∈ TauCeti.cylinderExtensionDomain A)
  (hr' : ∀ p ∈ TauCeti.cylinderExtensionDomain A, r p = p) (hA : IsClosed A) : TauCeti.NDRPair A
Lean

Formalized in Tau Ceti as TauCeti.NDRPair.ofRetraction.

Sources
LeanTauCeti.NDRPair.ofRetraction
Used by 1
Used byStrøm's product theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.