Generator-level barycentric boundary cancellation ∂ (sd σ) = sd (∂ σ)

This file proves the hard finite double-sum cancellation underlying the fact that the degree-wise barycentric subdivision operator commutes with the singular boundary on a single basis generator.

The main result is expandedBarycentricBoundaryCancellation:

∂ (sd σ) = sd (∂ σ)

stated over the actual expanded sums, using the actual singular-boundary formula (singularBoundary_chainGenerator_formula) and the actual subdivision operator (barycentricSubdivisionGenerator / barycentricSubdivisionLinearMap).

How the cancellation works

After expanding both sides on a generator σ : singularSimplices X (n+1) we get

∂(sd σ) = Σ_{π} sign(π) Σ_{i : Fin (n+2)} (-1)^i [face_i (σ ∘ a_π)] .

Splitting the inner face index i into internal faces i = castSucc i' (i' : Fin (n+1)) and the last face i = Fin.last (n+1):

• Internal faces cancel. For a fixed internal index i', pairing each permutation π with π' = (swap (castSucc i') (succ i')).trans π gives a fixed-point-free involution under which the affine faces are equal (faceSimplex_internal_swap_eq, from affineSubdiv_face_internal_swap) while the signs are opposite (permSignCoeff_adjacent_swap). Hence the sum over all permutations is 0, via internal_faces_double_sum_cancel.

• Last faces reindex. Writing j = π (last) and letting ρ : Perm (Fin (n+1)) be the induced permutation on the remaining vertices, the last face is the barycentric subdivision of the j-th boundary face of σ (faceSimplex_last_eq_subdiv_faceData, from affineSubdiv_face_last_eq_boundary_subdiv) and the signs match (permSignCoeff_last_face_of_faceData). The bijection lastFaceEquiv : (Fin (n+2) × Perm (Fin (n+1))) ≃ Perm (Fin (n+2)), (j, ρ) ↦ (extendLastPerm ρ).trans (insertLastPerm j), reindexes the last-face sum onto sd (∂ σ).

1. Naturality of toSSetObjEquiv and the topological coface map

theorem SphereOddDegree.AffineBarycentricSubdivision.toSSetObjEquiv_map_op_naturality (X : TopCat) (n m : ℕ) (g : { len := n } ⟶ { len := m }) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := m })) : (X.toSSetObjEquiv (Opposite.op { len := n })) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map g.op)) σ) = ((X.toSSetObjEquiv (Opposite.op { len := m })) σ).comp (TopCat.Hom.hom (SimplexCategory.toTop₀.map g))

Naturality of TopCat.toSSetObjEquiv. Applying the simplicial-set map (toSSet.obj X).map g.op corresponds, under toSSetObjEquiv, to precomposition with the topological realization toTop₀.map g of the simplex-category morphism g.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.cofaceTop (n : ℕ) (k : Fin (n + 2)) : C(↑(Delta n), ↑(Delta (n + 1)))

The topological coface map Δⁿ → Δⁿ⁺¹ deleting the k-th vertex, as the affine inclusion sending vertex t to vertex k.succAbove t.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.cofaceTop n k = { toFun := SphereOddDegree.FiniteSimplex.map k.succAbove, continuous_toFun := ⋯ }

theorem SphereOddDegree.AffineBarycentricSubdivision.cofaceTop_apply_base (n : ℕ) (k : Fin (n + 2)) (y : ↑(Delta n)) : ((cofaceTop n k) y) k = 0

The k-coordinate of cofaceTop n k y is zero: the affine coface never hits the deleted vertex k.

theorem SphereOddDegree.AffineBarycentricSubdivision.cofaceTop_last_castSucc (n : ℕ) (t : Fin (n + 1)) (y : ↑(Delta n)) : ((cofaceTop n (Fin.last (n + 1))) y) t.castSucc = y t

The last coface cofaceTop n (last) is the standard castSucc inclusion: its castSucc t coordinate is the t coordinate of y.

theorem SphereOddDegree.AffineBarycentricSubdivision.cofaceTop_eq (n : ℕ) (k : Fin (n + 2)) (y : Convexity.StdSimplex ℝ (Fin (n + 1))) : (intrinsicSimplexCoordinates (n + 1)) ((TopCat.Hom.hom (SimplexCategory.toTop₀.map (SimplexCategory.δ k))) y) = (cofaceTop n k) ((intrinsicSimplexCoordinates n) y)

The topological realization of the coface morphism δ k is the affine coface cofaceTop n k.

theorem SphereOddDegree.AffineBarycentricSubdivision.faceSimplex_continuousMap (X : TopCat) (n : ℕ) (k : Fin (n + 2)) (σ : singularSimplices X (n + 1)) : singularSimplexAsContinuousMap X n (AlexanderWhitney.faceSimplex X n k σ) = (singularSimplexAsContinuousMap X (n + 1) σ).comp (cofaceTop n k)

Face as a continuous map. The k-th boundary face of a singular simplex is, under toSSetObjEquiv, the precomposition with the topological coface cofaceTop n k.

2. Singular-simplex equality and the subdivision summand as a map

theorem SphereOddDegree.AffineBarycentricSubdivision.singularSimplices_ext {X : TopCat} {n : ℕ} {a b : singularSimplices X n} (h : singularSimplexAsContinuousMap X n a = singularSimplexAsContinuousMap X n b) : a = b

Two singular simplices coincide as soon as their associated continuous maps do (toSSetObjEquiv is injective).

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivSimplex_continuousMap (X : TopCat) (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (σ : singularSimplices X n) : singularSimplexAsContinuousMap X n (barycentricSubdivSimplex X n π σ) = (singularSimplexAsContinuousMap X n σ).comp (affineSubdivContinuousMap n π)

The barycentric subdivision summand σ ∘ a_π, viewed as a continuous map.

3. Internal-face bridge: affine faces agree under adjacent swap

theorem SphereOddDegree.AffineBarycentricSubdivision.faceSimplex_internal_swap_eq (X : TopCat) (n : ℕ) (π : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) (σ : singularSimplices X (n + 1)) : AlexanderWhitney.faceSimplex X n i.castSucc (barycentricSubdivSimplex X (n + 1) π σ) = AlexanderWhitney.faceSimplex X n i.castSucc (barycentricSubdivSimplex X (n + 1) (Equiv.trans (Equiv.swap i.castSucc i.succ) π) σ)

Internal-face identity at the chain level. For an internal face index castSucc i, the corresponding boundary face of the π-subdivision summand equals that of the adjacent-swapped permutation summand.

4. Last-face bridge and the last-face permutation bookkeeping

theorem SphereOddDegree.AffineBarycentricSubdivision.extendLastPerm_castSucc {n : ℕ} (ρ : Equiv.Perm (Fin (n + 1))) (t : Fin (n + 1)) : (extendLastPerm ρ) t.castSucc = (ρ t).castSucc

extendLastPerm ρ sends castSucc t to castSucc (ρ t).

theorem SphereOddDegree.AffineBarycentricSubdivision.extendLastPerm_lastVertex {n : ℕ} (ρ : Equiv.Perm (Fin (n + 1))) : (extendLastPerm ρ) (lastVertex n) = lastVertex n

extendLastPerm ρ fixes the last vertex.

theorem SphereOddDegree.AffineBarycentricSubdivision.lastFaceMap_apply_last {n : ℕ} (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) : (Equiv.trans (extendLastPerm ρ) (insertLastPerm j)) (lastVertex n) = j

The image of (j, ρ) under the last-face decomposition sends the last vertex to j.

theorem SphereOddDegree.AffineBarycentricSubdivision.lastFaceMap_apply_castSucc {n : ℕ} (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (t : Fin (n + 1)) : (Equiv.trans (extendLastPerm ρ) (insertLastPerm j)) t.castSucc = j.succAbove (ρ t)

The image of (j, ρ) under the last-face decomposition sends castSucc t to j.succAbove (ρ t).

theorem SphereOddDegree.AffineBarycentricSubdivision.faceSimplex_last_eq_subdiv_faceData (X : TopCat) (n : ℕ) (π : Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hρ : ∀ (t : Fin (n + 1)), j.succAbove (ρ t) = π t.castSucc) (σ : singularSimplices X (n + 1)) : AlexanderWhitney.faceSimplex X n (lastVertex n) (barycentricSubdivSimplex X (n + 1) π σ) = barycentricSubdivSimplex X n ρ (AlexanderWhitney.faceSimplex X n j σ)

Last-face identity at the chain level, face-data form. If j = π (last) and, on the remaining vertices, π is j.succAbove ∘ ρ, then the last boundary face of the π-subdivision summand is the ρ-subdivision summand of the j-th boundary face of σ.

5. The last-face reindexing equivalence

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.lastFaceMap (n : ℕ) : Fin (n + 2) × Equiv.Perm (Fin (n + 1)) → Equiv.Perm (Fin (n + 2))

The map underlying the last-face decomposition equivalence: (j, ρ) ↦ (extendLastPerm ρ).trans (insertLastPerm j).

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.lastFaceMap_injective (n : ℕ) : Function.Injective (lastFaceMap n)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.lastFaceEquiv (n : ℕ) : Fin (n + 2) × Equiv.Perm (Fin (n + 1)) ≃ Equiv.Perm (Fin (n + 2))

The last-face decomposition equivalence (Fin (n+2) × Perm (Fin (n+1))) ≃ Perm (Fin (n+2)).

Equations

• SphereOddDegree.AffineBarycentricSubdivision.lastFaceEquiv n = Equiv.ofBijective (SphereOddDegree.AffineBarycentricSubdivision.lastFaceMap n) ⋯

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.lastFaceEquiv_apply (n : ℕ) (p : Fin (n + 2) × Equiv.Perm (Fin (n + 1))) : (lastFaceEquiv n) p = Equiv.trans (extendLastPerm p.2) (insertLastPerm p.1)

6. Internal involution facts

theorem SphereOddDegree.AffineBarycentricSubdivision.internalSwap_involutive {n : ℕ} (i : Fin (n + 1)) : Function.Involutive fun (π : Equiv.Perm (Fin (n + 2))) => Equiv.trans (Equiv.swap i.castSucc i.succ) π

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

7. Internal faces cancel

theorem SphereOddDegree.AffineBarycentricSubdivision.internal_faces_sum_eq_zero (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X (n + 1)) : ∑ π : Equiv.Perm (Fin (n + 2)), ∑ i : Fin (n + 1), permSignCoeff R π • (-1) ^ ↑i.castSucc • chainGenerator R X n (AlexanderWhitney.faceSimplex X n i.castSucc (barycentricSubdivSimplex X (n + 1) π σ)) = 0

The internal-face double sum vanishes by adjacent-swap involution cancellation.

8. Last faces reindex to sd (∂ σ)

theorem SphereOddDegree.AffineBarycentricSubdivision.last_faces_sum_eq_subdiv_boundary (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X (n + 1)) : ∑ π : Equiv.Perm (Fin (n + 2)), permSignCoeff R π • (-1) ^ ↑(Fin.last (n + 1)) • chainGenerator R X n (AlexanderWhitney.faceSimplex X n (Fin.last (n + 1)) (barycentricSubdivSimplex X (n + 1) π σ)) = ∑ i : Fin (n + 2), (-1) ^ ↑i • barycentricSubdivisionGenerator R X n (AlexanderWhitney.faceSimplex X n i σ)

The last-face sum equals sd (∂ σ) after reindexing by lastFaceEquiv.

9. Main theorem

theorem SphereOddDegree.AffineBarycentricSubdivision.expandedBarycentricBoundaryCancellation (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X (n + 1)) : (ModuleCat.Hom.hom (singularBoundary R X n)) (barycentricSubdivisionGenerator R X (n + 1) σ) = (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) ((ModuleCat.Hom.hom (singularBoundary R X n)) (chainGenerator R X (n + 1) σ))

Expanded barycentric boundary cancellation on a generator. The singular boundary of the barycentric subdivision of a generator equals the barycentric subdivision of its boundary:

∂ (sd σ) = sd (∂ σ).

This is proved over the actual expanded sums, splitting the boundary of the subdivision into internal faces (which cancel) and last faces (which reindex to sd (∂ σ)).