Projection of the simultaneous child-zero set

For a compact prime configuration model, the simultaneous child-zero locus is closed in a compact space. Its projection to the parent-body/parameter cylinder is therefore compact and closed. The strict endpoint signs of a nice multivalued function show that this projection misses both endpoint boundaries. These facts provide the analytic and point-set-topological input to the separator construction. The cobordism theorem establishes the required lower and upper regions of the complement.

def NRR.PrimeConfigurationModel.projectedAllChildrenZeroSet {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : Set (BodySpace K A × ↑SignedInterval)

Projection of the simultaneous child-zero locus to the parent-body/parameter cylinder.

Equations

• M.projectedAllChildrenZeroSet hA φ = {z : NRR.BodySpace K A × ↑NRR.SignedInterval | ∃ (x : M.Point), ((z.1, x), z.2) ∈ M.allChildrenZeroSet hA φ}

theorem NRR.PrimeConfigurationModel.mem_projectedAllChildrenZeroSet_iff {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) : z ∈ M.projectedAllChildrenZeroSet hA φ ↔ ∃ (x : M.Point), ∀ (i : Fin p), φ.Zero (EMP.VariableBody.child M.sites hA ⋯ (z.1, x) i) z.2

Membership in the projected zero set is exactly the existence of one configuration for which all canonical children are zeros at the common parameter.

theorem NRR.PrimeConfigurationModel.isCompact_allChildrenZeroSet {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : IsCompact (M.allChildrenZeroSet hA φ)

The simultaneous zero locus in the total configuration cylinder is compact.

theorem NRR.PrimeConfigurationModel.isCompact_projectedAllChildrenZeroSet {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : IsCompact (M.projectedAllChildrenZeroSet hA φ)

The projected simultaneous-zero set is compact.

theorem NRR.PrimeConfigurationModel.isClosed_projectedAllChildrenZeroSet {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : IsClosed (M.projectedAllChildrenZeroSet hA φ)

The projected simultaneous-zero set is closed.

theorem NRR.PrimeConfigurationModel.not_mem_projectedAllChildrenZeroSet_left {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : (C, SignedInterval.left) ∉ M.projectedAllChildrenZeroSet hA φ

No projected simultaneous zero occurs at the lower endpoint.

theorem NRR.PrimeConfigurationModel.not_mem_projectedAllChildrenZeroSet_right {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : (C, SignedInterval.right) ∉ M.projectedAllChildrenZeroSet hA φ

No projected simultaneous zero occurs at the upper endpoint.

theorem NRR.PrimeConfigurationModel.disjoint_signedBottom_projectedAllChildrenZeroSet {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : Disjoint (signedBottom (BodySpace K A)) (M.projectedAllChildrenZeroSet hA φ)

The bottom boundary is disjoint from the projected simultaneous-zero set.

theorem NRR.PrimeConfigurationModel.disjoint_signedTop_projectedAllChildrenZeroSet {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : Disjoint (signedTop (BodySpace K A)) (M.projectedAllChildrenZeroSet hA φ)

The top boundary is disjoint from the projected simultaneous-zero set.