Reversal of an endpoint-identified relative affine collar

Reflection in the interval coordinate exchanges the two horizontal boundaries. To retain the standard boundary convention upper - lower, all top-cell coefficients are negated. This module performs that construction at the level of explicit affine cells, quotient facets, pointwise incidence, and endpoint-chain identification.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) : EquivariantPrismVertexParameters.CylinderPoint p

Reflection of the realization cylinder in its interval coordinate.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint z = { spatial := z.spatial, time := ⟨1 - ↑z.time, ⋯⟩ }

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint_spatial {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) : (reflectPoint z).spatial = z.spatial

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint_time {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) : ↑(reflectPoint z).time = 1 - ↑z.time

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint_involutive {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) : reflectPoint (reflectPoint z) = z

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint_injective {p : ℕ} : Function.Injective reflectPoint

Reflection is injective.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflectPoint_smul {p : ℕ} (g : ↥(PrimeSymmetry p)) (z : EquivariantPrismVertexParameters.CylinderPoint p) : reflectPoint (g • z) = g • reflectPoint z

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverseCells {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₁ N₀ M L

Reverse the affine cells and negate their oriented coefficients.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverse_facetSignature {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (o : C.FacetOccurrence) : (reverseCells C).facetSignature o = fun (i : Fin p) => reflectPoint (C.facetSignature o i)

Reversal carries original facet signatures to reflected signatures.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverse_facetSetoid_iff {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a b : C.FacetOccurrence) : (reverseCells C).facetSetoid a b ↔ C.facetSetoid a b

The facet orbit relations before and after reflection coincide.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.facetEquiv {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) : (reverseCells C).Facet ≃ C.Facet

Canonical equivalence between reflected and original quotient facets.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.facetEquiv_facetClass {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (o : C.FacetOccurrence) : (facetEquiv C) ((reverseCells C).facetClass o) = C.facetClass o

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverse_facetIncidence {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (s : (reverseCells C).Facet) : (reverseCells C).facetIncidence s = -C.facetIncidence ((facetEquiv C) s)

Reflection negates every pointwise facet incidence.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverse_isLower_iff_isUpper {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (s : (reverseCells C).Facet) : (reverseCells C).IsLowerFacet s ↔ C.IsUpperFacet ((facetEquiv C) s)

Lower-horizontal reflected facets are precisely upper-horizontal original facets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverse_isUpper_iff_isLower {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (s : (reverseCells C).Facet) : (reverseCells C).IsUpperFacet s ↔ C.IsLowerFacet ((facetEquiv C) s)

Upper-horizontal reflected facets are precisely lower-horizontal original facets.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverseCollar {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N₁ N₀ M L

Reverse a pointwise relative affine collar.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverseCollar_cells {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) : (reverseCollar C).cells = reverseCells C.cells

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflect_lowerCylinderPoint {p : ℕ} (x : Realization p) : reflectPoint (ExplicitAffineRelativeCollar.lowerCylinderPoint x) = ExplicitAffineRelativeCollar.upperCylinderPoint x

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reflect_upperCylinderPoint {p : ℕ} (x : Realization p) : reflectPoint (ExplicitAffineRelativeCollar.upperCylinderPoint x) = ExplicitAffineRelativeCollar.lowerCylinderPoint x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarReverse.reverseEndpointCollar {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M L) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₁ N₀ M L

Reverse an endpoint-identified collar.

Equations

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