Oriented boundary of the recursive one-step subdivision cylinder

The recursive cylinder is a cone over a triangulated boundary chain. This file proves its exact weighted boundary formula in two finite steps.

1. The triangulated boundary chain is closed. The upper barycentric boundary is moved to the original faces by oneStep_weighted_boundary; the recursively triangulated side boundaries are replaced by the induction hypothesis; codimension-two side terms cancel by double_boundary_weighted_zero.
2. The non-base facets of the cone are cones over the boundary of that closed boundary chain. Their weighted sum therefore vanishes, leaving precisely the cone-base chain.

The theorem is stated for arbitrary weights on ordered geometric vertex tuples. Taking the weight to be the characteristic function of one quotient-facet class gives the pointwise incidence identity needed by the global Fox--Neuwirth collar.

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.deleteTuple {X : Type} {n : ℕ} (v : Fin (n + 2) → X) (j : Fin (n + 2)) : Fin (n + 1) → X

Delete one entry from an ordered vertex tuple.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.deleteTuple v j i = v (j.succAbove i)

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.coneTuple {X : Type} {n : ℕ} (a : X) (v : Fin n → X) : Fin (n + 1) → X

Prepend a cone apex to an ordered base tuple.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.coneTuple a v i = Fin.cases a v i

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.facetTuple (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (j : Fin (d + 2)) : Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)

Ordered full facet of one recursive cylinder cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.fullBoundaryPairing (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) → R) : R

Alternating weighted boundary of the complete recursive cylinder chain.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.basePairing (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) → R) : R

Weighted cone-base chain.

Equations

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

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.tupleBoundaryWeight {R X : Type} [CommRing R] (d : ℕ) (W : (Fin d → X) → R) (v : Fin (d + 1) → X) : R

Boundary weight of one ordered d-simplex tuple.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.tupleBoundaryWeight d W v = ∑ j : Fin (d + 1), (-1) ^ ↑j * W fun (i : Fin d) => v (j.succAbove i)

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.BaseChainClosed (R : Type) [CommRing R] (d : ℕ) : Prop

The triangulated cone-base chain is closed in positive dimension.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.BaseChainClosed R 0 = True

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.facetTuple_succ_eq_coneTuple (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (j : Fin (d + 1)) : facetTuple d q j.succ = coneTuple (RelativeSubdivisionCylinderCombinatorics.apex d) fun (i : Fin d) => RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex d q (j.succAbove i)

Every non-base facet is the cone over the corresponding facet of the base tuple.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.facetTuple_zero_eq_base (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) : facetTuple d q 0 = RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex d q

The base facet is the declared triangulated-boundary simplex.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.faceSign_succ {R : Type} [CommRing R] {n : ℕ} (j : Fin (n + 1)) : SimplicialChain.faceSign j.succ = -(-1) ^ ↑j

Successor face signs differ from the corresponding base-boundary signs by a minus sign.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.radialPairing_eq_zero_of_baseClosed (R : Type) [CommRing R] (d : ℕ) (hclosed : BaseChainClosed R d) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) → R) : ∑ q : RelativeSubdivisionCylinderCombinatorics.Cell d, RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R d q * ∑ j : Fin (d + 1), SimplicialChain.faceSign j.succ * W (facetTuple d q j.succ) = 0

Closedness of the cone-base chain kills every radial cone facet.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.fullBoundaryPairing_eq_base_of_closed (R : Type) [CommRing R] (d : ℕ) (hclosed : BaseChainClosed R d) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) → R) : fullBoundaryPairing R d W = basePairing R d W

Once the base boundary chain is closed, the full cylinder boundary is exactly its cone-base chain.

Recursive closedness of the cone-base chain

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.sideTuple (d : ℕ) (k : Fin (d + 2)) (v : Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) : Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)

Embed an ordered tuple into the side opposite k.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.sideTuple d k v i = NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sidePoint d k (v i)

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.delete_sideTuple (d : ℕ) (k : Fin (d + 2)) (v : Fin (d + 2) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) (j : Fin (d + 2)) : sideTuple d k (deleteTuple v j) = fun (i : Fin (d + 1)) => RelativeSubdivisionCylinderCombinatorics.sidePoint d k (v (j.succAbove i))

Deleting a vertex from an embedded side tuple commutes with the side embedding.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.upper_boundary_pairing (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)) → R) : ∑ pi : Equiv.Perm (Fin (d + 2)), SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R pi * tupleBoundaryWeight (d + 1) W (RelativeSubdivisionCylinderCombinatorics.upperBoundaryVertex (d + 1) pi) = ∑ k : Fin (d + 2), SimplicialChain.faceSign k * ∑ rho : Equiv.Perm (Fin (d + 1)), SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R rho * W fun (i : Fin (d + 1)) => RelativeSubdivisionCylinderCombinatorics.sidePoint d k (RelativeSubdivisionCylinderCombinatorics.upperBoundaryVertex d rho i)

Boundary of an upper barycentric tuple, expressed on the original boundary faces.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.delete_lowerBoundaryVertex_eq_side (d : ℕ) (k : Fin (d + 2)) : deleteTuple (RelativeSubdivisionCylinderCombinatorics.lowerBoundaryVertex (d + 1)) k = sideTuple d k (RelativeSubdivisionCylinderCombinatorics.lowerBoundaryVertex d)

A lower boundary face is the lower boundary tuple in the corresponding spatial side.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.recursive_side_side_zero (R : Type) [CommRing R] (n : ℕ) (W : (Fin (n + 2) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 2)) × ↑(Set.Icc 0 1)) → R) : (∑ k : Fin (n + 3), SimplicialChain.faceSign k * ∑ l : Fin (n + 2), SimplicialChain.faceSign l * ∑ q : RelativeSubdivisionCylinderCombinatorics.Cell n, RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R n q * W fun (i : Fin (n + 2)) => RelativeSubdivisionCylinderCombinatorics.sidePoint (n + 1) k (RelativeSubdivisionCylinderCombinatorics.sidePoint n l (RelativeSubdivisionCylinderCombinatorics.vertex n q i))) = 0

A recursively triangulated codimension-two side occurs twice with opposite total sign.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.lowerPairing_tupleBoundaryWeight (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)) → R) : RelativeSubdivisionCylinderCombinatorics.Oriented.lowerPairing R (d + 1) (tupleBoundaryWeight (d + 1) W) = ∑ k : Fin (d + 2), SimplicialChain.faceSign k * RelativeSubdivisionCylinderCombinatorics.Oriented.lowerPairing R d fun (v : Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) => W (sideTuple d k v)

The lower coarse boundary of a tuple boundary is the signed sum of the lower boundaries inside the ambient spatial sides.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.upperPairing_tupleBoundaryWeight (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)) → R) : RelativeSubdivisionCylinderCombinatorics.Oriented.upperPairing R (d + 1) (tupleBoundaryWeight (d + 1) W) = ∑ k : Fin (d + 2), SimplicialChain.faceSign k * RelativeSubdivisionCylinderCombinatorics.Oriented.upperPairing R d fun (v : Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) => W (sideTuple d k v)

The upper barycentric boundary of a tuple boundary is the signed sum of the upper boundaries inside the ambient spatial sides.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.sidePairing_tupleBoundaryWeight (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)) → R) : RelativeSubdivisionCylinderCombinatorics.Oriented.sidePairing R d (tupleBoundaryWeight (d + 1) W) = -∑ k : Fin (d + 2), SimplicialChain.faceSign k * fullBoundaryPairing R d fun (v : Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) => W (sideTuple d k v)

Taking the boundary of every recursive side cell gives the negative signed sum of the complete lower-dimensional cylinder boundaries in the ambient spatial sides.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.neg_weighted_sidePairing_eq_recursive_side_side (R : Type) [CommRing R] (n : ℕ) (W : (Fin (n + 2) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 2)) × ↑(Set.Icc 0 1)) → R) : (-∑ k : Fin (n + 3), SimplicialChain.faceSign k * RelativeSubdivisionCylinderCombinatorics.Oriented.sidePairing R n fun (v : Fin (n + 2) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) × ↑(Set.Icc 0 1)) => W (sideTuple (n + 1) k v)) = ∑ k : Fin (n + 3), SimplicialChain.faceSign k * ∑ l : Fin (n + 2), SimplicialChain.faceSign l * ∑ q : RelativeSubdivisionCylinderCombinatorics.Cell n, RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R n q * W fun (i : Fin (n + 2)) => RelativeSubdivisionCylinderCombinatorics.sidePoint (n + 1) k (RelativeSubdivisionCylinderCombinatorics.sidePoint n l (RelativeSubdivisionCylinderCombinatorics.vertex n q i))

Expanding the remaining negative weighted recursive-side sum produces exactly the codimension-two side-side sum.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.baseChainClosed (R : Type) [CommRing R] (d : ℕ) : BaseChainClosed R d

The triangulated boundary chain of the recursive cylinder is closed in every dimension.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderBoundary.fullBoundaryPairing_eq_base (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) → R) : fullBoundaryPairing R d W = basePairing R d W

Exact arbitrary-weight boundary formula for the recursive one-step cylinder.