Reversal of assignments on relative affine collars #
Reflection changes only the time coordinate of a collar vertex. Therefore an assignment on the original collar can be transported to the reversed collar by using the same decorated local occurrence. Injectivity of interval reflection proves that the transported cover value descends to reversed global vertices. Local vertex maps are unchanged, so origin avoidance is preserved literally.
def
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.originalCoverVertex
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarReverse.reverseCells C))
:
A reversed local occurrence, viewed as the corresponding original occurrence.
Equations
Instances For
@[simp]
theorem
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.coverPoint_reverse
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarReverse.reverseCells C))
:
Reversed cover points are reflections of the original cover points.
noncomputable def
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.originalGlobalVertex
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarReverse.reverseCells C))
:
The original global vertex represented by a reversed local occurrence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseCoverVector
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
(s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarReverse.reverseCells C))
:
Piecewise value used for descent to reversed global vertices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseCoverVector_eq_of_coverPoint_eq
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
{s t : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarReverse.reverseCells C)}
(hst :
ExplicitAffineRelativeCollar.Parameters.coverPoint hp (ExplicitAffineRelativeCollarReverse.reverseCells C) s = ExplicitAffineRelativeCollar.Parameters.coverPoint hp (ExplicitAffineRelativeCollarReverse.reverseCells C) t)
:
Equality of reflected geometric vertices implies equality of their original quotient vertices.
noncomputable def
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseGlobalVector
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
:
Descended vector assignment on the reversed collar.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseGlobalVector_mk
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
(s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarReverse.reverseCells C))
:
theorem
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseGlobalVector_smul
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
(g : ↥(PrimeSymmetry p))
(x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (ExplicitAffineRelativeCollarReverse.reverseCells C))
:
Reversal preserves prime equivariance.
noncomputable def
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseAssignment
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
:
Assignment transported to the reversed cell system.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.localVertexMap_reverseAssignment
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
(q : C.Cell)
:
Reversal does not change any local target vertex value.
theorem
NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentReverse.reverseAssignment_avoidsOrigin
{p N₀ N₁ M L : ℕ}
{hp : Nat.Prime p}
(C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L)
(a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C)
(ha : ∀ (q : C.Cell), (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C a q).AvoidsOrigin)
(q : (ExplicitAffineRelativeCollarReverse.reverseCells C).Cell)
:
Cellwise origin avoidance is preserved under reversal.