Open-cover-small singular simplices

This file introduces the notion that a singular simplex of a space X is small with respect to an open cover of X: its image is contained in one of the open sets of the cover.

We work with the library's existing singular simplex API (SphereOddDegree.singularSimplices), whose underlying continuous map out of the topological standard simplex Delta n is recovered by SphereOddDegree.AffineBarycentricSubdivision.singularSimplexAsContinuousMap. No parallel singular-simplex type is introduced.

Main definitions

• SphereOddDegree.OpenCoverData X — a family of open subsets of X that covers X.
• SphereOddDegree.IsSmallSimplex 𝒰 σ — the predicate that the image (range) of the singular simplex σ is contained in some member of the cover 𝒰.

Main results

• SphereOddDegree.IsSmallSimplex.of_range_subset — smallness is inherited along any range inclusion of the underlying continuous maps.
• SphereOddDegree.IsSmallSimplex.comp_of_range_subset — if τ = σ ∘ φ for a continuous map φ : Delta m → Delta n, then smallness of σ implies smallness of τ.
• SphereOddDegree.IsSmallSimplex.face — every boundary face of a small simplex is small.

This file deliberately does not prove smallness of barycentric subdivision; that belongs to downstream modules.

1. Open cover data

structure SphereOddDegree.OpenCoverData (X : TopCat) : Type

An open cover of a topological space X: a family of open subsets whose union is all of X.

• sets : Set (Set ↑X)

  The underlying family of subsets of X.

• isOpen_mem (U : Set ↑X) : U ∈ self.sets → IsOpen U

  Each member of the family is open.

• covers (x : ↑X) : ∃ U ∈ self.sets, x ∈ U

  The family covers X.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.mvSimplexMap {X : TopCat} {n : ℕ} (σ : singularSimplices X n) : C(↑(AffineBarycentricSubdivision.Delta n), ↑X)

The underlying continuous map Delta n → X of a singular simplex σ. This is a thin alias for the library's singularSimplexAsContinuousMap, matching the schematic mvSimplexMap accessor.

Equations

• SphereOddDegree.mvSimplexMap σ = SphereOddDegree.AffineBarycentricSubdivision.singularSimplexAsContinuousMap X n σ

2. Smallness with respect to a cover

def SphereOddDegree.IsSmallSimplex {X : TopCat} (𝒰 : OpenCoverData X) {n : ℕ} (σ : singularSimplices X n) : Prop

A singular n-simplex σ is small with respect to an open cover 𝒰 if its image is contained in one of the open sets of the cover.

Equations

• SphereOddDegree.IsSmallSimplex 𝒰 σ = ∃ U ∈ 𝒰.sets, Set.range ⇑(SphereOddDegree.mvSimplexMap σ) ⊆ U

theorem SphereOddDegree.IsSmallSimplex.of_range_subset {X : TopCat} {𝒰 : OpenCoverData X} {m n : ℕ} {σ : singularSimplices X n} {τ : singularSimplices X m} (hσ : IsSmallSimplex 𝒰 σ) (h : Set.range ⇑(mvSimplexMap τ) ⊆ Set.range ⇑(mvSimplexMap σ)) : IsSmallSimplex 𝒰 τ

Smallness is inherited along any inclusion of ranges of the underlying continuous maps.

theorem SphereOddDegree.IsSmallSimplex.comp_of_range_subset {X : TopCat} {𝒰 : OpenCoverData X} {m n : ℕ} {σ : singularSimplices X n} {τ : singularSimplices X m} (φ : C(↑(AffineBarycentricSubdivision.Delta m), ↑(AffineBarycentricSubdivision.Delta n))) (hcomp : mvSimplexMap τ = (mvSimplexMap σ).comp φ) (hσ : IsSmallSimplex 𝒰 σ) : IsSmallSimplex 𝒰 τ

If τ factors as σ ∘ φ for a continuous map φ : Delta m → Delta n (at the level of underlying continuous maps), then smallness of σ implies smallness of τ.

theorem SphereOddDegree.IsSmallSimplex.face {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} {σ : singularSimplices X (n + 1)} (hσ : IsSmallSimplex 𝒰 σ) (i : Fin (n + 2)) : IsSmallSimplex 𝒰 (AlexanderWhitney.faceSimplex X n i σ)

Face stability. Every boundary face of a small simplex is small: a face has image contained in the image of the original simplex.