Piecewise-linear transport across a stellar subdivision

The barycentric identification of a stellar subdivision is a piecewise-linear map on the coordinate polyhedra. Its inverse is piecewise affine on the subdivided simplices, using the finite-simplex inverse criterion. These are the local transition maps needed to transport PL charts across stellar equivalences.

The inverse also has an explicit extension to arbitrary coordinate spaces: it removes the least coordinate on the starred face from each of its vertices and transfers the total removed mass to the new vertex. This extension is piecewise affine on minimum-coordinate cells and agrees with the inverse of the stellar homeomorphism of weak polyhedra. The resulting maps are packaged by the realization-level PLHomeomorphic relation, which is closed under symmetry and composition; this file derives such a package for every stellar equivalence, with no finiteness hypothesis on the complexes, and descends it through injective vertex relabelings for intrinsic stellar equivalence.

Reference: Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

@[instance_reducible]

noncomputable def stellarSubdivisionDecidableEq (α : Type u_1) : DecidableEq α

A local classical equality decision procedure for finite-coordinate bookkeeping.

noncomputable def Finset.stellarSubdivisionCoordinateMap {ι : Type u_1} (σ : Finset ι) (v : ι) : (ι → ℝ) →L[ℝ] ι → ℝ

The coordinate-space linear map induced by a stellar subdivision's barycentric map.

@[simp]

theorem Finset.stellarSubdivisionCoordinateMap_apply {ι : Type u_1} {σ : Finset ι} {v : ι} (x : ι → ℝ) (i : ι) : (σ.stellarSubdivisionCoordinateMap v) x i = x i + x v * ((if i ∈ σ then (↑σ.card)⁻¹ else 0) - if i = v then 1 else 0)

Coordinate formula for the barycentric map of a stellar subdivision.

@[simp]

theorem Finset.stellarSubdivisionCoordinateMap_coe {ι : Type u_1} (σ : Finset ι) (v : ι) (x : ι →₀ ℝ) : (σ.stellarSubdivisionCoordinateMap v) ⇑x = ⇑((σ.stellarSubdivisionLinearMap v) x)

The coordinate extension agrees with the finitely supported stellar map.

@[simp]

theorem Finset.stellarSubdivisionCoordinateMap_on_equiv {ι : Type u_1} {σ : Finset ι} {v : ι} [Finite ι] (x : ι →₀ ℝ) : (σ.stellarSubdivisionCoordinateMap v) (Finsupp.equivFunOnFinite x) = Finsupp.equivFunOnFinite ((σ.stellarSubdivisionLinearMap v) x)

The coordinate-space map agrees with the finitely supported stellar linear map.

noncomputable def Finset.stellarSubdivisionInverseExtension {ι : Type u_1} (σ : Finset ι) (hσ : σ.Nonempty) (v : ι) (x : ι → ℝ) : ι → ℝ

Extend the inverse stellar identification to coordinate space by transferring the least coordinate on σ to v. On an original polyhedron with unused vertex v, this is the inverse of the barycentric stellar map.

@[simp]

theorem Finset.stellarSubdivisionInverseExtension_apply {ι : Type u_1} [DecidableEq ι] (σ : Finset ι) (hσ : σ.Nonempty) (v : ι) (x : ι → ℝ) (i : ι) : σ.stellarSubdivisionInverseExtension hσ v x i = x i + σ.inf' hσ x * ((if i = v then ↑σ.card else 0) - if i ∈ σ then 1 else 0)

The inverse stellar extension's coordinate formula.

theorem Finset.isPiecewiseAffineOn_stellarSubdivisionInverseExtension {ι : Type u_1} (σ : Finset ι) (hσ : σ.Nonempty) (v : ι) : TauCeti.IsPiecewiseAffineOn (σ.stellarSubdivisionInverseExtension hσ v) Set.univ

The inverse stellar extension is piecewise affine on the entire coordinate space. Its cells are the regions on which one of the starred-face coordinates is least.

@[simp]

theorem Finset.stellarSubdivisionCoordinateMap_stellarSubdivisionInverseExtension {ι : Type u_1} {σ : Finset ι} (hσ : σ.Nonempty) {v : ι} (hvσ : v ∉ σ) {x : ι → ℝ} (hxv : x v = 0) : (σ.stellarSubdivisionCoordinateMap v) (σ.stellarSubdivisionInverseExtension hσ v x) = x

The barycentric coordinate extension cancels the inverse extension on coordinates vanishing at the new vertex. No positivity, support, or normalization is needed.

theorem Finset.stellarSubdivisionInverseExtension_stellarSubdivisionLinearMap {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ.Nonempty) {v : ι} (hvσ : v ∉ σ) {x : ι →₀ ℝ} (hxpos : ∀ (i : ι), 0 ≤ x i) (hxface : x.support ∈ K.stellarSubdivision σ v) : σ.stellarSubdivisionInverseExtension hσ v ⇑((σ.stellarSubdivisionLinearMap v) x) = ⇑x

On nonnegative coordinates supported on a stellar face, the inverse extension cancels the barycentric map. No normalization or finiteness of the complex or vertex type is needed.

theorem PreAbstractSimplicialComplex.exists_isPLOn_stellarSubdivisionLeftInverse {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (V : Finset ι) (hVσ : σ ⊆ V) (hV : ∀ τ ∈ K.stellarSubdivision σ v, τ ⊆ V) (hVv : v ∈ V) (hvσ : v ∉ σ) : let κ := ↥V; ∃ (g : (κ → ℝ) → κ → ℝ), TauCeti.IsPLOn g (⇑((σ.preimage (fun (i : κ) => ↑i) ⋯).stellarSubdivisionCoordinateMap ⟨v, hVv⟩) '' ⋃ (τ : ↑(K.stellarSubdivision σ v).faces), (convexHull ℝ) ((fun (x : κ) => Pi.single x 1) '' ↑((↑τ).preimage (fun (i : κ) => ↑i) ⋯))) ∧ ∀ x ∈ ⋃ (τ : ↑(K.stellarSubdivision σ v).faces), (convexHull ℝ) ((fun (x : κ) => Pi.single x 1) '' ↑((↑τ).preimage (fun (i : κ) => ↑i) ⋯)), g (((σ.preimage (fun (i : κ) => ↑i) ⋯).stellarSubdivisionCoordinateMap ⟨v, hVv⟩) x) = x

The inverse barycentric map is piecewise linear on finite active coordinates.

V is an explicit finite set of active vertices. It must contain the starred face, the new vertex, and every face of the stellar subdivision. This keeps the PL target finite-dimensional even when the original complex has an infinite ambient vertex type.

theorem PreAbstractSimplicialComplex.exists_homeomorph_stellarSubdivision_with_inverse {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} [DecidableEq ι] {A : AbstractSimplicialComplex ι} (hσ : σ ∈ K) (hv : {v} ∉ K) (hK : K ≤ A.toPreAbstractSimplicialComplex) (hS : K.stellarSubdivision σ v ≤ A.toPreAbstractSimplicialComplex) : ∃ (e : { x : A.Realization // (↑x).support ∈ K.stellarSubdivision σ v } ≃ₜ { x : A.Realization // (↑x).support ∈ K }), (∀ (x : { x : A.Realization // (↑x).support ∈ K.stellarSubdivision σ v }), ⇑↑↑(e x) = (σ.stellarSubdivisionCoordinateMap v) ⇑↑↑x) ∧ ∀ (y : { x : A.Realization // (↑x).support ∈ K }), ⇑↑↑(e.symm y) = σ.stellarSubdivisionInverseExtension ⋯ v ⇑↑↑y

The stellar homeomorphism has the barycentric continuous linear coordinate map as its forward extension and the piecewise-affine minimum-transfer map as its inverse extension. Thus stellar moves identify weak polyhedra by PL maps in both directions.

PL formulas along a stellar equivalence

theorem PreAbstractSimplicialComplex.IsStellarMove.plHomeomorphic {ι : Type u_1} [DecidableEq ι] {A B : PreAbstractSimplicialComplex ι} (h : A.IsStellarMove B) : A.PLHomeomorphic B

A single stellar move gives a PLHomeomorphic package.

theorem PreAbstractSimplicialComplex.StellarEquivalent.plHomeomorphic {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) : K.PLHomeomorphic L

A stellar equivalence identifies its weak polyhedra by ambient maps that are piecewise linear in their barycentric coordinates.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.plHomeomorphic {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) : K.PLHomeomorphic L

Intrinsically stellar-equivalent complexes have PL-homeomorphic weak polyhedra.