Documentation

TauCeti.Geometry.Manifold.SmoothEmbedding.Cylinder

The ends of a cylinder #

For a manifold Y modelled on I, the cylinder Y ร— [a, b] is a manifold modelled on I.prod (๐“กโˆ‚ 1). This file packages its bottom and top slices y โ†ฆ (y, a) and y โ†ฆ (y, b) as bundled smooth embeddings, and identifies their underlying continuous maps with the slice homotopy equivalences Y โ‰ƒโ‚• Y ร— [a, b].

Main definitions #

Main results #

source
noncomputable def TauCeti.SmoothEmbedding.cylinderBot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners โ„ E H) (n : WithTop โ„•โˆž) (a b : โ„) [Fact (a < b)] (Y : Type u_3) [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] :
SmoothEmbedding I (I.prod (modelWithCornersEuclideanHalfSpace 1)) n Y (Y ร— โ†‘(Set.Icc a b))

The inclusion y โ†ฆ (y, a) of a manifold as the bottom end of the cylinder Y ร— [a, b].

Instances For
    source
    noncomputable def TauCeti.SmoothEmbedding.cylinderTop {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners โ„ E H) (n : WithTop โ„•โˆž) (a b : โ„) [Fact (a < b)] (Y : Type u_3) [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] :
    SmoothEmbedding I (I.prod (modelWithCornersEuclideanHalfSpace 1)) n Y (Y ร— โ†‘(Set.Icc a b))

    The inclusion y โ†ฆ (y, b) of a manifold as the top end of the cylinder Y ร— [a, b].

    Instances For
      source
      @[simp]
      theorem TauCeti.SmoothEmbedding.cylinderBot_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {n : WithTop โ„•โˆž} {a b : โ„} [Fact (a < b)] {Y : Type u_3} [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] (y : Y) :
      (cylinderBot I n a b Y) y = (y, โŠฅ)

      The bottom end of a cylinder sends y to (y, a).

      source
      @[simp]
      theorem TauCeti.SmoothEmbedding.cylinderTop_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {n : WithTop โ„•โˆž} {a b : โ„} [Fact (a < b)] {Y : Type u_3} [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] (y : Y) :
      (cylinderTop I n a b Y) y = (y, โŠค)

      The top end of a cylinder sends y to (y, b).

      source
      theorem TauCeti.SmoothEmbedding.toContinuousMap_cylinderBot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {n : WithTop โ„•โˆž} {a b : โ„} [Fact (a < b)] {Y : Type u_3} [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] :
      (cylinderBot I n a b Y).toContinuousMap = (ContinuousMap.HomotopyEquiv.prodIcc โŠฅ).toFun

      The bottom end of a cylinder is the slice homotopy equivalence Y โ‰ƒโ‚• Y ร— [a, b] at a.

      source
      theorem TauCeti.SmoothEmbedding.toContinuousMap_cylinderTop {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {n : WithTop โ„•โˆž} {a b : โ„} [Fact (a < b)] {Y : Type u_3} [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] :
      (cylinderTop I n a b Y).toContinuousMap = (ContinuousMap.HomotopyEquiv.prodIcc โŠค).toFun

      The top end of a cylinder is the slice homotopy equivalence Y โ‰ƒโ‚• Y ร— [a, b] at b.