Finite cancellation kernels for barycentric subdivision

This file collects the purely finite, abstract algebraic cancellation and reindexing lemmas used in the boundary computation for barycentric subdivision.

They are stated for arbitrary finite index types and abelian groups, so they are independent of any singular-chain or face-map API:

• finite_sum_cancel_of_fixedPointFree_involution: a fixed-point-free involution pairing terms with opposite signs makes the total sum vanish;
• internal_faces_cancel_for_index / internal_faces_double_sum_cancel: the specializations used to cancel internal boundary faces;
• last_faces_reindex_of_equiv: a finite reindexing principle for the last faces.

No chain-level boundary statement is asserted here.

theorem SphereOddDegree.AffineBarycentricSubdivision.finite_sum_cancel_of_fixedPointFree_involution {α M : Type} [Fintype α] [AddCommGroup M] (ι : α → α) (hιι : Function.Involutive ι) (hneq : ∀ (a : α), ι a ≠ a) (f : α → M) (hpair : ∀ (a : α), f (ι a) = -f a) : ∑ a : α, f a = 0

A fixed-point-free involution cancellation principle for finite sums.

In the barycentric subdivision proof, α is Equiv.Perm (Fin (n+2)), ι π = (swap i i+1).trans π, and f π is the corresponding internal face term.

theorem SphereOddDegree.AffineBarycentricSubdivision.internal_faces_cancel_for_index {α M : Type} [Fintype α] [AddCommGroup M] (ι : α → α) (hιι : Function.Involutive ι) (hneq : ∀ (a : α), ι a ≠ a) (T : α → M) (hT : ∀ (a : α), T (ι a) = -T a) : ∑ a : α, T a = 0

Internal barycentric boundary faces cancel for each fixed internal face index.

theorem SphereOddDegree.AffineBarycentricSubdivision.internal_faces_double_sum_cancel {ιx α M : Type} [Fintype ιx] [Fintype α] [AddCommGroup M] (swapFor : ιx → α → α) (hswap_invol : ∀ (i : ιx), Function.Involutive (swapFor i)) (hswap_ne : ∀ (i : ιx) (a : α), swapFor i a ≠ a) (T : α → ιx → M) (hpair : ∀ (i : ιx) (a : α), T (swapFor i a) i = -T a i) : ∑ a : α, ∑ i : ιx, T a i = 0

Double internal-face cancellation after summing over all internal face indices.

theorem SphereOddDegree.AffineBarycentricSubdivision.last_faces_reindex_of_equiv {α β M : Type} [Fintype α] [Fintype β] [AddCommMonoid M] (e : α ≃ β) (L : α → M) (Rhs : β → M) (h : ∀ (a : α), L a = Rhs (e a)) : ∑ a : α, L a = ∑ b : β, Rhs b

A finite reindexing principle for the last faces.

In the barycentric subdivision proof, α is the set of permutations of Fin (n+2) and β is the sigma type of a deleted boundary vertex and a permutation of the remaining vertices. The equivalence is intended to be π ↦ (π last, lastFacePermutation π).