Chart-map representations of relative-collar assignments

A collar assignment represents a compatible chart map when every decorated local vertex value is the chart-map value at the represented spatial point. This invariant is independent of the time coordinate. It therefore passes through collar composition and interval reversal, and two assignments representing the same chart map agree automatically on a composition seam.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.Represents {p N A B M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (V : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) : Prop

Every decorated local occurrence is evaluated through one chart of K at the represented spatial point.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.RepresentsAtTime {p N A B M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (V : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (t : ℝ) : Prop

Boundary-restricted version of Represents.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.Represents.atTime {p N A B M L : ℕ} {hp : Nat.Prime p} {C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L} {K : CompatibleRefinedChartHomotopy.ChartMap hp N} {V : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ} (h : Represents C K V) (t : ℝ) : RepresentsAtTime C K V t

An unrestricted representation restricts to either horizontal boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.value_eq_of_spatial_eq {p N : ℕ} {hp : Nat.Prime p} {A₀ B₀ M₀ L₀ A₁ B₁ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A₀ B₀ M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A₁ B₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hC : Represents C K VC) (hD : Represents D K VD) (a : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp C) (b : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp D) (hab : (ExplicitAffineRelativeCollar.Parameters.coverPoint hp C a).spatial = (ExplicitAffineRelativeCollar.Parameters.coverPoint hp D b).spatial) : VC ⟦a⟧ = VD ⟦b⟧

Two represented assignments for the same chart map agree whenever their geometric spatial points agree.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.seamCompatible {p N : ℕ} {hp : Nat.Prime p} {A₀ B₀ M₀ L₀ B₁ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A₀ B₀ M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp B₀ B₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hC : Represents C K VC) (hD : Represents D K VD) : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D VC VD

Representation by one chart map supplies the seam condition required by collar composition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.seamCompatible_of_boundary {p N : ℕ} {hp : Nat.Prime p} {A₀ B₀ M₀ L₀ B₁ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A₀ B₀ M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp B₀ B₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hC : RepresentsAtTime C K VC 1) (hD : RepresentsAtTime D K VD 0) : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D VC VD

Upper and lower boundary representations by the same chart map supply a composition seam.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.combinedGlobalVector_represents {p N : ℕ} {hp : Nat.Prime p} {N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hC : Represents C K VC) (hD : Represents D K VD) : Represents (ExplicitAffineRelativeCollarCompose.combinedCells C D) K (ExplicitAffineRelativeCollarAssignmentCompose.combinedGlobalVector C D VC VD ⋯)

Composition of represented vector assignments represents the same chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.combinedAssignment_represents {p N : ℕ} {hp : Nat.Prime p} {N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (ha : Represents C K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a)) (hb : Represents D K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) : Represents (ExplicitAffineRelativeCollarCompose.combinedCells C D) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b ⋯))

The combined assignment of two represented assignments again represents the same chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.combinedAssignment_upper_represents_right {p N : ℕ} {hp : Nat.Prime p} {N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (hb : RepresentsAtTime D K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b) 1) : RepresentsAtTime (ExplicitAffineRelativeCollarCompose.combinedCells C D) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b hseam)) 1

The upper boundary of a composed assignment is represented by the right component's upper boundary representation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.combinedAssignment_lower_represents_left {p N : ℕ} {hp : Nat.Prime p} {N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (ha : RepresentsAtTime C K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) 0) : RepresentsAtTime (ExplicitAffineRelativeCollarCompose.combinedCells C D) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b hseam)) 0

The lower boundary of a composed assignment is represented by the left component's lower boundary representation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.reverseGlobalVector_represents {p N A B M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (ha : Represents C K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a)) : Represents (ExplicitAffineRelativeCollarReverse.reverseCells C) K (ExplicitAffineRelativeCollarAssignmentReverse.reverseGlobalVector C a)

Reversal preserves representation because reflection fixes the spatial coordinate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.reverseAssignment_represents {p N A B M L : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L) (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (ha : Represents C K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a)) : Represents (ExplicitAffineRelativeCollarReverse.reverseCells C) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarReverse.reverseCells C) (ExplicitAffineRelativeCollarAssignmentReverse.reverseAssignment C a))

Reversed assignments represent the same chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.lower_boundary_represents_base {p : ℕ} (hp : Nat.Prime p) {N0 d : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N0) {K1 : CompatibleRefinedChartHomotopy.ChartMap hp (N0 + d)} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp (N0 + d) (K.refine d) K1) (L : ℕ) : RepresentsAtTime (RelativeCollarMiddlePrism.cellSystem hp (N0 + d) L) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp (N0 + d) L) (CompatibleRefinedChartHomotopyPrism.assignment hp J L)) 0

When the lower endpoint of a chart homotopy is a refinement of a base chart map, the complete lower prism boundary represents that base map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ChartMapCollarRepresentation.upper_boundary_represents_base {p : ℕ} (hp : Nat.Prime p) {N0 d : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N0) {K0 : CompatibleRefinedChartHomotopy.ChartMap hp (N0 + d)} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp (N0 + d) K0 (K.refine d)) (L : ℕ) : RepresentsAtTime (RelativeCollarMiddlePrism.cellSystem hp (N0 + d) L) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp (N0 + d) L) (CompatibleRefinedChartHomotopyPrism.assignment hp J L)) 1

When the upper endpoint is a refinement of a base chart map, the complete upper prism boundary represents that base map.