Adjacent-swap sign lemma for barycentric subdivision

This file proves the sign part of the internal-face cancellation in the boundary computation for barycentric subdivision.

If τ is the adjacent transposition swapping positions i and i+1, then τ.trans π has the opposite sign from π. The final theorem is stated for the coefficient-ring sign convention used by permSignCoeff in BarycentricSubdivisionOperator.lean.

theorem SphereOddDegree.AffineBarycentricSubdivision.castSucc_ne_succ_adjacent {n : ℕ} (i : Fin (n + 1)) : i.castSucc ≠ i.succ

The adjacent entries i and i+1 in Fin (n+2) are distinct.

theorem SphereOddDegree.AffineBarycentricSubdivision.permSign_units_adjacent_swap {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) : Equiv.Perm.sign (Equiv.trans (Equiv.swap i.castSucc i.succ) π) = -Equiv.Perm.sign π

Unit-valued sign identity for left composition by the adjacent transposition swapping i and i+1.

The order is chosen to match the affine internal-swap lemma, where the swapped permutation is written

(Equiv.swap (Fin.castSucc i) (Fin.succ i)).trans π.

theorem SphereOddDegree.AffineBarycentricSubdivision.permSign_int_adjacent_swap {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) : ↑(Equiv.Perm.sign (Equiv.trans (Equiv.swap i.castSucc i.succ) π)) = -↑(Equiv.Perm.sign π)

Integer-valued version of permSign_units_adjacent_swap.

theorem SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff_adjacent_swap (R : Type) [CommRing R] {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) : permSignCoeff R (Equiv.trans (Equiv.swap i.castSucc i.succ) π) = -permSignCoeff R π

Coefficient-ring sign identity for the internal adjacent-swap cancellation.

This is the lemma needed to pair the internal boundary face coming from π with that coming from the adjacent-swapped permutation.