Last-face sign identity for barycentric subdivision

This file supplies the sign lemma needed for the last-face part of the proof that barycentric subdivision commutes with the singular boundary.

The theorem is deliberately stated in the same flexible face-data form as the last-face affine identity: instead of first choosing a canonical deletion permutation, it assumes the data

• j : Fin (n+2), the deleted target vertex;
• ρ : Perm (Fin (n+1)), the induced permutation on the remaining vertices;
• hj : j = π last;
• hρ : ∀ t, j.succAbove (ρ t) = π (Fin.castSucc t).

This is exactly the data consumed by the affine last-face lemma. The theorem then proves

(-1)^(n+1) sign(π) = (-1)^j sign(ρ).

This module proves the permutation-sign identity used by the boundary-chain theorem.

def SphereOddDegree.AffineBarycentricSubdivision.lastVertex (n : ℕ) : Fin (n + 2)

The last vertex of Fin (n+2).

Equations

• SphereOddDegree.AffineBarycentricSubdivision.lastVertex n = ⟨n + 1, ⋯⟩

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.lastVertex_val (n : ℕ) : ↑(lastVertex n) = n + 1

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.extendLastPerm {n : ℕ} (ρ : Equiv.Perm (Fin (n + 1))) : Equiv.Perm (Fin (n + 2))

Extend a permutation of the first n+1 indices to a permutation of Fin (n+2) fixing the last index.

This uses Mathlib's viaFintypeEmbedding, so its sign is exactly the sign of ρ.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.extendLastPerm ρ = ρ.viaFintypeEmbedding Fin.castSuccOrderEmb.toEmbedding

@[simp]

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.insertLastPerm {n : ℕ} (j : Fin (n + 2)) : Equiv.Perm (Fin (n + 2))

The order-preserving insertion permutation that sends the last domain vertex to j and sends the first n+1 domain vertices to the remaining target vertices in increasing order.

It is implemented as:

1. finRotate (n+2), sending the last input position to 0 and shifting the other positions to successors;
2. j.cycleRange.symm, sending 0 to j and successors to j.succAbove _.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.insertLastPerm j = Equiv.trans (finRotate (n + 2)) (Equiv.symm j.cycleRange)

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.insertLastPerm_last {n : ℕ} (j : Fin (n + 2)) : (insertLastPerm j) (lastVertex n) = j

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.insertLastPerm_castSucc {n : ℕ} (j : Fin (n + 2)) (t : Fin (n + 1)) : (insertLastPerm j) t.castSucc = j.succAbove t

theorem SphereOddDegree.AffineBarycentricSubdivision.sign_insertLastPerm {n : ℕ} (j : Fin (n + 2)) : Equiv.Perm.sign (insertLastPerm j) = (-1) ^ (n + 1) * (-1) ^ ↑j

Sign of the insertion permutation.

theorem SphereOddDegree.AffineBarycentricSubdivision.factor_lastFace_of_faceData {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hj : j = π (lastVertex n)) (hρ : ∀ (t : Fin (n + 1)), j.succAbove (ρ t) = π t.castSucc) : π = Equiv.trans (extendLastPerm ρ) (insertLastPerm j)

theorem SphereOddDegree.AffineBarycentricSubdivision.permSign_units_last_face_of_faceData {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hj : j = π (lastVertex n)) (hρ : ∀ (t : Fin (n + 1)), j.succAbove (ρ t) = π t.castSucc) : (-1) ^ (n + 1) * Equiv.Perm.sign π = (-1) ^ ↑j * Equiv.Perm.sign ρ

Unit-valued last-face sign identity, in the face-data form used by the last-face affine identity.

theorem SphereOddDegree.AffineBarycentricSubdivision.permSign_int_last_face_of_faceData {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hj : j = π (lastVertex n)) (hρ : ∀ (t : Fin (n + 1)), j.succAbove (ρ t) = π t.castSucc) : (-1) ^ (n + 1) * Equiv.Perm.sign π = (-1) ^ ↑j * Equiv.Perm.sign ρ

Integer-valued last-face sign identity.

theorem SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff_last_face_of_faceData (R : Type) [CommRing R] {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) (ρ : Equiv.Perm (Fin (n + 1))) (hj : j = π (lastVertex n)) (hρ : ∀ (t : Fin (n + 1)), j.succAbove (ρ t) = π t.castSucc) : (-1) ^ (n + 1) * permSignCoeff R π = (-1) ^ ↑j * permSignCoeff R ρ

Coefficient-ring last-face sign identity. This is the version to use in the barycentric subdivision boundary computation.