Finite cancellation for the boundary of a boundary

This module packages the elementary codimension-two cancellation used by the recursive relative subdivision cylinder. A sequential deletion is indexed by a first omitted vertex and a second vertex in the remaining ordered set. Reindexing by the corresponding ordered pair of distinct original vertices makes the cancellation involution simply swap the two vertices.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.DeletedVertexPair (n : ℕ) : Type

Ordered pairs of distinct vertices of an (n+2)-simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.DeletedVertexPair n = { z : Fin (n + 3) × Fin (n + 3) // z.1 ≠ z.2 }

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.deletedIndex {m : ℕ} (a b : Fin (m + 1)) (hab : a ≠ b) : Fin m

The index of b after deleting the distinct index a. This is the total inverse of a.succAbove on the complement of a, expressed without the newer partial Fin.predAbove API.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.deletedIndex a b hab = if hba : ↑b < ↑a then ⟨↑b, ⋯⟩ else ⟨↑b - 1, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.deletedIndex_val {m : ℕ} (a b : Fin (m + 1)) (hab : a ≠ b) : ↑(deletedIndex a b hab) = if ↑b < ↑a then ↑b else ↑b - 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.succAbove_deletedIndex {m : ℕ} (a b : Fin (m + 1)) (hab : a ≠ b) : a.succAbove (deletedIndex a b hab) = b

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.deletedIndex_succAbove {m : ℕ} (a : Fin (m + 1)) (k : Fin m) : deletedIndex a (a.succAbove k) ⋯ = k

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.sequentialDeletionEquiv (n : ℕ) : (_ : Fin (n + 3)) × Fin (n + 2) ≃ DeletedVertexPair n

A sequential deletion determines the two distinct vertices deleted from the original simplex.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.deletedVertexPairFintype (n : ℕ) : Fintype (DeletedVertexPair n)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.deletedVertexPairDecidableEq (n : ℕ) : DecidableEq (DeletedVertexPair n)

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.swapDeletedVertexPair (n : ℕ) : DeletedVertexPair n → DeletedVertexPair n

Swap the two deleted original vertices.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.swapDeletedVertexPair n z = ⟨((↑z).2, (↑z).1), ⋯⟩

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.swapDeletedVertexPair_involutive (n : ℕ) : Function.Involutive (swapDeletedVertexPair n)

Swapping deleted vertices is an involution.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.swapDeletedVertexPair_ne (n : ℕ) (z : DeletedVertexPair n) : swapDeletedVertexPair n z ≠ z

No ordered pair of distinct vertices is fixed by swapping.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.double_succAbove_eq (n : ℕ) (a b : Fin (n + 3)) (hab : a ≠ b) : (fun (i : Fin (n + 1)) => a.succAbove ((deletedIndex a b hab).succAbove i)) = fun (i : Fin (n + 1)) => b.succAbove ((deletedIndex b a ⋯).succAbove i)

The two orders of deleting distinct vertices induce the same ordered codimension-two face.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.doubleCofacePoint_eq (n : ℕ) (a b : Fin (n + 3)) (hab : a ≠ b) : (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => EquivariantPrismNonhorizontalCancellation.cofacePoint (n + 1) a (EquivariantPrismNonhorizontalCancellation.cofacePoint n (deletedIndex a b hab) x)) = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => EquivariantPrismNonhorizontalCancellation.cofacePoint (n + 1) b (EquivariantPrismNonhorizontalCancellation.cofacePoint n (deletedIndex b a ⋯) x)

Geometric coface maps are independent of the order in which two distinct vertices are deleted.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.double_faceSign_swap {R : Type} [CommRing R] (n : ℕ) (a b : Fin (n + 3)) (hab : a ≠ b) : SimplicialChain.faceSign a * SimplicialChain.faceSign (deletedIndex a b hab) = -(SimplicialChain.faceSign b * SimplicialChain.faceSign (deletedIndex b a ⋯))

The alternating signs of the two deletion orders are opposite.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.FiniteSimplexDoubleBoundary.double_boundary_weighted_zero {R X : Type} [CommRing R] (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 2)) → X) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) → R) : (∑ a : Fin (n + 3), SimplicialChain.faceSign a * ∑ k : Fin (n + 2), SimplicialChain.faceSign k * W fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => sigma (EquivariantPrismNonhorizontalCancellation.cofacePoint (n + 1) a (EquivariantPrismNonhorizontalCancellation.cofacePoint n k x))) = 0

Weighted finite form of boundary ∘ boundary = 0.