Gluing homotopies on weak realizations

A family on a weak realization, with a locally compact parameter space, is jointly continuous if and only if its restrictions to all closed simplex cylinders are continuous. The same criterion holds on the actual polyhedron of a precomplex, with the subspace topology, even when that precomplex omits vertices. On an open subset of the realization, continuity is detected on the traces of that subset in the closed simplex cylinders.

Compatible homotopies on the closed simplices therefore glue to a homotopy on the entire realization. The computation rule on each simplex also detects whether the glued homotopy fixes a subcomplex. These results permit simplex deformations to extend over infinite complexes without imposing a finite or locally finite triangulation.

The product topology is essential here: continuity separately in time and space would not suffice. We use Mathlib's quotient-map product lifting theorem, which requires local compactness only of the parameter space, and the final topology of the closed simplices.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2--3 (weak polyhedra and geometric simplicial collapse).

theorem AbstractSimplicialComplex.isQuotientMap_sigma_faceInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Topology.IsQuotientMap fun (p : (σ : TauCeti.SetLike.Face K) × StandardSimplex ↑σ) => K.faceInclusion p.fst p.snd

The closed simplices present the weak realization as a quotient of their disjoint union.

theorem AbstractSimplicialComplex.continuous_prod_iff_faceInclusion {ι : Type u_1} {K : AbstractSimplicialComplex ι} {P : Type u_2} {X : Type u_3} [TopologicalSpace P] [TopologicalSpace X] [LocallyCompactSpace P] {f : P × K.Realization → X} : Continuous f ↔ ∀ (σ : TauCeti.SetLike.Face K), Continuous fun (p : P × StandardSimplex ↑σ) => f (p.1, K.faceInclusion σ p.2)

Joint continuity with a locally compact parameter can be checked on closed simplex cylinders. Neither the realization nor the vertex type needs to be locally compact or finite.

theorem AbstractSimplicialComplex.isQuotientMap_sigma_subtype_faceInclusion {ι : Type u_1} {K : AbstractSimplicialComplex ι} {L : PreAbstractSimplicialComplex ι} (hL : L ≤ K.toPreAbstractSimplicialComplex) : Topology.IsQuotientMap fun (p : (σ : ↑L.faces) × StandardSimplex ↑σ) => ⟨K.faceInclusion ⟨↑p.fst, ⋯⟩ p.snd, ⋯⟩

The simplices of a precomplex present its actual polyhedron as a quotient, including when the precomplex has no faces or omits ambient vertices.

theorem AbstractSimplicialComplex.continuous_prod_subtype_iff_faceInclusion {ι : Type u_1} {K : AbstractSimplicialComplex ι} {P : Type u_2} {X : Type u_3} [TopologicalSpace P] [TopologicalSpace X] [LocallyCompactSpace P] {L : PreAbstractSimplicialComplex ι} (hL : L ≤ K.toPreAbstractSimplicialComplex) {f : P × { x : K.Realization // (↑x).support ∈ L } → X} : Continuous f ↔ ∀ (σ : Finset ι) (hσ : σ ∈ L), Continuous fun (p : P × StandardSimplex σ) => f (p.1, ⟨K.faceInclusion ⟨σ, ⋯⟩ p.2, ⋯⟩)

Joint continuity on a precomplex polyhedron is detected on its closed simplex cylinders, with a locally compact parameter space and the ambient weak subspace topology.

theorem AbstractSimplicialComplex.continuous_prod_subtype_iff_faceInclusion_of_isOpen {ι : Type u_1} {K : AbstractSimplicialComplex ι} {P : Type u_2} {X : Type u_3} [TopologicalSpace P] [TopologicalSpace X] [LocallyCompactSpace P] {U : Set K.Realization} (hU : IsOpen U) {f : P × ↑U → X} : Continuous f ↔ ∀ (σ : TauCeti.SetLike.Face K), Continuous fun (p : P × ↑(K.faceInclusion σ ⁻¹' U)) => f (p.1, ⟨K.faceInclusion σ ↑p.2, ⋯⟩)

Joint continuity on an open subset of a weak realization, with a locally compact parameter, is detected on the traces of that subset in the closed simplex cylinders. Unlike a subcomplex, an open subset meets a closed simplex in a set which need not be a union of faces.

noncomputable def AbstractSimplicialComplex.homotopyOfFaces {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_3} [TopologicalSpace X] {f₀ f₁ : C(K.Realization, X)} (H : (σ : TauCeti.SetLike.Face K) → (f₀.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ }).Homotopy (f₁.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ })) (hH : ∀ (σ τ : TauCeti.SetLike.Face K) (x : StandardSimplex ↑σ) (y : StandardSimplex ↑τ), K.faceInclusion σ x = K.faceInclusion τ y → ∀ (t : ↑unitInterval), (H σ) (t, x) = (H τ) (t, y)) : f₀.Homotopy f₁

Glue homotopies on all closed simplices, provided they agree wherever their face maps have the same image. The endpoint maps are the given global continuous maps.

@[simp]

theorem AbstractSimplicialComplex.homotopyOfFaces_apply_faceInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_3} [TopologicalSpace X] {f₀ f₁ : C(K.Realization, X)} (H : (σ : TauCeti.SetLike.Face K) → (f₀.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ }).Homotopy (f₁.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ })) (hH : ∀ (σ τ : TauCeti.SetLike.Face K) (x : StandardSimplex ↑σ) (y : StandardSimplex ↑τ), K.faceInclusion σ x = K.faceInclusion τ y → ∀ (t : ↑unitInterval), (H σ) (t, x) = (H τ) (t, y)) (σ : TauCeti.SetLike.Face K) (t : ↑unitInterval) (x : StandardSimplex ↑σ) : (K.homotopyOfFaces H hH) (t, K.faceInclusion σ x) = (H σ) (t, x)

The glued homotopy agrees with the specified homotopy on every closed simplex.

theorem AbstractSimplicialComplex.homotopyOfFaces_unique {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_3} [TopologicalSpace X] {f₀ f₁ : C(K.Realization, X)} (H : (σ : TauCeti.SetLike.Face K) → (f₀.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ }).Homotopy (f₁.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ })) (hH : ∀ (σ τ : TauCeti.SetLike.Face K) (x : StandardSimplex ↑σ) (y : StandardSimplex ↑τ), K.faceInclusion σ x = K.faceInclusion τ y → ∀ (t : ↑unitInterval), (H σ) (t, x) = (H τ) (t, y)) (G : f₀.Homotopy f₁) (hG : ∀ (σ : TauCeti.SetLike.Face K) (t : ↑unitInterval) (x : StandardSimplex ↑σ), G (t, K.faceInclusion σ x) = (H σ) (t, x)) : G = K.homotopyOfFaces H hH

A homotopy with the given restrictions on all closed simplices is the glued homotopy.

noncomputable def AbstractSimplicialComplex.homotopyRelOfFaces {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_3} [TopologicalSpace X] {f₀ f₁ : C(K.Realization, X)} (H : (σ : TauCeti.SetLike.Face K) → (f₀.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ }).Homotopy (f₁.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ })) (hH : ∀ (σ τ : TauCeti.SetLike.Face K) (x : StandardSimplex ↑σ) (y : StandardSimplex ↑τ), K.faceInclusion σ x = K.faceInclusion τ y → ∀ (t : ↑unitInterval), (H σ) (t, x) = (H τ) (t, y)) {S : Set K.Realization} (hfix : ∀ (σ : TauCeti.SetLike.Face K) (t : ↑unitInterval) (x : StandardSimplex ↑σ), K.faceInclusion σ x ∈ S → (H σ) (t, x) = f₀ (K.faceInclusion σ x)) : f₀.HomotopyRel f₁ S

Glue simplex homotopies which fix the traces of S to a homotopy relative to S. In particular, S may be the retained polyhedron of a simplicial collapse.

@[simp]

theorem AbstractSimplicialComplex.homotopyRelOfFaces_apply_faceInclusion {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_3} [TopologicalSpace X] {f₀ f₁ : C(K.Realization, X)} (H : (σ : TauCeti.SetLike.Face K) → (f₀.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ }).Homotopy (f₁.comp { toFun := K.faceInclusion σ, continuous_toFun := ⋯ })) (hH : ∀ (σ τ : TauCeti.SetLike.Face K) (x : StandardSimplex ↑σ) (y : StandardSimplex ↑τ), K.faceInclusion σ x = K.faceInclusion τ y → ∀ (t : ↑unitInterval), (H σ) (t, x) = (H τ) (t, y)) {S : Set K.Realization} (hfix : ∀ (σ : TauCeti.SetLike.Face K) (t : ↑unitInterval) (x : StandardSimplex ↑σ), K.faceInclusion σ x ∈ S → (H σ) (t, x) = f₀ (K.faceInclusion σ x)) (σ : TauCeti.SetLike.Face K) (t : ↑unitInterval) (x : StandardSimplex ↑σ) : (K.homotopyRelOfFaces H hH hfix) (t, K.faceInclusion σ x) = (H σ) (t, x)

The relative glued homotopy agrees with the specified homotopy on each closed simplex.