The mapping cylinder of a continuous map

The mapping cylinder of f : C(X, Y) is the cylinder I × X glued to Y by identifying the top face {1} × X with its image under f. It contains X as the bottom face {0} × X and Y as the glued base, it retracts onto Y by collapsing the cylinder along f, and the composite X → Mf → Y of the two structure maps is f itself.

Sliding every point of the cylinder to the top face deforms the mapping cylinder onto its base without moving the base, so the base inclusion is a homotopy equivalence. Together with the factorization this replaces an arbitrary continuous map, up to homotopy equivalence of its target, by the inclusion of a closed subspace; that inclusion is moreover a cofibration, which is proved in TauCeti.Topology.Homotopy.Extension.MappingCylinder.

The quotient is presented here as the quotient by the kernel of the normalization which replaces a point (1, x) of the top face by f x. That makes two points of I × X ⊕ Y identified exactly when the gluing forces it, which is what TauCeti.MappingCylinder.mkCyl_eq_mkCyl_iff and its companions record.

Main declarations

• TauCeti.MappingCylinder: the mapping cylinder, with its two structure maps TauCeti.MappingCylinder.mkCyl and TauCeti.MappingCylinder.mkBase and the presentation TauCeti.MappingCylinder.isQuotientMap_sumElim_mkCyl_mkBase of the underlying set as a quotient.
• TauCeti.MappingCylinder.lift: the universal property, together with TauCeti.MappingCylinder.ind and TauCeti.MappingCylinder.continuous_prod_iff, the continuity criterion for homotopies out of the mapping cylinder.
• TauCeti.MappingCylinder.incl and TauCeti.MappingCylinder.proj: the inclusion of the source and the projection onto the target, with TauCeti.MappingCylinder.proj_comp_incl the factorization of f and TauCeti.MappingCylinder.isClosedEmbedding_incl, TauCeti.MappingCylinder.isClosedEmbedding_mkBase the closedness of the two subspaces, and TauCeti.MappingCylinder.inclHomeomorph the homeomorphism of the source with the bottom face, through which TauCeti.MappingCylinder.proj_comp_subtypeVal_comp_inclHomeomorph factors f.
• TauCeti.MappingCylinder.deformation: the mapping cylinder deformation retracts onto its base, with TauCeti.MappingCylinder.homotopyEquiv the resulting homotopy equivalence with the target, and TauCeti.MappingCylinder.incl_homotopic_mkBase_comp the resulting homotopy from the bottom face inclusion to f followed by the base inclusion.
• TauCeti.MappingCylinder.exists_mem_range_incl_joined: when f is surjective on path components, every point of the mapping cylinder is joined by a path to the bottom face.

References

• A. Hatcher, Algebraic Topology, Chapter 0, the section "Mapping cylinders".
• G. W. Whitehead, Elements of Homotopy Theory, Chapter I.

def TauCeti.MappingCylinder {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : Type (max u v)

The mapping cylinder of f : C(X, Y): the cylinder I × X glued to Y along the map sending (1, x) to f x.

The presentation as a quotient is private to this file and is not part of the public interface: points of the mapping cylinder come from TauCeti.MappingCylinder.mkCyl and TauCeti.MappingCylinder.mkBase, which points they identify from TauCeti.MappingCylinder.mkCyl_eq_mkCyl_iff and its companions, maps out of it from TauCeti.MappingCylinder.lift, equalities of such maps from TauCeti.MappingCylinder.hom_ext, and statements about all of its points from TauCeti.MappingCylinder.ind.

The topology is transported from the private quotient; the instance is @[no_expose], which is what lets its body name the private constant.

@[instance_reducible]

instance TauCeti.MappingCylinder.instTopologicalSpace {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : TopologicalSpace (MappingCylinder f)

noncomputable def TauCeti.MappingCylinder.mkCyl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : C(↑unitInterval × X, MappingCylinder f)

The point of the mapping cylinder of f represented by a point of the cylinder I × X.

noncomputable def TauCeti.MappingCylinder.mkBase {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : C(Y, MappingCylinder f)

The point of the mapping cylinder of f represented by a point of the target Y.

@[simp]

theorem TauCeti.MappingCylinder.mkCyl_one {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (x : X) : (mkCyl f) (1, x) = (mkBase f) (f x)

The top face of the cylinder is glued to the base along f.

@[simp]

theorem TauCeti.MappingCylinder.mkCyl_eq_mkCyl_iff {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {s t : ↑unitInterval} {x y : X} : (mkCyl f) (s, x) = (mkCyl f) (t, y) ↔ s = t ∧ x = y ∨ s = 1 ∧ t = 1 ∧ f x = f y

Two points of the cylinder have the same image in the mapping cylinder exactly when they are equal, or both lie in the top face and have the same image under f.

@[simp]

theorem TauCeti.MappingCylinder.mkCyl_eq_mkBase_iff {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {s : ↑unitInterval} {x : X} {y : Y} : (mkCyl f) (s, x) = (mkBase f) y ↔ s = 1 ∧ f x = y

A point of the cylinder and a point of the target have the same image in the mapping cylinder exactly when the former lies in the top face and the gluing sends it to the latter.

@[simp]

theorem TauCeti.MappingCylinder.mkBase_inj {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {y z : Y} : (mkBase f) y = (mkBase f) z ↔ y = z

theorem TauCeti.MappingCylinder.mkBase_injective {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : Function.Injective ⇑(mkBase f)

theorem TauCeti.MappingCylinder.ind {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {p : MappingCylinder f → Prop} (cyl : ∀ (q : ↑unitInterval × X), p ((mkCyl f) q)) (base : ∀ (y : Y), p ((mkBase f) y)) (m : MappingCylinder f) : p m

Every point of the mapping cylinder comes from the cylinder or from the base.

theorem TauCeti.MappingCylinder.isQuotientMap_sumElim_mkCyl_mkBase {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : Topology.IsQuotientMap (Sum.elim ⇑(mkCyl f) ⇑(mkBase f))

The mapping cylinder is a quotient of I × X ⊕ Y.

theorem TauCeti.MappingCylinder.isClosed_of_preimages {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {S : Set (MappingCylinder f)} (hcyl : IsClosed (⇑(mkCyl f) ⁻¹' S)) (hbase : IsClosed (⇑(mkBase f) ⁻¹' S)) : IsClosed S

A subset of the mapping cylinder is closed as soon as its preimages in the cylinder and in the base are.

noncomputable def TauCeti.MappingCylinder.lift {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {W : Type w} [TopologicalSpace W] (g : C(↑unitInterval × X, W)) (h : C(Y, W)) (hgh : ∀ (x : X), g (1, x) = h (f x)) : C(MappingCylinder f, W)

The universal property of the mapping cylinder. A map on the cylinder and a map on the base which agree on the glued top face assemble into a map out of the mapping cylinder.

@[simp]

theorem TauCeti.MappingCylinder.lift_mkCyl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {W : Type w} [TopologicalSpace W] {g : C(↑unitInterval × X, W)} {h : C(Y, W)} (hgh : ∀ (x : X), g (1, x) = h (f x)) (p : ↑unitInterval × X) : (lift g h hgh) ((mkCyl f) p) = g p

@[simp]

theorem TauCeti.MappingCylinder.lift_mkBase {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {W : Type w} [TopologicalSpace W] {g : C(↑unitInterval × X, W)} {h : C(Y, W)} (hgh : ∀ (x : X), g (1, x) = h (f x)) (y : Y) : (lift g h hgh) ((mkBase f) y) = h y

theorem TauCeti.MappingCylinder.hom_ext {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {W : Type w} [TopologicalSpace W] {F G : C(MappingCylinder f, W)} (cyl : ∀ (p : ↑unitInterval × X), F ((mkCyl f) p) = G ((mkCyl f) p)) (base : ∀ (y : Y), F ((mkBase f) y) = G ((mkBase f) y)) : F = G

Extensionality for maps out of the mapping cylinder. Two continuous maps out of the mapping cylinder which agree on the cylinder and on the base are equal.

theorem TauCeti.MappingCylinder.hom_ext_iff {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {W : Type w} [TopologicalSpace W] {F G : C(MappingCylinder f, W)} : F = G ↔ (∀ (p : ↑unitInterval × X), F ((mkCyl f) p) = G ((mkCyl f) p)) ∧ ∀ (y : Y), F ((mkBase f) y) = G ((mkBase f) y)

theorem TauCeti.MappingCylinder.lift_unique {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {W : Type w} [TopologicalSpace W] {g : C(↑unitInterval × X, W)} {h : C(Y, W)} (hgh : ∀ (x : X), g (1, x) = h (f x)) {F : C(MappingCylinder f, W)} (hcyl : ∀ (p : ↑unitInterval × X), F ((mkCyl f) p) = g p) (hbase : ∀ (y : Y), F ((mkBase f) y) = h y) : F = lift g h hgh

Uniqueness in the universal property of the mapping cylinder. A map out of the mapping cylinder is determined by its restrictions to the cylinder and to the base.

theorem TauCeti.MappingCylinder.continuous_prod_iff {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {Z : Type u_1} {W : Type u_2} [TopologicalSpace Z] [LocallyCompactSpace Z] [TopologicalSpace W] {g : Z × MappingCylinder f → W} : Continuous g ↔ (Continuous fun (q : Z × ↑unitInterval × X) => g (q.1, (mkCyl f) q.2)) ∧ Continuous fun (q : Z × Y) => g (q.1, (mkBase f) q.2)

Continuity criterion for maps out of Z × Mf. For a locally compact space Z, a map out of the product of Z with the mapping cylinder is continuous exactly when it is continuous on Z × (I × X) and on Z × Y. For Z = I this builds homotopies out of the mapping cylinder.

noncomputable def TauCeti.MappingCylinder.incl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : C(X, MappingCylinder f)

The inclusion of the source of f into its mapping cylinder as the bottom face of the cylinder.

noncomputable def TauCeti.MappingCylinder.proj {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : C(MappingCylinder f, Y)

The projection of the mapping cylinder of f onto its target: the cylinder is collapsed along f.

@[simp]

theorem TauCeti.MappingCylinder.incl_apply {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (x : X) : (incl f) x = (mkCyl f) (0, x)

@[simp]

theorem TauCeti.MappingCylinder.proj_mkCyl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (p : ↑unitInterval × X) : (proj f) ((mkCyl f) p) = f p.2

@[simp]

theorem TauCeti.MappingCylinder.proj_mkBase {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (y : Y) : (proj f) ((mkBase f) y) = y

@[simp]

theorem TauCeti.MappingCylinder.proj_comp_mkBase {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : (proj f).comp (mkBase f) = ContinuousMap.id Y

@[simp]

theorem TauCeti.MappingCylinder.proj_comp_incl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : (proj f).comp (incl f) = f

The mapping cylinder factors f as its inclusion into the cylinder followed by the projection onto the target.

theorem TauCeti.MappingCylinder.mkCyl_mem_range_incl_iff {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} {s : ↑unitInterval} {x : X} : (mkCyl f) (s, x) ∈ Set.range ⇑(incl f) ↔ s = 0

A point of the cylinder lies in the bottom face exactly when its image in the mapping cylinder lies in the image of the source.

theorem TauCeti.MappingCylinder.mkBase_notMem_range_incl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (y : Y) : (mkBase f) y ∉ Set.range ⇑(incl f)

No point of the base of the mapping cylinder comes from the source.

theorem TauCeti.MappingCylinder.isClosed_range_incl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : IsClosed (Set.range ⇑(incl f))

The image of the source of f in the mapping cylinder is closed.

theorem TauCeti.MappingCylinder.isClosedEmbedding_incl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : Topology.IsClosedEmbedding ⇑(incl f)

The source of f is a closed subspace of its mapping cylinder.

noncomputable def TauCeti.MappingCylinder.inclHomeomorph {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : X ≃ₜ ↑(Set.range ⇑(incl f))

The source of f is homeomorphic to the bottom face range (incl f) of its mapping cylinder.

@[simp]

theorem TauCeti.MappingCylinder.inclHomeomorph_apply_coe {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (x : X) : ↑((inclHomeomorph f) x) = (incl f) x

@[simp]

theorem TauCeti.MappingCylinder.proj_comp_subtypeVal_comp_inclHomeomorph {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : (proj f).comp ((ContinuousMap.subtypeVal (Set.range ⇑(incl f))).comp ↑(inclHomeomorph f)) = f

f factors as the homeomorphism of its source with the bottom face of the mapping cylinder, followed by the inclusion of the bottom face and the projection onto the target.

theorem TauCeti.MappingCylinder.isClosedEmbedding_mkBase {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : Topology.IsClosedEmbedding ⇑(mkBase f)

The target of f is a closed subspace of its mapping cylinder.

noncomputable def TauCeti.MappingCylinder.deformation {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : (ContinuousMap.id (MappingCylinder f)).HomotopyRel ((mkBase f).comp (proj f)) (Set.range ⇑(mkBase f))

The mapping cylinder deformation retracts onto its base. Sliding every point of the cylinder to the top face is a homotopy from the identity of the mapping cylinder to the projection followed by the base inclusion, and it does not move the base.

noncomputable def TauCeti.MappingCylinder.homotopyEquiv {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) : ContinuousMap.HomotopyEquiv (MappingCylinder f) Y

The mapping cylinder of f is homotopy equivalent to the target of f, by the projection and the base inclusion.

@[simp]

theorem TauCeti.MappingCylinder.homotopyEquiv_apply {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (m : MappingCylinder f) : (homotopyEquiv f).toFun m = (proj f) m

The homotopy equivalence with the target is the projection.

theorem TauCeti.MappingCylinder.homotopyEquiv_toFun {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : (homotopyEquiv f).toFun = proj f

The forward map of the homotopy equivalence with the target is the projection.

@[simp]

theorem TauCeti.MappingCylinder.homotopyEquiv_symm_apply {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (y : Y) : (homotopyEquiv f).symm.toFun y = (mkBase f) y

The homotopy inverse of the projection is the base inclusion.

theorem TauCeti.MappingCylinder.incl_homotopic_mkBase_comp {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : (incl f).Homotopic ((mkBase f).comp f)

The inclusion of the bottom face is homotopic to f followed by the base inclusion: follow the deformation onto the base.

theorem TauCeti.MappingCylinder.joined_mkBase_proj {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (m : MappingCylinder f) : Joined m ((mkBase f) ((proj f) m))

Every point of the mapping cylinder is joined by a path to the point of the base below it: follow the deformation onto the base.

theorem TauCeti.MappingCylinder.exists_mem_range_incl_joined {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} (h : ∀ (y : Y), ∃ (x : X), Joined (f x) y) (m : MappingCylinder f) : ∃ b ∈ Set.range ⇑(incl f), Joined m b

If every point of Y is joined by a path to a point of the image of f, then every point of the mapping cylinder is joined by a path to a point of the bottom face.