Internal-swap barycenter lemmas for barycentric subdivision

This file supplies the three local lemmas needed before proving the internal face-cancellation part of the barycentric-subdivision boundary identity.

The main theorem is prefixBarycenter_internal_swap_eq: if τ is the adjacent swap of the i-th and (i+1)-st ambient vertices, then every prefix barycenter except the deleted i-th one is unchanged after replacing π by τ.trans π.

The proof is deliberately stated in terms of reindexing of the prefix domain; this is the right form for the later face-map proof.

theorem SphereOddDegree.AffineBarycentricSubdivision.stdSimplex_map_barycenter_equiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (e : X ≃ Y) [Nonempty X] [Nonempty Y] : FiniteSimplex.map (⇑e) FiniteSimplex.barycenter = FiniteSimplex.barycenter

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_eq_of_prefix_reindex {n : ℕ} {π π' : Equiv.Perm (Fin (n + 1))} {k : Fin (n + 1)} (e : Equiv.Perm (Fin (↑k + 1))) (h : ∀ (t : Fin (↑k + 1)), prefixVertex n π k t = prefixVertex n π' k (e t)) : prefixBarycenter n π k = prefixBarycenter n π' k

If two maps out of the prefix domain differ only by a permutation of that domain, then the corresponding prefix barycenters are equal.

Internal adjacent swap on prefix barycenters

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.prefixDomainAdjacentSwap {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 2)) (hik : ↑i + 1 ≤ ↑k) : Equiv.Perm (Fin (↑k + 1))

The domain permutation used when a prefix already contains both adjacent indices i and i+1: swap their representatives in the smaller prefix domain.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.prefixDomainAdjacentSwap i k hik = Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixVertex_internal_swap_reindex {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) (k : Fin (n + 2)) (hk : k ≠ i.castSucc) : ∃ (e : Equiv.Perm (Fin (↑k + 1))), ∀ (t : Fin (↑k + 1)), prefixVertex (n + 1) π k t = prefixVertex (n + 1) (Equiv.trans (Equiv.swap i.castSucc i.succ) π) k (e t)

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_internal_swap_eq {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) (k : Fin (n + 2)) (hk : k ≠ i.castSucc) : prefixBarycenter (n + 1) π k = prefixBarycenter (n + 1) (Equiv.trans (Equiv.swap i.castSucc i.succ) π) k

Prefix barycenters are unchanged by the internal adjacent swap, except at the deleted prefix index itself.

This is the main local affine fact needed for the internal-face cancellation in the proof that barycentric subdivision commutes with the singular boundary.