Affine barycentric subdivision maps on topological standard simplices

This file supplies the raw affine layer needed before the singular-chain barycentric subdivision operator.

For a permutation π : Equiv.Perm (Fin (n+1)), the π-summand of the barycentric subdivision of the topological standard simplex has vertices

b_k = barycenter {π 0, ..., π k}.

The file defines:

• prefixVertex : the ordered prefix map Fin (k+1) -> Fin (n+1);
• prefixBarycenter : the barycenter of the first k+1 vertices in that permuted order, as a point of SphereOddDegree.finiteSimplex ℝ (Fin (n+1));
• affineSubdivMap : the affine self-map of Δ^n sending vertex k to prefixBarycenter n π k.

This deliberately does not claim the chain-level boundary identity or the subdivision chain homotopy. Those are separate later files.

@[reducible, inline]

abbrev SphereOddDegree.AffineBarycentricSubdivision.Delta (n : ℕ) : Set (Fin (n + 1) → ℝ)

The ambient topological n-simplex, represented as the subtype of nonnegative coordinate functions on Fin (n+1) summing to 1.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.Delta n = SphereOddDegree.finiteSimplex ℝ (Fin (n + 1))

def SphereOddDegree.AffineBarycentricSubdivision.prefixVertex (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : Fin (↑k + 1) → Fin (n + 1)

The k-prefix vertex map associated to a permutation of the vertices of Δ^n. It sends 0,...,k into Fin (n+1) by the permuted order π.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.prefixVertex n π k i = π ⟨↑i, ⋯⟩

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : ↑(Delta n)

The barycenter of the first k+1 vertices in the order given by π, viewed as a point of the ambient simplex Δ^n. This uses Mathlib's existing SphereOddDegree.FiniteSimplex.barycenter and SphereOddDegree.FiniteSimplex.map, avoiding a hand proof that the coordinates are nonnegative and have total mass 1.

Equations

• One or more equations did not get rendered due to their size.

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_def (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : prefixBarycenter n π k = FiniteSimplex.map (prefixVertex n π k) FiniteSimplex.barycenter

Coordinate formula for prefixBarycenter. In words, the j-coordinate is 1/(k+1) if j occurs among π 0, ..., π k, and 0 otherwise. We keep it as an unfolded SphereOddDegree.FiniteSimplex.map formula because this is the form most useful for later simp-based face computations.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMapFun (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) : Fin (n + 1) → ℝ

The coordinate function of the affine map attached to the permutation π. It is the convex combination of the prefix barycenters with weights given by x.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMapFun n π x j = ∑ k : Fin (n + 1), x k * (SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter n π k) j

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMapFun_nonneg (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (j : Fin (n + 1)) : 0 ≤ affineSubdivMapFun n π x j

Nonnegativity of every coordinate of affineSubdivMapFun.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMapFun_sum_eq_one (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) : ∑ j : Fin (n + 1), affineSubdivMapFun n π x j = 1

The coordinates of affineSubdivMapFun sum to 1.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ↑(Delta n) → ↑(Delta n)

The affine self-map of Δ^n associated to a permutation π; this is the geometric simplex appearing as one signed summand in barycentric subdivision.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap n π x = ⟨SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMapFun n π x, ⋯⟩

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_apply (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (j : Fin (n + 1)) : (affineSubdivMap n π x) j = ∑ k : Fin (n + 1), x k * (prefixBarycenter n π k) j

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_vertex (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : affineSubdivMap n π (FiniteSimplex.vertex k) = prefixBarycenter n π k

The affine map sends the k-th vertex of the domain simplex to the k-th prefix barycenter.

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixVertex_comp (n : ℕ) (π τ : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : prefixVertex n (Equiv.trans τ π) k = fun (i : Fin (↑k + 1)) => π (prefixVertex n τ k i)

Naturality of the construction under postcomposition of the vertex permutation. This is a lightweight bookkeeping lemma useful when comparing adjacent permutation summands later.

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_zero (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : prefixBarycenter n π 0 = FiniteSimplex.vertex (π 0)

The first prefix barycenter is the first permuted vertex.