LeanPool.WhiteheadTheorem.Shapes.Jar

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

@[reducible, inline]

abbrev HEP.Jar (n : ℕ) : Type u_1

Jar

Equations

• HEP.Jar n = (↑(TopCat.disk n) × ↑unitInterval)

def HEP.Jar.mid (n : ℕ) : Set (Jar n)

mid

Equations

• HEP.Jar.mid n = {({ down := ⟨x, property⟩ }, ⟨y, property_1⟩) : HEP.Jar n | ‖x‖ ≤ 1 - y / 2}

def HEP.Jar.rim (n : ℕ) : Set (Jar n)

rim

Equations

• HEP.Jar.rim n = {({ down := ⟨x, property⟩ }, ⟨y, property_1⟩) : HEP.Jar n | ‖x‖ ≥ 1 - y / 2}

def HEP.Jar.closedCover (n : ℕ) : Fin 2 → Set (Jar n)

closedCover

Equations

• HEP.Jar.closedCover n = ![HEP.Jar.mid n, HEP.Jar.rim n]

theorem HEP.Jar.continuous_sub_div_two : Continuous fun (y : ℝ) => 1 - y / 2

theorem HEP.Jar.isClosed_mid (n : ℕ) : IsClosed (mid n)

theorem HEP.Jar.isClosed_rim (n : ℕ) : IsClosed (rim n)

noncomputable def HEP.Jar.midProjToFun (n : ℕ) : ↑(mid n) → ↑(TopCat.disk n)

midProjToFun

Equations

• HEP.Jar.midProjToFun n ⟨({ down := ⟨x, property⟩ }, ⟨y, property_1⟩), property_2⟩ = { down := ⟨(2 / (2 - y)) • x, ⋯⟩ }

theorem HEP.Jar.continuous_midProjToFun (n : ℕ) : Continuous (midProjToFun n)

noncomputable def HEP.Jar.midProj (n : ℕ) : C(↑(mid n), ↑(TopCat.disk n))

midProj

Equations

• HEP.Jar.midProj n = { toFun := HEP.Jar.midProjToFun n, continuous_toFun := ⋯ }

theorem HEP.Jar.rim_fst_ne_zero (n : ℕ) (p : ↑(rim n)) : ‖↑(↑p).1.down‖ ≠ 0

noncomputable def HEP.Jar.rimProjFstToFun (n : ℕ) : ↑(rim n) → ↑(TopCat.diskBoundary n)

rimProjFstToFun

Equations

• HEP.Jar.rimProjFstToFun n ⟨({ down := ⟨x, property⟩ }, snd), property_1⟩ = { down := ⟨(1 / ‖x‖) • x, ⋯⟩ }

theorem HEP.Jar.continuous_rimProjFstToFun (n : ℕ) : Continuous (rimProjFstToFun n)

noncomputable def HEP.Jar.rimProjFst (n : ℕ) : C(↑(rim n), ↑(TopCat.diskBoundary n))

rimProjFst

Equations

• HEP.Jar.rimProjFst n = { toFun := HEP.Jar.rimProjFstToFun n, continuous_toFun := ⋯ }

noncomputable def HEP.Jar.rimProjSndToFun (n : ℕ) : ↑(rim n) → ↑unitInterval

rimProjSndToFun

Equations

• HEP.Jar.rimProjSndToFun n ⟨({ down := ⟨x, property⟩ }, ⟨y, property_1⟩), property_2⟩ = ⟨(y - 2) / ‖x‖ + 2, ⋯⟩

theorem HEP.Jar.continuous_rimProjSndToFun (n : ℕ) : Continuous (rimProjSndToFun n)

noncomputable def HEP.Jar.rimProjSnd (n : ℕ) : C(↑(rim n), ↑unitInterval)

rimProjSnd

Equations

• HEP.Jar.rimProjSnd n = { toFun := HEP.Jar.rimProjSndToFun n, continuous_toFun := ⋯ }

noncomputable def HEP.Jar.rimProj (n : ℕ) : C(↑(rim n), ↑(TopCat.diskBoundary n) × ↑unitInterval)

rimProj

Equations

• HEP.Jar.rimProj n = (HEP.Jar.rimProjFst n).prodMk (HEP.Jar.rimProjSnd n)

noncomputable def HEP.Jar.proj (n : ℕ) {Y : Type u_1} [TopologicalSpace Y] (f : C(↑(TopCat.disk n), Y)) (H : C(↑(TopCat.diskBoundary n) × ↑unitInterval, Y)) (i : Fin 2) : C(↑(closedCover n i), Y)

proj

Equations

• HEP.Jar.proj n f H = Fin.cons (f.comp (HEP.Jar.midProj n)) (Fin.cons (H.comp (HEP.Jar.rimProj n)) finZeroElim)

theorem HEP.Jar.proj_compatible (n : ℕ) {Y : Type u_1} [TopologicalSpace Y] (f : C(↑(TopCat.disk n), Y)) (H : C(↑(TopCat.diskBoundary n) × ↑unitInterval, Y)) (hf : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n)) = ⇑H ∘ fun (x : ↑(TopCat.diskBoundary n)) => (x, 0)) (p : Jar n) (hp0 : p ∈ closedCover n 0) (hp1 : p ∈ closedCover n 1) : (proj n f H 0) ⟨p, hp0⟩ = (proj n f H 1) ⟨p, hp1⟩

theorem HEP.Jar.proj_compatible' (n : ℕ) {Y : Type u_1} [TopologicalSpace Y] (f : C(↑(TopCat.disk n), Y)) (H : C(↑(TopCat.diskBoundary n) × ↑unitInterval, Y)) (hf : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n)) = ⇑H ∘ fun (x : ↑(TopCat.diskBoundary n)) => (x, 0)) (i j : Fin 2) (p : Jar n) (hpi : p ∈ closedCover n i) (hpj : p ∈ closedCover n j) : (proj n f H i) ⟨p, hpi⟩ = (proj n f H j) ⟨p, hpj⟩

theorem HEP.Jar.closedCover_isCover (n : ℕ) (p : Jar n) : ∃ (i : Fin 2), p ∈ closedCover n i

theorem HEP.Jar.closedCover_isClosed (n : ℕ) (i : Fin 2) : IsClosed (closedCover n i)

noncomputable def HEP.Jar.homotopyExtension (n : ℕ) {Y : Type u_1} [TopologicalSpace Y] (f : C(↑(TopCat.disk n), Y)) (H : C(↑(TopCat.diskBoundary n) × ↑unitInterval, Y)) (hf : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n)) = ⇑H ∘ fun (x : ↑(TopCat.diskBoundary n)) => (x, 0)) : C(Jar n, Y)

homotopyExtension

Equations

• HEP.Jar.homotopyExtension n f H hf = ContinuousMap.liftCoverClosed (HEP.Jar.closedCover n) (HEP.Jar.proj n f H) ⋯ ⋯ ⋯

theorem HEP.Jar.homotopyExtension_bottom_commutes (n : ℕ) {Y : Type u_1} [TopologicalSpace Y] (f : C(↑(TopCat.disk n), Y)) (H : C(↑(TopCat.diskBoundary n) × ↑unitInterval, Y)) (hf : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n)) = ⇑H ∘ fun (x : ↑(TopCat.diskBoundary n)) => (x, 0)) : ⇑f = ⇑(homotopyExtension n f H hf) ∘ fun (x : ↑(TopCat.disk n)) => (x, 0)

theorem HEP.Jar.homotopyExtension_wall_commutes (n : ℕ) {Y : Type u_1} [TopologicalSpace Y] (f : C(↑(TopCat.disk n), Y)) (H : C(↑(TopCat.diskBoundary n) × ↑unitInterval, Y)) (hf : ⇑f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n)) = ⇑H ∘ fun (x : ↑(TopCat.diskBoundary n)) => (x, 0)) : ⇑H = ⇑(homotopyExtension n f H hf) ∘ Prod.map (⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n))) id