Pointed back-and-forth restriction to a fiber

The converse of the back-and-forth assembly, in pointed form and with the owner row retained. For rows r : R, s : S, a label τ, and component tuples ā : Fin k → C r τ, b̄ : Fin k → D s τ, write rowPts r ā for the assembled tuple (row r, pt r τ (ā 0), …) of length k + 1.

Theorem (bfEquiv_restrict_pointed): if rowPts r ā ≡_β rowPts s b̄ in the assembled language, then ā ≡_β b̄ in the components, at the same level β.

The owner row is kept throughout the induction because it is what forces responses into the correct fiber: a move by a point of the fiber (r, τ) is answered, by the lab τ and own atoms against the retained row, by a point of the fiber (s, τ) (a private lemma). Owner-indexed nullary atoms (lift0) read at the row supply the component nullary facts, so empty fibers are handled with no fiber point. At level zero the component atoms are exactly the assembled eq, lift, and lift0 atoms on the canonical points (relMap_lift_pt, relMap_lift0_row).

Corollary (bfEquiv_restrict_nil): row r ≡_β row s gives C r τ ≡_β D s τ as structures (empty tuples) for every label τ.

Lifted nullary facts distinguish rows already at level zero, so the corollary is a genuine constraint on the rows, not an automatic agreement.

def FirstOrder.Language.FiberAssembly.rowPts {U R : Type u} {C : R → Label U → Type u} (r : R) (τ : Label U) {k : ℕ} (a : Fin k → C r τ) : Fin (k + 1) → Carrier R C

The assembled tuple of a row followed by points of one of its fibers.

Equations

• FirstOrder.Language.FiberAssembly.rowPts r τ a = Fin.cons (FirstOrder.Language.FiberAssembly.Carrier.row r) fun (j : Fin k) => FirstOrder.Language.FiberAssembly.Carrier.pt r τ (a j)

@[simp]

theorem FirstOrder.Language.FiberAssembly.rowPts_zero {U R : Type u} {C : R → Label U → Type u} (r : R) (τ : Label U) {k : ℕ} (a : Fin k → C r τ) : rowPts r τ a 0 = Carrier.row r

@[simp]

theorem FirstOrder.Language.FiberAssembly.rowPts_succ {U R : Type u} {C : R → Label U → Type u} (r : R) (τ : Label U) {k : ℕ} (a : Fin k → C r τ) (j : Fin k) : rowPts r τ a j.succ = Carrier.pt r τ (a j)

theorem FirstOrder.Language.FiberAssembly.snoc_rowPts {U R : Type u} {C : R → Label U → Type u} (r : R) (τ : Label U) {k : ℕ} (a : Fin k → C r τ) (x : C r τ) : Fin.snoc (rowPts r τ a) (Carrier.pt r τ x) = rowPts r τ (Fin.snoc a x)

Appending a point of the fiber to the assembled tuple appends it to the component tuple.

The response to a fiber point lands in the image fiber

Level zero

theorem FirstOrder.Language.FiberAssembly.sameAtomicType_of_rowPts {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {r : R} {s : S} {τ : Label U} {k : ℕ} {a : Fin k → C r τ} {b : Fin k → D s τ} (h : SameAtomicType (rowPts r τ a) (rowPts s τ b)) : SameAtomicType a b

Assembled atomic agreement of the pointed tuples gives component atomic agreement.

The theorem

theorem FirstOrder.Language.FiberAssembly.bfEquiv_restrict_pointed {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] (β : Ordinal.{u_1}) {r : R} {s : S} (τ : Label U) {k : ℕ} {a : Fin k → C r τ} {b : Fin k → D s τ} : BFEquiv β (k + 1) (rowPts r τ a) (rowPts s τ b) → BFEquiv β k a b

Pointed back-and-forth restriction: assembled equivalence of the pointed tuples, owner rows retained, restricts to component equivalence of the points at the same level.

theorem FirstOrder.Language.FiberAssembly.bfEquiv_restrict_nil {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] (β : Ordinal.{u_1}) {r : R} {s : S} (h : BFEquiv β 1 ![Carrier.row r] ![Carrier.row s]) (τ : Label U) : BFEquiv β 0 Fin.elim0 Fin.elim0

Empty-tuple corollary: equivalent rows have equivalent fibers at every label.