Attaching families of cells over a parameter space

Let A be a subspace of a space Y, and let α i : P × ∂D^{k i} → A be continuous families of attaching maps, parametrized by a space P. Attaching, over each p ∈ P, one disc D^{k i} along each α i p gives the fiberwise adjunction space

(P × A) ∪_α ⨆ᵢ (P × D^{k i}),

the pushout in TopCat of (p, s) ↦ (p, α i (p, s)) along the inclusions P × ∂D^{k i} → P × D^{k i} (TauCeti.fiberwiseCellAttachment). It lies over P (TauCeti.fiberwiseCellAttachmentProj), and its points over p are those of the attachment A ∪_{α p} ⨆ᵢ D^{k i}. Characteristic families χ i : P × D^{k i} → Y restricting to α i on the boundary spheres induce the comparison map (P × A) ∪_α ⨆ᵢ (P × D^{k i}) → P × Y over P (TauCeti.fiberwiseCellComparison). These are the families of cell attachments met when the charts of a Morse function at a critical level vary continuously with a parameter.

Two families χ₀ and χ₁ of characteristic maps are compared as in Milnor's Lemma 3.6, now over P. Given self-maps h i of P × D^{k i} over P preserving P × ∂D^{k i}, and homotopies K i : χ₁ i ≃ χ₀ i ∘ (p, h i) keeping P × ∂D^{k i} in A, the fiberwise reattachment map (TauCeti.fiberwiseCellReattachment)

E : (P × A) ∪_{α₁} ⨆ᵢ (P × D^{k i}) → (P × A) ∪_{α₀} ⨆ᵢ (P × D^{k i})

is the identity on P × A, sends (p, x) in the i-th disc with ‖x‖ ≤ 1/2 to the point (p, h i (p, 2x)) of the i-th disc, and sends (p, x) with 1/2 ≤ ‖x‖ to the point (p, K i (2 - 2‖x‖, (p, x/‖x‖))) of P × A. It lies over P, and Φ₀ ∘ E is homotopic to Φ₁ relative to P × A through maps over P (TauCeti.fiberwiseCellReattachmentHomotopy), for the comparison maps Φ₀ and Φ₁.

All of these constructions are natural in the parameter space: along a continuous map g : P' → P, the attachments of the restricted families map to the original ones over g (TauCeti.fiberwiseCellAttachmentMap), compatibly with the comparison maps and with the reattachment maps (TauCeti.fiberwiseCellReattachment_comp_fiberwiseCellAttachmentMap) and with the homotopies (TauCeti.fiberwiseCellReattachmentHomotopy_fiberwiseCellAttachmentMap). In particular, for the inclusion of a subspace P' ⊆ P, restricting the data to P' gives the same construction over P'.

References

• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Lemma 3.6 and Remark 3.3.

noncomputable def TauCeti.fiberwiseAttachingMap {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) : (∐ fun (i : ι) => ↧(P × ↑(TopCat.diskBoundary (k i)))) ⟶ ↧(P × ↑A)

The coproduct of the maps (p, s) ↦ (p, α i (p, s)) from P × ∂D^{k i} to P × A.

noncomputable def TauCeti.fiberwiseBoundaryInclusion (P : Type u) [TopologicalSpace P] {ι : Type u} (k : ι → ℕ) : (∐ fun (i : ι) => ↧(P × ↑(TopCat.diskBoundary (k i)))) ⟶ ∐ fun (i : ι) => ↧(P × ↑(TopCat.disk (k i)))

The coproduct of the inclusions P × ∂D^{k i} → P × D^{k i}.

noncomputable def TauCeti.fiberwiseCellAttachment {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) : TopCat

The fiberwise adjunction space (P × A) ∪_α ⨆ᵢ (P × D^{k i}) of a family of attaching maps α i : P × ∂D^{k i} → A: over each p, one disc D^{k i} is attached to A along each α i (p, ·). It is the pushout in TopCat of TauCeti.fiberwiseAttachingMap α along TauCeti.fiberwiseBoundaryInclusion (TauCeti.isPushout_fiberwiseCellAttachment).

noncomputable def TauCeti.fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) : ↧(P × ↑A) ⟶ fiberwiseCellAttachment α

The inclusion of P × A into the fiberwise adjunction space.

noncomputable def TauCeti.fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (i : ι) : ↧(P × ↑(TopCat.disk (k i))) ⟶ fiberwiseCellAttachment α

The family over P of characteristic maps P × D^{k i} → (P × A) ∪_α ⨆ᵢ (P × D^{k i}) of the cells attached along α i.

theorem TauCeti.isPushout_fiberwiseCellAttachment {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) : CategoryTheory.IsPushout (fiberwiseAttachingMap α) (fiberwiseBoundaryInclusion P k) (fiberwiseCellAttachmentIncl α) (CategoryTheory.Limits.Sigma.desc (fiberwiseCellAttachmentCell α))

The fiberwise adjunction space is the pushout of the attaching maps along the boundary inclusions, with the inclusion of P × A and the characteristic maps of the cells as its legs.

@[simp]

theorem TauCeti.fiberwiseAttachingMap_ι {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (i : ι) (x : P × ↑(TopCat.diskBoundary (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseAttachingMap α)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => ↧(P × ↑(TopCat.diskBoundary (k i)))) i)) x) = (x.1, (α i) x)

On the i-th summand, the coproduct of the attaching maps is (p, s) ↦ (p, α i (p, s)).

@[simp]

theorem TauCeti.fiberwiseBoundaryInclusion_ι {P : Type u} [TopologicalSpace P] {ι : Type u} {k : ι → ℕ} (i : ι) (x : P × ↑(TopCat.diskBoundary (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseBoundaryInclusion P k)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => ↧(P × ↑(TopCat.diskBoundary (k i)))) i)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => ↧(P × ↑(TopCat.disk (k i)))) i)) (x.1, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) x.2)

On the i-th summand, the coproduct of the boundary inclusions is the inclusion P × ∂D^{k i} → P × D^{k i}.

theorem TauCeti.fiberwiseCellAttachmentCell_diskBoundaryInclusion {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) (p, (α i) (p, s))

On the boundary spheres, the characteristic maps of the cells are the attaching maps followed by the inclusion of P × A.

noncomputable def TauCeti.fiberwiseCellAttachmentDesc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) : fiberwiseCellAttachment α ⟶ Z

A map on P × A and maps on the families of discs which agree along the attaching maps induce a map out of the fiberwise adjunction space.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentIncl_desc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) : CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentIncl α) (fiberwiseCellAttachmentDesc α g G hG) = g

@[simp]

theorem TauCeti.fiberwiseCellAttachmentIncl_desc_assoc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) {Z✝ : TopCat} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentIncl α) (CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentDesc α g G hG) h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem TauCeti.fiberwiseCellAttachmentCell_desc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) (i : ι) : CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentCell α i) (fiberwiseCellAttachmentDesc α g G hG) = G i

@[simp]

theorem TauCeti.fiberwiseCellAttachmentCell_desc_assoc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) (i : ι) {Z✝ : TopCat} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentCell α i) (CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentDesc α g G hG) h) = CategoryTheory.CategoryStruct.comp (G i) h

@[simp]

theorem TauCeti.fiberwiseCellAttachmentDesc_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) (x : P × ↑A) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentDesc α g G hG)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x) = (CategoryTheory.ConcreteCategory.hom g) x

@[simp]

theorem TauCeti.fiberwiseCellAttachmentDesc_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} (g : ↧(P × ↑A) ⟶ Z) (G : (i : ι) → ↧(P × ↑(TopCat.disk (k i))) ⟶ Z) (hG : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (CategoryTheory.ConcreteCategory.hom (G i)) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = (CategoryTheory.ConcreteCategory.hom g) (p, (α i) (p, s))) (i : ι) (x : P × ↑(TopCat.disk (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentDesc α g G hG)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x) = (CategoryTheory.ConcreteCategory.hom (G i)) x

theorem TauCeti.fiberwiseCellAttachment_continuousMap_ext {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {W : Type u} [TopologicalSpace W] {g g' : C(↑(fiberwiseCellAttachment α), W)} (h₀ : ∀ (x : ↑↧(P × ↑A)), g ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x) = g' ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x)) (h : ∀ (i : ι) (x : ↑↧(P × ↑(TopCat.disk (k i)))), g ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x) = g' ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x)) : g = g'

Continuous maps out of the fiberwise adjunction space agree as soon as they agree on P × A and on the cells.

theorem TauCeti.fiberwiseCellAttachment_hom_ext {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {Z : TopCat} {g g' : fiberwiseCellAttachment α ⟶ Z} (h₀ : ∀ (x : ↑↧(P × ↑A)), (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x) = (CategoryTheory.ConcreteCategory.hom g') ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x)) (h : ∀ (i : ι) (x : ↑↧(P × ↑(TopCat.disk (k i)))), (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x) = (CategoryTheory.ConcreteCategory.hom g') ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x)) : g = g'

Maps out of the fiberwise adjunction space are determined by their restrictions to P × A and to the cells.

theorem TauCeti.range_fiberwiseCellAttachmentIncl_union_iUnion_range_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) ∪ ⋃ (i : ι), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) = Set.univ

Every point of the fiberwise adjunction space lies in P × A or in a cell.

noncomputable def TauCeti.fiberwiseCellAttachmentCylinderDesc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {W : Type u} [TopologicalSpace W] (L : C(↑unitInterval × P × ↑A, W)) (C : (i : ι) → C(↑unitInterval × P × ↑(TopCat.disk (k i)), W)) (hC : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (C i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = L (t, p, (α i) (p, s))) : C(↑unitInterval × ↑(fiberwiseCellAttachment α), W)

The map I × ((P × A) ∪_α ⨆ᵢ (P × D^{k i})) → W glued from L : I × (P × A) → W and maps C i : I × (P × D^{k i}) → W that agree along the attaching maps: the form of TauCeti.fiberwiseCellAttachmentDesc for homotopies out of the fiberwise adjunction space.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentCylinderDesc_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {W : Type u} [TopologicalSpace W] (L : C(↑unitInterval × P × ↑A, W)) (C : (i : ι) → C(↑unitInterval × P × ↑(TopCat.disk (k i)), W)) (hC : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (C i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = L (t, p, (α i) (p, s))) (t : ↑unitInterval) (x : P × ↑A) : (fiberwiseCellAttachmentCylinderDesc α L C hC) (t, (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x) = L (t, x)

@[simp]

theorem TauCeti.fiberwiseCellAttachmentCylinderDesc_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {W : Type u} [TopologicalSpace W] (L : C(↑unitInterval × P × ↑A, W)) (C : (i : ι) → C(↑unitInterval × P × ↑(TopCat.disk (k i)), W)) (hC : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (C i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = L (t, p, (α i) (p, s))) (t : ↑unitInterval) (i : ι) (x : P × ↑(TopCat.disk (k i))) : (fiberwiseCellAttachmentCylinderDesc α L C hC) (t, (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x) = (C i) (t, x)

noncomputable def TauCeti.fiberwiseCellAttachmentProj {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) : fiberwiseCellAttachment α ⟶ ↧P

The projection of the fiberwise adjunction space (P × A) ∪_α ⨆ᵢ (P × D^{k i}) to the parameter space P.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentProj_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (x : P × ↑A) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x) = x.1

@[simp]

theorem TauCeti.fiberwiseCellAttachmentProj_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (i : ι) (x : P × ↑(TopCat.disk (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x) = x.1

theorem TauCeti.fiberwiseCellAttachment_induction {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) {motive : ↑(fiberwiseCellAttachment α) → Prop} (h₀ : ∀ (x : P × ↑A), motive ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x)) (h : ∀ (i : ι) (x : P × ↑(TopCat.disk (k i))), motive ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x)) (y : ↑(fiberwiseCellAttachment α)) : motive y

A property of the points of the fiberwise adjunction space holds as soon as it holds at the points of P × A and of the cells.

noncomputable def TauCeti.fiberwiseCellComparison {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α i) (p, s))) : fiberwiseCellAttachment α ⟶ ↧(P × Y)

The comparison map (P × A) ∪_α ⨆ᵢ (P × D^{k i}) → P × Y over P of a family of characteristic maps χ i : P × D^{k i} → Y restricting to the attaching maps α i on the boundary spheres: it is the inclusion on P × A and (p, x) ↦ (p, χ i (p, x)) on the i-th cell.

@[simp]

theorem TauCeti.fiberwiseCellComparison_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α i) (p, s))) (x : P × ↑A) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellComparison α χ hχ)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) x) = (x.1, ↑x.2)

@[simp]

theorem TauCeti.fiberwiseCellComparison_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α i) (p, s))) (i : ι) (x : P × ↑(TopCat.disk (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellComparison α χ hχ)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) x) = (x.1, (χ i) x)

@[simp]

theorem TauCeti.fst_fiberwiseCellComparison {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α i) (p, s))) (y : ↑(fiberwiseCellAttachment α)) : ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellComparison α χ hχ)) y).1 = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α)) y

The comparison map lies over P.

noncomputable def TauCeti.fiberwiseCellReattachment {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) : fiberwiseCellAttachment α₁ ⟶ fiberwiseCellAttachment α₀

The fiberwise reattachment map E : (P × A) ∪_{α₁} ⨆ᵢ (P × D^{k i}) → (P × A) ∪_{α₀} ⨆ᵢ (P × D^{k i}) of a family over P of self-maps h i of the disc pairs (D^{k i}, ∂D^{k i}) and of homotopies K i : χ₁ i ≃ χ₀ i ∘ (p, h i) of families of characteristic maps keeping the boundary spheres in A. It is the identity on P × A; on the i-th family of discs it sends (p, x) to the point (p, h i (p, 2x)) of the i-th cell when ‖x‖ ≤ 1/2, and to the point (p, K i (2 - 2‖x‖, (p, x/‖x‖))) of P × A when 1/2 ≤ ‖x‖.

@[simp]

theorem TauCeti.fiberwiseCellReattachment_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (x : P × ↑A) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellReattachment α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α₁)) x) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α₀)) x

The fiberwise reattachment map is the identity on P × A.

theorem TauCeti.fiberwiseCellReattachment_fiberwiseCellAttachmentCell_of_norm_le {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (i : ι) (p : P) {w v : ↑(TopCat.disk (k i))} (hw : ‖↑w.down‖ ≤ 1 / 2) (hv : ↑v.down = 2 • ↑w.down) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellReattachment α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α₁ i)) (p, w)) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α₀ i)) (p, (h i) (p, v))

On the disc of radius 1/2 of the i-th cell over p, the fiberwise reattachment map is x ↦ h i (p, 2x), read in the i-th cell over p.

theorem TauCeti.fiberwiseCellReattachment_fiberwiseCellAttachmentCell_of_le_norm {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (i : ι) (p : P) {w : ↑(TopCat.disk (k i))} (hw : 1 / 2 ≤ ‖↑w.down‖) {t : ↑unitInterval} (ht : ↑t = 2 - 2 * ‖↑w.down‖) {s : ↑(TopCat.diskBoundary (k i))} (hs : ↑s.down = ‖↑w.down‖⁻¹ • ↑w.down) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellReattachment α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α₁ i)) (p, w)) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α₀)) (p, ⟨(K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s), ⋯⟩)

Outside the disc of radius 1/2 of the i-th cell over p, the fiberwise reattachment map is x ↦ K i (2 - 2‖x‖, (p, x/‖x‖)), read in P × A.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentProj_fiberwiseCellReattachment {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (y : ↑(fiberwiseCellAttachment α₁)) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α₀)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellReattachment α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK)) y) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α₁)) y

The fiberwise reattachment map lies over P.

noncomputable def TauCeti.fiberwiseCellReattachmentHomotopy {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) : (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (fiberwiseCellReattachment α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK) (fiberwiseCellComparison α₀ χ₀ hχ₀))).HomotopyRel (TopCat.Hom.hom (fiberwiseCellComparison α₁ χ₁ hχ₁)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α₁)))

Φ₀ ∘ E is homotopic to Φ₁ over P, relative to P × A. The homotopy from the fiberwise reattachment map followed by the comparison map Φ₀ to the comparison map Φ₁. It fixes the points of P × A, lies over P at all times (TauCeti.fst_fiberwiseCellReattachmentHomotopy), and on the i-th cell it is K i read along the straight-line homotopy TauCeti.TopCat.reattachmentPath in the cylinder I × D^{k i}.

@[simp]

theorem TauCeti.fiberwiseCellReattachmentHomotopy_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (t : ↑unitInterval) (x : P × ↑A) : (fiberwiseCellReattachmentHomotopy α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK) (t, (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α₁)) x) = (x.1, ↑x.2)

@[simp]

theorem TauCeti.fiberwiseCellReattachmentHomotopy_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (t : ↑unitInterval) (i : ι) (x : P × ↑(TopCat.disk (k i))) : (fiberwiseCellReattachmentHomotopy α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK) (t, (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α₁ i)) x) = (x.1, (K i) ((TopCat.reattachmentPath (x.2, t)).1, x.1, (TopCat.reattachmentPath (x.2, t)).2))

@[simp]

theorem TauCeti.fst_fiberwiseCellReattachmentHomotopy {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (t : ↑unitInterval) (y : ↑(fiberwiseCellAttachment α₁)) : ((fiberwiseCellReattachmentHomotopy α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK) (t, y)).1 = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α₁)) y

The homotopy from Φ₀ ∘ E to Φ₁ lies over P at all times.

noncomputable def TauCeti.fiberwiseCellAttachmentMap {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) : fiberwiseCellAttachment α' ⟶ fiberwiseCellAttachment α

The map of fiberwise adjunction spaces over a map g : P' → P of parameter spaces, for families of attaching maps α' i (p, s) = α i (g p, s) restricted along g: it is g × id on P' × A and on each family of discs. For the inclusion of a subspace P' ⊆ P, it includes the attachment of the restricted families into the attachment over P.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentMap_fiberwiseCellAttachmentIncl {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) (x : P' × ↑A) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentMap g α α' hα)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α')) x) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentIncl α)) (g x.1, x.2)

@[simp]

theorem TauCeti.fiberwiseCellAttachmentMap_fiberwiseCellAttachmentCell {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) (i : ι) (x : P' × ↑(TopCat.disk (k i))) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentMap g α α' hα)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α' i)) x) = (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentCell α i)) (g x.1, x.2)

@[simp]

theorem TauCeti.fiberwiseCellAttachmentProj_fiberwiseCellAttachmentMap {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) (y : ↑(fiberwiseCellAttachment α')) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentMap g α α' hα)) y) = g ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentProj α')) y)

The map of fiberwise adjunction spaces lies over g.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentMap_id {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (α i) (p, s) = (α i) ((ContinuousMap.id P) p, s)) : fiberwiseCellAttachmentMap (ContinuousMap.id P) α α hα = CategoryTheory.CategoryStruct.id (fiberwiseCellAttachment α)

The map of fiberwise adjunction spaces over the identity of P is the identity.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentMap_comp {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) {P'' : Type u} [TopologicalSpace P''] (g' : C(P'', P')) (α'' : (i : ι) → C(P'' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα' : ∀ (i : ι) (p : P'') (s : ↑(TopCat.diskBoundary (k i))), (α'' i) (p, s) = (α' i) (g' p, s)) : CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentMap g' α' α'' hα') (fiberwiseCellAttachmentMap g α α' hα) = fiberwiseCellAttachmentMap (g.comp g') α α'' ⋯

Maps of fiberwise adjunction spaces compose along composites of parameter maps.

@[simp]

theorem TauCeti.fiberwiseCellAttachmentMap_comp_assoc {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) {P'' : Type u} [TopologicalSpace P''] (g' : C(P'', P')) (α'' : (i : ι) → C(P'' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα' : ∀ (i : ι) (p : P'') (s : ↑(TopCat.diskBoundary (k i))), (α'' i) (p, s) = (α' i) (g' p, s)) {Z : TopCat} (h : fiberwiseCellAttachment α ⟶ Z) : CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentMap g' α' α'' hα') (CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentMap g α α' hα) h) = CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentMap (g.comp g') α α'' ⋯) h

Maps of fiberwise adjunction spaces compose along composites of parameter maps.

theorem TauCeti.fiberwiseCellComparison_fiberwiseCellAttachmentMap {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (α' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (hα : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α' i) (p, s) = (α i) (g p, s)) (χ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α i) (p, s))) (χ' : (i : ι) → C(P' × ↑(TopCat.disk (k i)), Y)) (hχ' : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (χ' i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α' i) (p, s))) (hχχ' : ∀ (i : ι) (p : P') (x : ↑(TopCat.disk (k i))), (χ' i) (p, x) = (χ i) (g p, x)) (y : ↑(fiberwiseCellAttachment α')) : (CategoryTheory.ConcreteCategory.hom (fiberwiseCellComparison α χ hχ)) ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentMap g α α' hα)) y) = (g ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellComparison α' χ' hχ')) y).1, ((CategoryTheory.ConcreteCategory.hom (fiberwiseCellComparison α' χ' hχ')) y).2)

The map of fiberwise adjunction spaces over g intertwines the comparison maps of characteristic families χ' i (p, x) = χ i (g p, x) restricted along g.

theorem TauCeti.fiberwiseCellReattachment_comp_fiberwiseCellAttachmentMap {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (α₀' α₁' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀' χ₁' : (i : ι) → C(P' × ↑(TopCat.disk (k i)), Y)) (hχ₀' : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (χ₀' i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀' i) (p, s))) (hχ₁' : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (χ₁' i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁' i) (p, s))) (h' : (i : ι) → C(P' × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh' : ∀ (i : ι) (p : P'), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h' i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K' : (i : ι) → (χ₁' i).Homotopy ((χ₀' i).comp (ContinuousMap.fst.prodMk (h' i)))) (hK' : ∀ (i : ι) (t : ↑unitInterval) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (K' i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (hα₀ : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α₀' i) (p, s) = (α₀ i) (g p, s)) (hα₁ : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α₁' i) (p, s) = (α₁ i) (g p, s)) (hh'h : ∀ (i : ι) (p : P') (x : ↑(TopCat.disk (k i))), (h' i) (p, x) = (h i) (g p, x)) (hK'K : ∀ (i : ι) (t : ↑unitInterval) (p : P') (x : ↑(TopCat.disk (k i))), (K' i) (t, p, x) = (K i) (t, g p, x)) : CategoryTheory.CategoryStruct.comp (fiberwiseCellReattachment α₀' α₁' χ₀' χ₁' hχ₀' hχ₁' h' hh' K' hK') (fiberwiseCellAttachmentMap g α₀ α₀' hα₀) = CategoryTheory.CategoryStruct.comp (fiberwiseCellAttachmentMap g α₁ α₁' hα₁) (fiberwiseCellReattachment α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK)

The fiberwise reattachment map is natural in the parameter space. Let g : P' → P be continuous, and restrict along g the data of a fiberwise reattachment map over P: the attaching maps, the self-maps h' i (p, x) = h i (g p, x) of the discs and the homotopies K' i (t, (p, x)) = K i (t, (g p, x)). Then the reattachment map over P' of the restricted data, followed by the map of fiberwise adjunction spaces over g, is the map over g followed by the reattachment map over P.

theorem TauCeti.fiberwiseCellReattachmentHomotopy_fiberwiseCellAttachmentMap {P Y : Type u} [TopologicalSpace P] [TopologicalSpace Y] {A : Set Y} {ι : Type u} {k : ι → ℕ} {P' : Type u} [TopologicalSpace P'] (g : C(P', P)) (α₀ α₁ : (i : ι) → C(P × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀ χ₁ : (i : ι) → C(P × ↑(TopCat.disk (k i)), Y)) (hχ₀ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₀ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀ i) (p, s))) (hχ₁ : ∀ (i : ι) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (χ₁ i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁ i) (p, s))) (h : (i : ι) → C(P × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh : ∀ (i : ι) (p : P), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K : (i : ι) → (χ₁ i).Homotopy ((χ₀ i).comp (ContinuousMap.fst.prodMk (h i)))) (hK : ∀ (i : ι) (t : ↑unitInterval) (p : P) (s : ↑(TopCat.diskBoundary (k i))), (K i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (α₀' α₁' : (i : ι) → C(P' × ↑(TopCat.diskBoundary (k i)), ↑A)) (χ₀' χ₁' : (i : ι) → C(P' × ↑(TopCat.disk (k i)), Y)) (hχ₀' : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (χ₀' i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₀' i) (p, s))) (hχ₁' : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (χ₁' i) (p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) = ↑((α₁' i) (p, s))) (h' : (i : ι) → C(P' × ↑(TopCat.disk (k i)), ↑(TopCat.disk (k i)))) (hh' : ∀ (i : ι) (p : P'), Set.MapsTo (fun (w : ↑(TopCat.disk (k i))) => (h' i) (p, w)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))) (K' : (i : ι) → (χ₁' i).Homotopy ((χ₀' i).comp (ContinuousMap.fst.prodMk (h' i)))) (hK' : ∀ (i : ι) (t : ↑unitInterval) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (K' i) (t, p, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s) ∈ A) (hα₁ : ∀ (i : ι) (p : P') (s : ↑(TopCat.diskBoundary (k i))), (α₁' i) (p, s) = (α₁ i) (g p, s)) (hK'K : ∀ (i : ι) (t : ↑unitInterval) (p : P') (x : ↑(TopCat.disk (k i))), (K' i) (t, p, x) = (K i) (t, g p, x)) (t : ↑unitInterval) (y : ↑(fiberwiseCellAttachment α₁')) : (fiberwiseCellReattachmentHomotopy α₀ α₁ χ₀ χ₁ hχ₀ hχ₁ h hh K hK) (t, (CategoryTheory.ConcreteCategory.hom (fiberwiseCellAttachmentMap g α₁ α₁' hα₁)) y) = (g ((fiberwiseCellReattachmentHomotopy α₀' α₁' χ₀' χ₁' hχ₀' hχ₁' h' hh' K' hK') (t, y)).1, ((fiberwiseCellReattachmentHomotopy α₀' α₁' χ₀' χ₁' hχ₀' hχ₁' h' hh' K' hK') (t, y)).2)

The homotopy Φ₀ ∘ E ≃ Φ₁ is natural in the parameter space. For data restricted along a continuous map g : P' → P, with K' i (t, (p, x)) = K i (t, (g p, x)), the homotopy over P read on the image of the map of fiberwise adjunction spaces over g is the homotopy over P' followed by g × id.