Equivariant zero-free coordinate homotopies

This file packages the continuous objects used by the unconditional S6 argument. The target is the full labelled coordinate representation Fin p → ℝ; prime symmetry acts simultaneously on the Fox--Neuwirth realization and by coordinate permutation on the target.

The crucial distinction is between avoiding the origin in the full coordinate representation and avoiding zero only in the deviation representation. The projected simultaneous-child-zero set is exactly the locus where the full coordinate map meets the origin.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.CoordinateMap {p : ℕ} : Type

Continuous coordinate-valued maps on the order-complex realization.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.CoordinateMap = NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.ContinuousCoordinateMap p

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.IsEquivariant (p : ℕ) (F : CoordinateMap) : Prop

Prime-equivariance of a continuous coordinate map.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.IsEquivariant p F = NRR.FoxNeuwirthOrderComplex.IsEquivariantCoordinateMap p F

structure NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.ZeroFreeMap {p : ℕ} (hp : Nat.Prime p) : Type

A continuous prime-equivariant coordinate map avoiding the origin.

• map : CoordinateMap

  The underlying continuous coordinate map.

• equivariant : IsEquivariant p self.map
• zeroFree (x : Realization p) : self.map x ≠ 0

structure NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.ZeroFreeHomotopy {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : ZeroFreeMap hp) : Type

A continuous equivariant homotopy through maps avoiding the origin.

• map : C(Realization p × ↑(Set.Icc 0 1), Fin p → ℝ)

  The continuous map on the realization times the unit interval defining the homotopy.

• map_zero (x : Realization p) : self.map (x, ⟨0, _proof_1⟩) = F₀.map x
• map_one (x : Realization p) : self.map (x, ⟨1, _proof_2⟩) = F₁.map x
• equivariant (g : ↥(PrimeSymmetry p)) (x : Realization p) (t : ↑(Set.Icc 0 1)) : self.map (g • x, t) = g • self.map (x, t)
• zeroFree (x : Realization p) (t : ↑(Set.Icc 0 1)) : self.map (x, t) ≠ 0

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.ZeroFreeHomotopy.refl {p : ℕ} (hp : Nat.Prime p) (F : ZeroFreeMap hp) : ZeroFreeHomotopy hp F F

The constant zero-free homotopy.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.ZeroFreeHomotopy.symm {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : ZeroFreeMap hp} (H : ZeroFreeHomotopy hp F₀ F₁) : ZeroFreeHomotopy hp F₁ F₀

Reverse a zero-free homotopy.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.ZeroFreeHomotopy.trans {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ F₂ : ZeroFreeMap hp} (H₀₁ : ZeroFreeHomotopy hp F₀ F₁) (H₁₂ : ZeroFreeHomotopy hp F₁ F₂) : ZeroFreeHomotopy hp F₀ F₂

Concatenate two zero-free homotopies.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.ZeroFreeHomotopy.segment {p : ℕ} {hp : Nat.Prime p} (F₀ F₁ : ZeroFreeMap hp) (hseg : ∀ (x : Realization p) (t : ↑(Set.Icc 0 1)), (1 - ↑t) • F₀.map x + ↑t • F₁.map x ≠ 0) : ZeroFreeHomotopy hp F₀ F₁

Straight-line homotopy, under a pointwise nonvanishing hypothesis.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childMap {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) : CoordinateMap

A coordinate map obtained by freezing the parent-body/interval parameter in the child test map.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childMap_equivariant {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) : IsEquivariant p (childMap hp hA phi z)

The frozen child map is prime-equivariant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childMap_zeroFree {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (hz : z ∈ ((orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ) (x : Realization p) : (childMap hp hA phi z) x ≠ 0

Outside the projected zero set, the frozen child coordinate map avoids the origin.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childZeroFreeMap {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (hz : z ∈ ((orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ) : ZeroFreeMap hp

The child map as a bundled zero-free equivariant map.

Equations

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