LeanPool.WhiteheadTheorem.Shapes.Maps

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

theorem ContinuousMap.mulRight_one (X : Type u_1) [TopologicalSpace X] [mulOne : MulOneClass X] [ContinuousMul X] : ContinuousMap.mulRight 1 = ContinuousMap.id X

theorem ContinuousMap.mulRight_zero (X : Type u_1) [TopologicalSpace X] [mulOne : MulZeroClass X] [ContinuousMul X] : ContinuousMap.mulRight 0 = const X 0

theorem ContinuousMap.prodMap_id_id (X Y : Type u) [TopologicalSpace X] [TopologicalSpace Y] : (ContinuousMap.id X).prodMap (ContinuousMap.id Y) = ContinuousMap.id (X × Y)

@[reducible, inline]

abbrev TopCat.Cyl.i₀ (A : TopCat) : A ⟶ ↧(↑A × ↑unitInterval)

The inclusion map a ↦ ⟨a, 0⟩ from A to the cylinder whose base is A

Equations

• TopCat.Cyl.i₀ A = TopCat.ofHom { toFun := fun (a : ↑A) => (a, 0), continuous_toFun := ⋯ }

@[reducible, inline]

abbrev TopCat.Cyl.i₁ (A : TopCat) : A ⟶ ↧(↑A × ↑unitInterval)

The inclusion map a ↦ ⟨a, 1⟩ from A to the cylinder whose base is A

Equations

• TopCat.Cyl.i₁ A = TopCat.ofHom { toFun := fun (a : ↑A) => (a, 1), continuous_toFun := ⋯ }

@[reducible, inline]

abbrev TopCat.Cyl.r₀ (A : TopCat) : ↧(↑A × ↑unitInterval) ⟶ A

The retraction from a cylinder to its base

Equations

• TopCat.Cyl.r₀ A = TopCat.ofHom { toFun := fun (x : ↑A × ↑unitInterval) => match x with | (a, snd) => a, continuous_toFun := ⋯ }

@[simp]

theorem TopCat.Cyl.i₀_r₀_eq_id {A : TopCat} : CategoryTheory.CategoryStruct.comp (i₀ A) (r₀ A) = CategoryTheory.CategoryStruct.id A

@[simp]

theorem TopCat.Cyl.i₁_r₀_eq_id {A : TopCat} : CategoryTheory.CategoryStruct.comp (i₁ A) (r₀ A) = CategoryTheory.CategoryStruct.id A

theorem TopCat.Cyl.set_neq_zero_eq_compl_range_i₀ (X : TopCat) : {(fst, t) : ↑↧(↑X × ↑unitInterval) | t ≠ 0} = (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i₀ X)))ᶜ

def TopCat.Cyl.i₁ToComplRangeI₀ (X : TopCat) : C(↑X, ↑(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i₀ X))).compl)

i₁ToComplRangeI₀

Equations

• TopCat.Cyl.i₁ToComplRangeI₀ X = { toFun := fun (x : ↑X) => ⟨(CategoryTheory.ConcreteCategory.hom (TopCat.Cyl.i₁ X)) x, ⋯⟩, continuous_toFun := ⋯ }

theorem TopCat.Cyl.isClosed_range_i₀ (X : TopCat) : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i₀ X)))

theorem TopCat.Cyl.isClosedEmbedding_i₁ToComplRangeI₀ (X : TopCat) : Topology.IsClosedEmbedding ⇑(i₁ToComplRangeI₀ X)

@[instance_reducible]

noncomputable instance TopCat.Cyl.decidableInRangeI₀ {X : TopCat} (z : ↑↧(↑X × ↑unitInterval)) : Decidable (z ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i₀ X)))

used in isEmbedding_domIncl

Equations

• TopCat.Cyl.decidableInRangeI₀ z = ⋯.mpr inferInstance

@[reducible, inline]

abbrev TopCat.PathSpace.eval₀ (Y : TopCat) : ↧C(↑unitInterval, ↑Y) ⟶ Y

Given a path, return its source point (value at 0). The continuity of this function, through typeclass resolution, implicitly relies on the fact that I is locally compact.

Equations

• TopCat.PathSpace.eval₀ Y = TopCat.ofHom { toFun := fun (f : C(↑unitInterval, ↑Y)) => f 0, continuous_toFun := ⋯ }

@[reducible, inline]

abbrev TopCat.PathSpace.eval₁ (Y : TopCat) : ↧C(↑unitInterval, ↑Y) ⟶ Y

Given a path, return its target point (value at 1). The continuity of this function, through typeclass resolution, implicitly relies on the fact that I is locally compact.

Equations

• TopCat.PathSpace.eval₁ Y = TopCat.ofHom { toFun := fun (f : C(↑unitInterval, ↑Y)) => f 1, continuous_toFun := ⋯ }

@[reducible, inline]

abbrev TopCat.PathSpace.evalAt (Y : TopCat) (t : ↑unitInterval) : ↧C(↑unitInterval, ↑Y) ⟶ Y

evalAt

Equations

• TopCat.PathSpace.evalAt Y t = TopCat.ofHom { toFun := fun (f : C(↑unitInterval, ↑Y)) => f t, continuous_toFun := ⋯ }

@[reducible, inline]

abbrev TopCat.PathSpace.homToConstPaths {X Y : TopCat} (f : X ⟶ Y) : X ⟶ ↧C(↑unitInterval, ↑Y)

Given a morphism f : X ⟶ Y, return a morphism X ⟶ TopCat.of C(I, Y) that sends each point x : X to the constant path at f x : Y.

Equations

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