Separators from locally constant obstruction values

A mod-prime zero count is naturally defined only away from the projected zero set. If that count is locally constant on the complement, takes one value along the bottom boundary, and takes a different value along the top boundary, then its value classes split the complement into the two open regions required by TopBottomComplement.

This construction avoids any local path-connectedness assumption on the base hyperspace.

structure NRR.ComplementObstructionValue (X : Type u_3) [TopologicalSpace X] (carrier : Set (X × ↑SignedInterval)) (I : Type u_4) : Type (max u_3 u_4)

A locally constant invariant on the complement of a proposed separator carrier.

• value (z : X × ↑SignedInterval) : z ∈ carrierᶜ → I

  Value of the obstruction at a point outside the carrier.

• lowerValue : I

  Value selecting the lower side.

• locally_constant (z : X × ↑SignedInterval) (hz : z ∈ carrierᶜ) : ∃ (U : Set (X × ↑SignedInterval)) (hUout : U ⊆ carrierᶜ), IsOpen U ∧ z ∈ U ∧ ∀ (w : X × ↑SignedInterval) (hw : w ∈ U), self.value w ⋯ = self.value z hz

  Every complement point has an ambient open neighborhood, still in the complement, on which the obstruction value is constant.

• bottom_outside : signedBottom X ⊆ carrierᶜ

  The bottom boundary is outside the carrier.

• top_outside : signedTop X ⊆ carrierᶜ

  The top boundary is outside the carrier.

• bottom_value (x : X) : self.value (x, SignedInterval.left) ⋯ = self.lowerValue

  The obstruction has the selected lower value at every bottom point.

• top_value_ne (x : X) : self.value (x, SignedInterval.right) ⋯ ≠ self.lowerValue

  The obstruction differs from the lower value at every top point.

def NRR.ComplementObstructionValue.lower {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : Set (X × ↑SignedInterval)

Complement points carrying the distinguished lower value.

Equations

• D.lower = {z : X × ↑NRR.SignedInterval | ∃ (hz : z ∈ carrierᶜ), D.value z hz = D.lowerValue}

def NRR.ComplementObstructionValue.upper {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : Set (X × ↑SignedInterval)

Complement points carrying any other value.

Equations

• D.upper = {z : X × ↑NRR.SignedInterval | ∃ (hz : z ∈ carrierᶜ), D.value z hz ≠ D.lowerValue}

theorem NRR.ComplementObstructionValue.isOpen_lower {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : IsOpen D.lower

The lower value class is open in the ambient cylinder.

theorem NRR.ComplementObstructionValue.isOpen_upper {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : IsOpen D.upper

The union of all other value classes is open in the ambient cylinder.

theorem NRR.ComplementObstructionValue.disjoint_lower_upper {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : Disjoint D.lower D.upper

The two value regions are disjoint.

theorem NRR.ComplementObstructionValue.compl_eq {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : carrierᶜ = D.lower ∪ D.upper

The complement is exactly the union of the two value regions.

theorem NRR.ComplementObstructionValue.bottom_subset_lower {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : signedBottom X ⊆ D.lower

Bottom points belong to the lower value region.

theorem NRR.ComplementObstructionValue.top_subset_upper {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : signedTop X ⊆ D.upper

Top points belong to the upper value region.

def NRR.ComplementObstructionValue.toTopBottomComplement {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) : TopBottomComplement X carrier

A locally constant obstruction value constructs the required complement decomposition.

Equations

• D.toTopBottomComplement = { lower := D.lower, upper := D.upper, isOpen_lower := ⋯, isOpen_upper := ⋯, disjoint_lower_upper := ⋯, compl_eq := ⋯, bottom_subset_lower := ⋯, top_subset_upper := ⋯ }

def NRR.ComplementObstructionValue.toTopBottomSeparator {X : Type u_1} {I : Type u_2} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : ComplementObstructionValue X carrier I) (hcarrier : IsClosed carrier) : TopBottomSeparator X

Adding closedness of the carrier gives a top--bottom separator.

Equations

• D.toTopBottomSeparator hcarrier = D.toTopBottomComplement.toSeparator hcarrier