Homotopies along paths of linear isometries

A path γ of linear isometries of a normed space E, continuous in the operator-norm topology, moves every point x of E along the path t ↦ γ t x. On a subset S of E preserved by every γ t, this is a homotopy (t, x) ↦ γ t x between any two self-maps of S acting as γ 0 and γ 1.

Main declarations

• TauCeti.linearIsometryEquivPathHomotopy: the homotopy (t, x) ↦ γ t x of self-maps of an invariant subset S, read on ULift S so that it applies to the disks and spheres of TopCat.
• TauCeti.coe_linearIsometryEquivPathHomotopy_apply_down: the homotopy acts at time t by γ t.

def TauCeti.linearIsometryEquivPathHomotopy {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Set E} {γ : ↑unitInterval → E ≃ₗᵢ[𝕜] E} (hS : ∀ (t : ↑unitInterval), Set.MapsTo (⇑(γ t)) S S) (hγ : Continuous fun (t : ↑unitInterval) => ↑↑(γ t)) {f₀ f₁ : C(ULift.{u, u_2} ↑S, ULift.{u, u_2} ↑S)} (hf₀ : ∀ (x : ULift.{u, u_2} ↑S), ↑(f₀ x).down = (γ 0) ↑x.down) (hf₁ : ∀ (x : ULift.{u, u_2} ↑S), ↑(f₁ x).down = (γ 1) ↑x.down) : f₀.Homotopy f₁

A path γ of linear isometries of E, continuous in the operator-norm topology and preserving a subset S, gives the homotopy (t, x) ↦ γ t x from a self-map f₀ of S acting as γ 0 to a self-map f₁ of S acting as γ 1.

@[simp]

theorem TauCeti.coe_linearIsometryEquivPathHomotopy_apply_down {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Set E} {γ : ↑unitInterval → E ≃ₗᵢ[𝕜] E} (hS : ∀ (t : ↑unitInterval), Set.MapsTo (⇑(γ t)) S S) (hγ : Continuous fun (t : ↑unitInterval) => ↑↑(γ t)) {f₀ f₁ : C(ULift.{u, u_2} ↑S, ULift.{u, u_2} ↑S)} (hf₀ : ∀ (x : ULift.{u, u_2} ↑S), ↑(f₀ x).down = (γ 0) ↑x.down) (hf₁ : ∀ (x : ULift.{u, u_2} ↑S), ↑(f₁ x).down = (γ 1) ↑x.down) (p : ↑unitInterval × ULift.{u, u_2} ↑S) : ↑((linearIsometryEquivPathHomotopy hS hγ hf₀ hf₁) p).down = (γ p.1) ↑p.2.down

The homotopy TauCeti.linearIsometryEquivPathHomotopy acts at time t by γ t.