Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite cone collapse

Abstract

An explicit based homotopy inverse for collapsing a finite cone subcomplex.

Definition 1.1 (Coordinate face simplices).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.faceSimplex

Formalization. D5/S3/Geometry/FiniteConeCollapse.faceSimplex (✓ std3).

Source. Repository-derived.

Commentary.

For a finite vertex type V and a finite subset s, the face simplex consists of real coordinate vectors with nonnegative entries summing to one and with every coordinate outside s equal to zero. The simplex of the empty face is empty.

Theorem 1.2 (Actual affine simplices).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.faceSimplex_eq_convexHull

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteConeCollapse.faceSimplex_eq_convexHull (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite subset s of V, its coordinate simplex equals the convex hull in the real coordinate space of the coordinate vertices indexed by s. Thus the coordinate model is the usual geometric simplex, including its boundary faces.

Definition 1.3 (Finite geometric realization).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.realization

Formalization. D5/S3/Geometry/FiniteConeCollapse.realization (✓ std3).

Source. Repository-derived.

Commentary.

The realization of a Mathlib pre-abstract simplicial complex is the union of its actual coordinate face simplices, with the subspace topology inherited from the finite real coordinate space. The ambient vertex type may contain vertices absent from the complex.

Definition 1.4 (An actual cone subcomplex).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.ConePair

Formalization. D5/S3/Geometry/FiniteConeCollapse.ConePair (✓ std3).

Source. Repository-derived.

Commentary.

A cone pair consists of an ambient complex M, a subcomplex C, and an apex p whose singleton is a face of C. Adjoining p to any face of C again gives a face of C. These are face conditions on the given complexes, and do not assert any extension property or homotopy equivalence. The singleton cone is included.

Definition 1.5 (The realized subcomplex).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.coneSet

Formalization. D5/S3/Geometry/FiniteConeCollapse.coneSet (✓ std3).

Source. Repository-derived.

Commentary.

Inside the ambient coordinate realization, the cone set is exactly the set of points belonging to the coordinate realization of C.

Definition 1.6 (The based coordinate vertex).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.apexPoint

Formalization. D5/S3/Geometry/FiniteConeCollapse.apexPoint (✓ std3).

Source. Repository-derived.

Commentary.

The basepoint is the coordinate vector with entry one at p and zero at every other vertex.

Definition 1.7 (Coordinate truncation and cone contraction).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.controlledHomotopy

Formalization. D5/S3/Geometry/FiniteConeCollapse.controlledHomotopy (✓ std3).

Source. Repository-derived.

Commentary.

For each cone face, sum the coordinates outside that face, and take the minimum of these finitely many sums. This continuous nonnegative function vanishes exactly on the cone. Truncate every coordinate by the smaller of that minimum and 1 divided by twice the number of ambient vertices plus two, then normalize. Throughout the unit interval the denominator is at least one half, the support stays in the original face, and points sufficiently near the cone enter an actual cone face. A continuous collar coefficient then turns on the linear contraction to p only after truncation has reached that face. The resulting ambient homotopy starts at the identity, preserves the cone, finishes by sending the cone to p, and fixes p throughout.

Definition 1.8 (The actual collapse relation).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.collapseSetoid

Formalization. D5/S3/Geometry/FiniteConeCollapse.collapseSetoid (✓ std3).

Source. Repository-derived.

Commentary.

Two points are related exactly when they are equal or both belong to the realized cone. The quotient carries the quotient topology.

Definition 1.9 (The continuous quotient map).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.quotientMap

Formalization. D5/S3/Geometry/FiniteConeCollapse.quotientMap (✓ std3).

Source. Repository-derived.

Commentary.

The forward map sends a point to its class under the actual collapse relation.

Definition 1.10 (An explicit continuous inverse up to homotopy).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.collapseInverse

Formalization. D5/S3/Geometry/FiniteConeCollapse.collapseInverse (✓ std3).

Source. Repository-derived.

Commentary.

The final controlled deformation is constant on every collapse fiber. Its quotient lift is the continuous inverse map and sends the cone class to p.

Definition 1.11 (Both based inverse homotopies).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.basedCollapse

Formalization. D5/S3/Geometry/FiniteConeCollapse.basedCollapse (✓ std3).

Source. Repository-derived.

Commentary.

The ambient controlled deformation is a homotopy from the identity to the quotient map followed by the inverse, relative to p. Composing the deformation with the quotient map is constant on each collapse fiber at every time, so it descends to the second homotopy, from the quotient identity to the inverse followed by the quotient map, relative to the cone class. Joint continuity follows from Mathlib’s quotient-product lifting theorem using local compactness of the unit interval.

Definition 1.12 (Based homotopy equivalence of the actual quotient).

Lean statement: D5/S3/Geometry/FiniteConeCollapse.collapseEquiv

Formalization. D5/S3/Geometry/FiniteConeCollapse.collapseEquiv (✓ std3).

Source. Repository-derived.

Commentary.

For every finite cone pair, the actual quotient map is a homotopy equivalence with the displayed inverse and both displayed based homotopies. This is the finite cone collapse lemma. It does not settle the additional join, graph substitution, or zero-vertex conventions of Carnero Bravo’s Question 22.

References