Last-face affine identity for barycentric subdivision

This file isolates the affine part of the last-face calculation in the proof that barycentric subdivision commutes with the singular boundary.

The theorem is stated in a face-data form. Suppose

• π : Equiv.Perm (Fin (n+2)) is a top-dimensional subdivision summand;
• ι : Fin (n+1) -> Fin (n+2) is the vertex inclusion of the codimension-one face missing the last vertex π last;
• ρ : Equiv.Perm (Fin (n+1)) is the induced permutation on that face;
• ι (ρ t) = π (Fin.castSucc t) for every t.

Then the restriction of the affine subdivision map for π to the final domain face is the inclusion of the affine subdivision map for ρ on the boundary face.

This deliberately avoids fixing the library's eventual coface-map API. Later, one instantiates ι with the ordinary order-preserving injection missing π last, and ρ with the induced ordering of the remaining vertices.

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_castSucc_eq_map_of_prefix {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (ι : Fin (n + 1) → Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hιρ : ∀ (t : Fin (n + 1)), ι (ρ t) = π t.castSucc) (k : Fin (n + 1)) : prefixBarycenter (n + 1) π k.castSucc = FiniteSimplex.map ι (prefixBarycenter n ρ k)

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdiv_face_last_eq_boundary_subdiv_of_faceData {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (ι : Fin (n + 1) → Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hιρ : ∀ (t : Fin (n + 1)), ι (ρ t) = π t.castSucc) (x : ↑(Delta (n + 1))) (y : ↑(Delta n)) (hxlast : x ⟨n + 1, ⋯⟩ = 0) (hy : ∀ (k : Fin (n + 1)), y k = x k.castSucc) : affineSubdivMap (n + 1) π x = FiniteSimplex.map ι (affineSubdivMap n ρ y)

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdiv_face_last_eq_boundary_subdiv {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (ι : Fin (n + 1) → Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hιρ : ∀ (t : Fin (n + 1)), ι (ρ t) = π t.castSucc) (x : ↑(Delta (n + 1))) (y : ↑(Delta n)) (hxlast : x ⟨n + 1, ⋯⟩ = 0) (hy : ∀ (k : Fin (n + 1)), y k = x k.castSucc) : affineSubdivMap (n + 1) π x = FiniteSimplex.map ι (affineSubdivMap n ρ y)

A slightly shorter alias for the last-face affine identity.