Endpoint homotopies for the child-coordinate family

At the lower endpoint every child coordinate is negative, and at the upper endpoint every child coordinate is positive. Hence the straight-line segments to the corresponding shifted S5 reference lifts remain in the negative and positive orthants, respectively.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childMap_left_neg {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) (x : Realization p) (i : Fin p) : (childMap hp hA phi (C, SignedInterval.left)) x i < 0

The full child coordinate map is pointwise negative at the lower endpoint.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childMap_right_pos {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) (x : Realization p) (i : Fin p) : 0 < (childMap hp hA phi (C, SignedInterval.right)) x i

The full child coordinate map is pointwise positive at the upper endpoint.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.segment_ne_zero_of_coordinatewise_neg {p : ℕ} (hp : Nat.Prime p) {v w : Fin p → ℝ} (hv : ∀ (i : Fin p), v i < 0) (hw : ∀ (i : Fin p), w i < 0) (t : ↑(Set.Icc 0 1)) : (1 - ↑t) • v + ↑t • w ≠ 0

A convex combination of two coordinatewise-negative vectors is nonzero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.segment_ne_zero_of_coordinatewise_pos {p : ℕ} (hp : Nat.Prime p) {v w : Fin p → ℝ} (hv : ∀ (i : Fin p), 0 < v i) (hw : ∀ (i : Fin p), 0 < w i) (t : ↑(Set.Icc 0 1)) : (1 - ↑t) • v + ↑t • w ≠ 0

A convex combination of two coordinatewise-positive vectors is nonzero.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childLeftToNegativeReference {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : ZeroFreeHomotopy hp (childZeroFreeMap hp hA phi (C, SignedInterval.left) ⋯) (EquivariantPLPositiveRay.negativeReferenceZeroFreeMap hp)

Lower child map to negative shifted reference.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childRightToPositiveReference {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : ZeroFreeHomotopy hp (childZeroFreeMap hp hA phi (C, SignedInterval.right) ⋯) (EquivariantPLPositiveRay.positiveReferenceZeroFreeMap hp)

Upper child map to positive shifted reference.

Equations

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