Recursive one-step subdivision cylinders

This module gives the explicit finite cell and vertex formulas for the relative triangulation of Delta d x I whose lower boundary is the coarse simplex and whose upper boundary is its first barycentric subdivision.

The construction is recursive. Triangulate the boundary of the prism by one coarse lower simplex, all barycentric top simplices, and recursively triangulated side cylinders. Every boundary simplex is then coned to the central point (barycenter, 1 / 2).

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Cell : ℕ → Type

Top cells of the recursive cone triangulation of Delta d x I.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Cell 0 = (Unit ⊕ Equiv.Perm (Fin 1))

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.cellDecidableEq (d : ℕ) : DecidableEq (Cell d)

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.cellDecidableEq d = Classical.decEq (NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Cell d)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.cellFintype (d : ℕ) : Fintype (Cell d)

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.cellFintype 0 = id inferInstance
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.cellFintype d.succ = id inferInstance

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.lowerCell (d : ℕ) : Cell d

The cell coned from the coarse lower simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.lowerCell 0 = Sum.inl ()
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.lowerCell d.succ = Sum.inl ()

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.upperCell (d : ℕ) : Equiv.Perm (Fin (d + 1)) → Cell d

The cell coned from one top barycentric simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.upperCell 0 pi = Sum.inr pi
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.upperCell n.succ pi = Sum.inr (Sum.inl pi)

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sideCell (d : ℕ) (k : Fin (d + 2)) (q : Cell d) : Cell (d + 1)

A cell coned from a recursively triangulated side face.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sideCell d k q = Sum.inr (Sum.inr (k, q))

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.apex (d : ℕ) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)

The central cone point.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.lowerBoundaryVertex (d : ℕ) (i : Fin (d + 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)

Coarse lower-boundary vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.upperBoundaryVertex (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (i : Fin (d + 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)

Barycentric upper-boundary vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sidePoint (d : ℕ) (k : Fin (d + 2)) (z : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)

Embed a point of a lower-dimensional cylinder into the side opposite k.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sidePoint d k z = (SphereOddDegree.FiniteSimplex.map k.succAbove z.1, z.2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sidePoint_spatial_succAbove (d : ℕ) (k : Fin (d + 2)) (z : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) (i : Fin (d + 1)) : (sidePoint d k z).1 (k.succAbove i) = z.1 i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sidePoint_spatial_deleted (d : ℕ) (k : Fin (d + 2)) (z : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) : (sidePoint d k z).1 k = 0

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

Ordered vertices of a recursive cylinder cell.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_zero (d : ℕ) (q : Cell d) : vertex d q 0 = apex d

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_succ_lower (d : ℕ) (j : Fin (d + 1)) : vertex d (lowerCell d) j.succ = lowerBoundaryVertex d j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_succ_upper (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (j : Fin (d + 1)) : vertex d (upperCell d pi) j.succ = upperBoundaryVertex d pi j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_succ_side (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (j : Fin (d + 2)) : vertex (d + 1) (sideCell d k q) j.succ = sidePoint d k (vertex d q j)

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.spatialPoint (d : ℕ) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)

Spatial barycentric interpolation of a recursive cylinder cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.timePoint (d : ℕ) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(Set.Icc 0 1)

Time barycentric interpolation of a recursive cylinder cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart (d : ℕ) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)

Affine chart of one recursive one-step cylinder cell.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_vertex (d : ℕ) (q : Cell d) (i : Fin (d + 2)) : chart d q (SphereOddDegree.FiniteSimplex.vertex i) = vertex d q i

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_spatial_affine (d : ℕ) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (c : Fin (d + 1)) : (chart d q w).1 c = ∑ i : Fin (d + 2), w i * (vertex d q i).1 c

Every spatial coordinate is the barycentric interpolation of declared vertices.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_time_affine (d : ℕ) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(chart d q w).2 = ∑ i : Fin (d + 2), w i * ↑(vertex d q i).2

The time coordinate is the barycentric interpolation of declared vertex times.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.timePoint_lower (d : ℕ) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(timePoint d (lowerCell d) w) = w 0 / 2

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.timePoint_upper (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(timePoint d (upperCell d pi) w) = 1 - w 0 / 2

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.timePoint_side (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 2))) : ↑(timePoint (d + 1) (sideCell d k q) w) = w 0 / 2 + ∑ i : Fin (d + 2), w i.succ * ↑(vertex d q i).2

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.spatialPoint_lower_coord (d : ℕ) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (c : Fin (d + 1)) : (spatialPoint d (lowerCell d) w) c = w 0 * (SphereOddDegree.AffineBarycentricSubdivision.deltaBarycenter d) c + w c.succ

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.spatialPoint_upper_coord (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (c : Fin (d + 1)) : (spatialPoint d (upperCell d pi) w) c = w 0 * (SphereOddDegree.AffineBarycentricSubdivision.deltaBarycenter d) c + ∑ i : Fin (d + 1), w i.succ * (SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter d pi i) c

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.spatialPoint_side_missing_coord (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 2))) : (spatialPoint (d + 1) (sideCell d k q) w) k = w 0 * (SphereOddDegree.AffineBarycentricSubdivision.deltaBarycenter (d + 1)) k

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_lower_injective (d : ℕ) : Function.Injective (chart d (lowerCell d))

The lower cone simplex is nondegenerate.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_upper_injective (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) : Function.Injective (chart d (upperCell d pi))

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_injective_of_chart_injective (d : ℕ) (q : Cell d) (hchart : Function.Injective (chart d q)) : Function.Injective (vertex d q)

Pairwise distinct vertices follow from injectivity of the affine chart.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.lowerFacet_classification (d : ℕ) (q : Cell d) (j : Fin (d + 2)) (h : ∀ (i : Fin (d + 1)), ↑(vertex d q (j.succAbove i)).2 = 0) : q = lowerCell d ∧ j = 0

A facet is entirely at time zero exactly for the coarse lower base facet.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.upperFacet_classification (d : ℕ) (q : Cell d) (j : Fin (d + 2)) (h : ∀ (i : Fin (d + 1)), ↑(vertex d q (j.succAbove i)).2 = 1) : j = 0 ∧ ∃ (pi : Equiv.Perm (Fin (d + 1))), q = upperCell d pi

A facet is entirely at time one exactly for an upper barycentric base facet.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sum_succ_eq_one_sub (n : ℕ) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : ∑ i : Fin (n + 1), w i.succ = 1 - w 0

The coordinates after the leading cone coordinate sum to 1 - w 0.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.succ_eq_zero_of_zero_eq_one (n : ℕ) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) (h0 : w 0 = 1) (i : Fin (n + 1)) : w i.succ = 0

At the cone apex all tail coordinates vanish.

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.coneTail {n : ℕ} (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)

Normalize the tail barycentric coordinates away from the cone apex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.coneTail_apply {n : ℕ} (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) (hw : w 0 ≠ 1) (i : Fin (n + 1)) : (coneTail w) i = w i.succ / (1 - w 0)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.sidePoint_time (d : ℕ) (k : Fin (d + 2)) (z : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)) : (sidePoint d k z).2 = z.2

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.spatialPoint_side_succAbove_decompose (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 2))) (hw : w 0 ≠ 1) (c : Fin (d + 1)) : (spatialPoint (d + 1) (sideCell d k q) w) (k.succAbove c) = w 0 * (SphereOddDegree.AffineBarycentricSubdivision.deltaBarycenter (d + 1)) (k.succAbove c) + (1 - w 0) * (spatialPoint d q (coneTail w)) c

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.timePoint_side_decompose (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 2))) (hw : w 0 ≠ 1) : ↑(timePoint (d + 1) (sideCell d k q) w) = w 0 / 2 + (1 - w 0) * ↑(timePoint d q (coneTail w))

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_side_injective (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (hq : Function.Injective (chart d q)) : Function.Injective (chart (d + 1) (sideCell d k q))

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.chart_injective_all (d : ℕ) (q : Cell d) : Function.Injective (chart d q)

Every recursive one-step cylinder chart is injective.

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_injective_all (d : ℕ) (q : Cell d) : Function.Injective (vertex d q)

Every recursive cylinder cell has pairwise distinct ordered vertices.

def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt (d : ℕ) : Cell d → ℤ

Integral orientation coefficient of a recursive cylinder top cell.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt 0 (Sum.inl val) = -1
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt 0 (Sum.inr pi) = ↑(Equiv.Perm.sign pi)
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt _d.succ (Sum.inl val) = -1
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt _d.succ (Sum.inr (Sum.inl pi)) = ↑(Equiv.Perm.sign pi)

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient (R : Type) [CommRing R] (d : ℕ) : Cell d → R

Orientation coefficient with values in an arbitrary commutative ring.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R 0 (Sum.inl val) = -1
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R 0 (Sum.inr pi) = SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R pi
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R _d.succ (Sum.inl val) = -1
• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient R _d.succ (Sum.inr (Sum.inl pi)) = SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R pi

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt_lower (d : ℕ) : coefficientInt d (lowerCell d) = -1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt_upper (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) : coefficientInt d (upperCell d pi) = ↑(Equiv.Perm.sign pi)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficientInt_side (d : ℕ) (k : Fin (d + 2)) (q : Cell d) : coefficientInt (d + 1) (sideCell d k q) = -(-1) ^ ↑k * coefficientInt d q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient_lower (R : Type) [CommRing R] (d : ℕ) : coefficient R d (lowerCell d) = -1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient_upper (R : Type) [CommRing R] (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) : coefficient R d (upperCell d pi) = SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R pi

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.coefficient_side (R : Type) [CommRing R] (d : ℕ) (k : Fin (d + 2)) (q : Cell d) : coefficient R (d + 1) (sideCell d k q) = -(-1) ^ ↑k * coefficient R d q

noncomputable def NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex (d : ℕ) (q : Cell d) (i : Fin (d + 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d) × ↑(Set.Icc 0 1)

Ordered vertex signature of the cone-base facet.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex d q i = NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex d q i.succ

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex_lower (d : ℕ) (i : Fin (d + 1)) : baseFacetVertex d (lowerCell d) i = lowerBoundaryVertex d i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex_upper (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (i : Fin (d + 1)) : baseFacetVertex d (upperCell d pi) i = upperBoundaryVertex d pi i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetVertex_side (d : ℕ) (k : Fin (d + 2)) (q : Cell d) (i : Fin (d + 2)) : baseFacetVertex (d + 1) (sideCell d k q) i = sidePoint d k (vertex d q i)

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

Weighted pairing with the triangulated boundary simplex opposite the cone apex.

Equations

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

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

The lower coarse boundary contribution.

Equations

• NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.lowerPairing R d W = -W (NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.lowerBoundaryVertex d)

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

The upper barycentric-subdivision boundary contribution.

Equations

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

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

Recursive side-boundary contribution in positive dimension.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetPairing_zero (R : Type) [CommRing R] (W : (Fin 1 → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta 0) × ↑(Set.Icc 0 1)) → R) : baseFacetPairing R 0 W = lowerPairing R 0 W + upperPairing R 0 W

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.Oriented.baseFacetPairing_succ (R : Type) [CommRing R] (d : ℕ) (W : (Fin (d + 2) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1)) × ↑(Set.Icc 0 1)) → R) : baseFacetPairing R (d + 1) W = lowerPairing R (d + 1) W + upperPairing R (d + 1) W + sidePairing R d W

theorem NRR.FoxNeuwirthOrderComplex.RelativeSubdivisionCylinderCombinatorics.vertex_eq_lowerBoundaryVertex_of_time_eq_zero (d : ℕ) (q : Cell d) (i : Fin (d + 2)) : ↑(vertex d q i).2 = 0 → ∃ (j : Fin (d + 1)), vertex d q i = lowerBoundaryVertex d j