Route B, Step 2: the movable parameter space

This file packages the already existing boundary-relative scalar parameters as a finite-dimensional product of real lines. It also records the elementary coordinate-replacement and reconstruction lemmas needed by the incidence argument.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MovableParameterSpace {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

The finite-dimensional real parameter space of all movable scalar orbits.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.baseMovableParameters {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) : MovableParameterSpace hp C

Movable coordinates extracted from a full assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) : Parameters.Assignment hp C

Reconstruct the full equivariant assignment while retaining every frozen horizontal coordinate literally.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters_frozen {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) {q : Parameters.Parameter hp C} (hq : Parameters.IsFrozenParameter hp C q) : assignmentOfMovableParameters hp C base x q = base q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters_movable {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) (q : Parameters.MovableParameter hp C) : assignmentOfMovableParameters hp C base x ↑q = x q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignmentOf_baseMovableParameters {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) : assignmentOfMovableParameters hp C base (baseMovableParameters hp C base) = base

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.replaceCoordinate {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x : MovableParameterSpace hp C) (q : Parameters.MovableParameter hp C) (r : ℝ) : MovableParameterSpace hp C

Replace one movable scalar orbit and leave every other movable orbit fixed.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.replaceCoordinate hp C x q r = Function.update x q r

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.replaceCoordinate_same {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x : MovableParameterSpace hp C) (q : Parameters.MovableParameter hp C) (r : ℝ) : replaceCoordinate hp C x q r q = r

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.replaceCoordinate_other {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x : MovableParameterSpace hp C) {q q' : Parameters.MovableParameter hp C} (h : q' ≠ q) (r : ℝ) : replaceCoordinate hp C x q r q' = x q'

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignment_replaceCoordinate_frozen {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) (q : Parameters.MovableParameter hp C) (r : ℝ) {s : Parameters.Parameter hp C} (hs : Parameters.IsFrozenParameter hp C s) : assignmentOfMovableParameters hp C base (replaceCoordinate hp C x q r) s = base s

Replacing one movable coordinate has no effect on frozen endpoint data.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.vectorValue_assignmentOfMovableParameters_smul {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) (g : ↥(PrimeSymmetry p)) (v : Parameters.GlobalVertex hp C) : Parameters.vectorValue hp C (assignmentOfMovableParameters hp C base x) (g • v) = g • Parameters.vectorValue hp C (assignmentOfMovableParameters hp C base x) v

Every reconstructed full assignment remains prime-equivariant.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MovableClose {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x y : MovableParameterSpace hp C) (ε : ℝ) : Prop

Coordinatewise closeness in the movable product.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters_close {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x y : MovableParameterSpace hp C) {ε : ℝ} (hε : 0 < ε) (hxy : MovableClose hp C x y ε) : EquivariantPrismGenericPerturbation.AssignmentClose (assignmentOfMovableParameters hp C base x) (assignmentOfMovableParameters hp C base y) ε

Coordinatewise movable closeness lifts to coordinatewise closeness of the reconstructed full assignments.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.continuous_apply_movableParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : Parameters.MovableParameter hp C) : Continuous fun (x : MovableParameterSpace hp C) => x q

Evaluation at one movable coordinate is continuous in the product topology.

Continuity of reconstructed scalar coordinates

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.continuous_assignmentOfMovableParameters_apply {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : Parameters.Parameter hp C) : Continuous fun (x : MovableParameterSpace hp C) => assignmentOfMovableParameters hp C base x q

Every scalar coordinate of the reconstructed full assignment depends continuously on the movable product parameter.