LeanPool.WhiteheadTheorem.Shapes.MappingCylinder

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Shapes.MappingCylinder.

noncomputable def TopCat.MapCyl {X Y : TopCat} (f : X ⟶ Y) : TopCat

The mapping cylinder of a continuous map f : X ⟶ Y.

Equations

• TopCat.MapCyl f = CategoryTheory.Limits.pushout f (TopCat.Cyl.i₀ X)

@[reducible, inline]

noncomputable abbrev TopCat.MapCyl.inl {X Y : TopCat} (f : X ⟶ Y) : Y ⟶ MapCyl f

inl

Equations

• TopCat.MapCyl.inl f = CategoryTheory.Limits.pushout.inl f (TopCat.Cyl.i₀ X)

@[reducible, inline]

noncomputable abbrev TopCat.MapCyl.inr {X Y : TopCat} (f : X ⟶ Y) : of (↑X × ↑unitInterval) ⟶ MapCyl f

inr

Equations

• TopCat.MapCyl.inr f = CategoryTheory.Limits.pushout.inr f (TopCat.Cyl.i₀ X)

theorem TopCat.MapCyl.condition {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (inl f) = CategoryTheory.CategoryStruct.comp (Cyl.i₀ X) (inr f)

condition

@[reducible, inline]

noncomputable abbrev TopCat.MapCyl.domIncl {X Y : TopCat} (f : X ⟶ Y) : X ⟶ MapCyl f

Inclusion map from the domain X to the mapping cylinder of f : X ⟶ Y

Equations

• TopCat.MapCyl.domIncl f = CategoryTheory.CategoryStruct.comp (TopCat.Cyl.i₁ X) (TopCat.MapCyl.inr f)

def TopCat.MapCyl.codIncl {X Y : TopCat} (f : X ⟶ Y) : Y ⟶ MapCyl f

Inclusion map from the codomain Y to the mapping cylinder of f : X ⟶ Y

Equations

• @TopCat.MapCyl.codIncl = @TopCat.MapCyl.inl

@[reducible, inline]

abbrev TopCat.MapCyl.top {X Y : TopCat} (f : X ⟶ Y) : Set ↑(MapCyl f)

The top surface of the mapping cylinder

Equations

• TopCat.MapCyl.top f = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.MapCyl.domIncl f))

theorem TopCat.MapCyl.domIncl_hom_eq_pushoutInr'_comp {X Y : TopCat} (f : X ⟶ Y) : Hom.hom (domIncl f) = (pushoutInr' f (Cyl.i₀ X)).comp (Cyl.i₁ToComplRangeI₀ X)

theorem TopCat.MapCyl.isEmbedding_domIncl {X Y : TopCat} (f : X ⟶ Y) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (domIncl f))

noncomputable def TopCat.MapCyl.domHomeoTop {X Y : TopCat} (f : X ⟶ Y) : ↑X ≃ₜ ↑(top f)

The domain X of a continuous map f is homeomorphic to the top surface of the mapping cylinder of f.

Equations

• TopCat.MapCyl.domHomeoTop f = ⋯.toHomeomorph

noncomputable def TopCat.MapCyl.domInclToTop {X Y : TopCat} (f : X ⟶ Y) : C(↑X, ↑(top f))

domInclToTop

Equations

• TopCat.MapCyl.domInclToTop f = ↑(TopCat.MapCyl.domHomeoTop f)

def TopCat.MapCyl.domInclFromTop {X Y : TopCat} (f : X ⟶ Y) : C(↑(top f), ↑(MapCyl f))

domInclFromTop

Equations

• TopCat.MapCyl.domInclFromTop f = { toFun := Subtype.val, continuous_toFun := ⋯ }

theorem TopCat.MapCyl.domIncl_hom_eq_domInclFromTop_comp_domInclToTop {X Y : TopCat} (f : X ⟶ Y) : Hom.hom (domIncl f) = (domInclFromTop f).comp (domInclToTop f)

theorem TopCat.MapCyl.domIncl_toFun_eq_domInclFromTop_comp_domInclToTop {X Y : TopCat} (f : X ⟶ Y) : (Hom.hom (domIncl f)).toFun = ⇑(domInclFromTop f) ∘ ⇑(domInclToTop f)

theorem TopCat.MapCyl.isHomeomorph_domInclToTop {X Y : TopCat} (f : X ⟶ Y) : IsHomeomorph ⇑(domInclToTop f)

noncomputable def TopCat.MapCyl.retr {X Y : TopCat} (f : X ⟶ Y) : MapCyl f ⟶ Y

The retraction from a mapping cylinder of f : X ⟶ Y to its base Y

Equations

• TopCat.MapCyl.retr f = CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.comp (TopCat.Cyl.r₀ X) f) ⋯

theorem TopCat.MapCyl.domIncl_retr_eq {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (domIncl f) (retr f) = f

theorem TopCat.MapCyl.domIncl_retr_eq_assoc {X Y : TopCat} (f : X ⟶ Y) {a✝ : TopCat} {h : Y ⟶ a✝} : CategoryTheory.CategoryStruct.comp (domIncl f) (CategoryTheory.CategoryStruct.comp (retr f) h) = CategoryTheory.CategoryStruct.comp f h

theorem TopCat.MapCyl.inl_retr_eq_id {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (inl f) (retr f) = CategoryTheory.CategoryStruct.id Y

theorem TopCat.MapCyl.codIncl_retr_eq_id {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (codIncl f) (retr f) = CategoryTheory.CategoryStruct.id Y

noncomputable def TopCat.MapCyl.curriedDeformRetr {X Y : TopCat} (f : X ⟶ Y) : MapCyl f ⟶ of C(↑unitInterval, ↑(MapCyl f))

The curried form of the deformation retraction from a mapping cylinder of f : X ⟶ Y to its base Y. This is a curried homotopy from retr f ≫ inl f (when t = 0) to 𝟙 (MapCyl f) (when t = 1). The curried form facilitates the proof of continuity (see MapCyl.equivBase.left_inv), and is equal to uncurried form when evaluated at any t : I (see curriedDeformRetrEvalAt_eq_deformRetrEvalAt).

Note: s * t uses the instance unitInterval.continuousMul in Shapes/Maps.lean.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TopCat.MapCyl.curriedDeformRetrEvalAt {X Y : TopCat} (f : X ⟶ Y) (t : ↑unitInterval) : MapCyl f ⟶ MapCyl f

curriedDeformRetrEvalAt

Equations

• TopCat.MapCyl.curriedDeformRetrEvalAt f t = TopCat.ofHom ((TopCat.Hom.hom (TopCat.MapCyl.curriedDeformRetr f)).uncurry.curryLeft t)

theorem TopCat.MapCyl.curriedDeformRetrEvalAt_hom_apply {X Y : TopCat} (f : X ⟶ Y) (t : ↑unitInterval) (z : ↑(MapCyl f)) : (Hom.hom (curriedDeformRetrEvalAt f t)) z = ((Hom.hom (curriedDeformRetr f)) z) t

noncomputable def TopCat.MapCyl.deformRetrEvalAt {X Y : TopCat} (f : X ⟶ Y) (t : ↑unitInterval) : MapCyl f ⟶ MapCyl f

The homotopy (deformation retraction) from retr f ≫ inl f (when t = 0) to 𝟙 (MapCyl f) (when t = 1), evaluated at t.

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.MapCyl.deformRetrEvalAt_zero {X Y : TopCat} (f : X ⟶ Y) : deformRetrEvalAt f 0 = CategoryTheory.CategoryStruct.comp (retr f) (inl f)

theorem TopCat.MapCyl.deformRetrEvalAt_one {X Y : TopCat} (f : X ⟶ Y) : deformRetrEvalAt f 1 = CategoryTheory.CategoryStruct.id (MapCyl f)

theorem TopCat.MapCyl.curriedDeformRetrEvalAt_eq_deformRetrEvalAt {X Y : TopCat} (f : X ⟶ Y) (t : ↑unitInterval) : curriedDeformRetrEvalAt f t = deformRetrEvalAt f t

noncomputable def TopCat.MapCyl.homotopyEquivBase {X Y : TopCat} (f : X ⟶ Y) : ContinuousMap.HomotopyEquiv ↑(MapCyl f) ↑Y

The mapping cylinder of f : X ⟶ Y is homotopy equivalent to its base Y.

Equations

• TopCat.MapCyl.homotopyEquivBase f = { toFun := TopCat.Hom.hom (TopCat.MapCyl.retr f), invFun := TopCat.Hom.hom (TopCat.MapCyl.inl f), left_inv := ⋯, right_inv := ⋯ }

TODO: Show inl f is a topological embedding using inl f ≫ retr f = 𝟙 Y, i.e., using homotopyEquivBase.right_inv.

theorem TopCat.MapCyl.isHomotopyEquiv_retr {X Y : TopCat} (f : X ⟶ Y) : IsHomotopyEquiv (Hom.hom (retr f))