Assignment composition for endpoint-identified relative affine collars

The geometric composition of two collars is already available in ExplicitAffineRelativeCollarCompose. This file supplies the corresponding assignment layer.

An assignment is most conveniently built from an equivariant vector value on global vertices. For a composed collar, the value on each half is inherited from the corresponding component. The only additional hypothesis is literal agreement at every geometric seam vertex. Under that hypothesis the two local definitions descend through equality of combined geometric vertices.

The resulting combined assignment reconstructs the original component assignments on every local cell. Consequently any cellwise property stated only in terms of localVertexMap, in particular origin avoidance, is transported without a new geometric proof.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.assignmentOfEquivariantVector {p : ℕ} {hp : Nat.Prime p} {A B M L : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L) (V : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (hV : ∀ (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C), V (g • x) = g • V x) : ExplicitAffineRelativeCollar.Parameters.Assignment hp C

Construct a scalar quotient assignment from an equivariant vector value on global vertices.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.vectorValue_assignmentOfEquivariantVector {p : ℕ} {hp : Nat.Prime p} {A B M L : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B M L) (V : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (hV : ∀ (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C), V (g • x) = g • V x) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp C (assignmentOfEquivariantVector C V hV) x = V x

The assignment reconstructed from an equivariant vector has the prescribed vector value.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.leftCoverVertex {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp C) : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarCompose.combinedCells C D)

A local vertex occurrence from the left collar, embedded in the combined cover.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.leftCoverVertex C D s = (s.1, Sum.inl s.2.1, s.2.2)

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.rightCoverVertex {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp D) : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarCompose.combinedCells C D)

A local vertex occurrence from the right collar, embedded in the combined cover.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.rightCoverVertex C D s = (s.1, Sum.inr s.2.1, s.2.2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.coverPoint_leftCoverVertex {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp C) : ExplicitAffineRelativeCollar.Parameters.coverPoint hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (leftCoverVertex C D s) = ExplicitAffineRelativeCollarCompose.leftPoint (ExplicitAffineRelativeCollar.Parameters.coverPoint hp C s)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.coverPoint_rightCoverVertex {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp D) : ExplicitAffineRelativeCollar.Parameters.coverPoint hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (rightCoverVertex C D s) = ExplicitAffineRelativeCollarCompose.rightPoint (ExplicitAffineRelativeCollar.Parameters.coverPoint hp D s)

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) : Prop

Seam compatibility for two vector assignments. It is stated directly on geometric cover occurrences so it applies before either component is embedded into the combined quotient.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedCoverVector {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) → Fin p → ℝ

Piecewise vector value on decorated local occurrences of the combined collar.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedCoverVector C D VC VD (g, Sum.inl q, i) = VC ⟦(g, q, i)⟧
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedCoverVector C D VC VD (g, Sum.inr q, i) = VD ⟦(g, q, i)⟧

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedCoverVector_eq_of_coverPoint_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hseam : SeamCompatible C D VC VD) {a b : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (ExplicitAffineRelativeCollarCompose.combinedCells C D)} (hab : ExplicitAffineRelativeCollar.Parameters.coverPoint hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) a = ExplicitAffineRelativeCollar.Parameters.coverPoint hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) b) : combinedCoverVector C D VC VD a = combinedCoverVector C D VC VD b

Component compatibility and seam compatibility make the piecewise vector depend only on the combined geometric vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedGlobalVector {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hseam : SeamCompatible C D VC VD) : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) → Fin p → ℝ

Global combined vector obtained by descent from the piecewise cover value.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedGlobalVector_left {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hseam : SeamCompatible C D VC VD) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp C) : combinedGlobalVector C D VC VD hseam ⟦leftCoverVertex C D s⟧ = VC ⟦s⟧

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedGlobalVector_right {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hseam : SeamCompatible C D VC VD) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp D) : combinedGlobalVector C D VC VD hseam ⟦rightCoverVertex C D s⟧ = VD ⟦s⟧

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedGlobalVector_smul {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (VC : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C → Fin p → ℝ) (VD : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D → Fin p → ℝ) (hC : ∀ (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C), VC (g • x) = g • VC x) (hD : ∀ (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp D), VD (g • x) = g • VD x) (hseam : SeamCompatible C D VC VD) (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (ExplicitAffineRelativeCollarCompose.combinedCells C D)) : combinedGlobalVector C D VC VD hseam (g • x) = g • combinedGlobalVector C D VC VD hseam x

Equivariance of both component vector values is inherited by the combined vector.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (ExplicitAffineRelativeCollarCompose.combinedCells C D)

Compose two assignments whose vector values agree on every combined seam vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.localVertexMap_combinedAssignment_left {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (q : C.Cell) : ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) (Sum.inl q) = ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C a q

Local values on a left cell are reconstructed literally from the left assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.localVertexMap_combinedAssignment_right {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (q : D.Cell) : ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) (Sum.inr q) = ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D b q

Local values on a right cell are reconstructed literally from the right assignment.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.vectorValue_combinedAssignment_left_sample {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (s : C.VertexSlot) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (Sum.inl s.1, s.2)) = ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C s)

On a left local slot, the combined assignment reconstructs the left component vector.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.vectorValue_combinedAssignment_right_sample {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (s : D.VertexSlot) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (Sum.inr s.1, s.2)) = ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp D s)

On a right local slot, the combined assignment reconstructs the right component vector.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment_lowerFixed {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (G : Realization p → Fin p → ℝ) (hleft : ∀ (s : C.VertexSlot), ↑(C.slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C s) = G (C.slotPoint s).spatial) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C D).VertexSlot) : ↑((ExplicitAffineRelativeCollarCompose.combinedCells C D).slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) s) = G ((ExplicitAffineRelativeCollarCompose.combinedCells C D).slotPoint s).spatial

A lower-boundary value formula on the left component is preserved by composition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment_upperFixed {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (G : Realization p → Fin p → ℝ) (hright : ∀ (s : D.VertexSlot), ↑(D.slotPoint s).time = 1 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp D s) = G (D.slotPoint s).spatial) (s : (ExplicitAffineRelativeCollarCompose.combinedCells C D).VertexSlot) : ↑((ExplicitAffineRelativeCollarCompose.combinedCells C D).slotPoint s).time = 1 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) s) = G ((ExplicitAffineRelativeCollarCompose.combinedCells C D).slotPoint s).spatial

An upper-boundary value formula on the right component is preserved by composition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment_horizontalVertexFixed {p Nmid M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) (EC : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level Nmid M₀ L₀) (ED : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid A₁.level M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp EC.cells) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp ED.cells) (hseam : SeamCompatible EC.cells ED.cells (ExplicitAffineRelativeCollar.Parameters.vectorValue hp EC.cells a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp ED.cells b)) (hlower : ∀ (s : EC.cells.VertexSlot), ↑(EC.cells.slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp EC.cells a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp EC.cells s) = A₀.map (EC.cells.slotPoint s).spatial) (hupper : ∀ (s : ED.cells.VertexSlot), ↑(ED.cells.slotPoint s).time = 1 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp ED.cells b (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp ED.cells s) = A₁.map (ED.cells.slotPoint s).spatial) : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ (ExplicitAffineRelativeCollarCompose.endpointIdentifiedCollar EC ED) (combinedAssignment EC.cells ED.cells a b hseam)

Composition preserves the external horizontal endpoint values. Only the lower values of the left assignment and the upper values of the right assignment are needed; the common seam is handled separately by SeamCompatible.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment_avoidsOrigin {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (hC : ∀ (q : C.Cell), (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C a q).AvoidsOrigin) (hD : ∀ (q : D.Cell), (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D b q).AvoidsOrigin) (q : (ExplicitAffineRelativeCollarCompose.combinedCells C D).Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (combinedAssignment C D a b hseam) q).AvoidsOrigin

Cellwise origin avoidance is preserved under assignment composition.