The labeled-fiber language, the generic row assembly, and its prefix specialization

A row assembly glues a family of component structures into one structure: a set of rows, and for every row r and every label τ a fiber C r τ carrying a component structure. The generic assembly is parameterized by an arbitrary row type R and fiber family C : R → Label U → Type, so that different row types (finite allowed words now, infinite allowed paths later) and different fiber families can be compared by the assembly theorems. The prefix specialization instantiates it with rows the allowed words and fibers chosen by the prefix rule.

Labels and the language

Labels are all nonempty words over a linear order U, admissible or not (Label U), so the signature does not depend on any allowed-word membership. The language lang U Lc is relational, with equality and the symbols of Sym U Lc:

• row, arity 1: the element is a row.
• own, arity 2: own(x, r) says x is a fiber point whose owner row is r.
• lab τ, arity 1: the element is a fiber point with label τ.
• lift R, arity l + 1, for a component symbol R : Lc.Relations (l + 1): all arguments lie in one fiber (same owner row, same label) and R holds there of their component elements. Mixed-fiber tuples and row arguments are false.
• lift0 R τ, arity 1, for a component symbol R : Lc.Relations 0: lift0 R τ (r) says r is a row and R holds in the fiber of r at label τ. This lift is owner-indexed: the nullary fact is read at the owner, so it is visible even when that fiber has no points.

Component-language boundary. The assembly encodes the relation symbols of Lc only; component function symbols are not encoded, so two component structures with the same relational data but different function interpretations assemble identically. For that reason the restriction theorem that recovers component isomorphisms from an assembled isomorphism requires [Lc.IsRelational]; the definitions here do not, and no unused hypothesis is imposed.

The generic assembly

Carrier R C is the disjoint union of the rows and of all fiber points (Carrier.row, Carrier.pt). instStructure interprets every symbol as listed above (relMap), with one interpretation equation per symbol.

The prefix specialization

• A row is an allowed word: a nondecreasing list p over U with p[i] ∈ A i for the allowed sets A : ℕ → Set U (IsAllowed, Row A); the empty word is a row.
• The fiber of p at τ is the component B (last τ) if τ is a prefix of p, and the default component B_* otherwise (compIndex, Comp, prefixFiber). compIndex is computable, so on concrete inputs the fiber type reduces definitionally; this is a convenience for regressions and claims nothing about an effective presentation of the whole assembly.
• PrefixCarrier B_* B A := Carrier (Row A) (prefixFiber B_* B A).

The construction uses allowed-word membership, order comparisons, prefixes, and the component family. No well-founded initial segment W appears anywhere. The input order on rows and its successor relation are not symbols of lang.

The symbol set is countable when U and the component symbols are (instCountableSigmaSym).

Labels

def FirstOrder.Language.FiberAssembly.Label (U : Type u) : Type u

The labels: nonempty words over U, admissible or not.

Equations

• FirstOrder.Language.FiberAssembly.Label U = { τ : List U // τ ≠ [] }

def FirstOrder.Language.FiberAssembly.Label.last {U : Type u} (τ : Label U) : U

The last letter of a label.

Equations

• τ.last = (↑τ).getLast ⋯

The language

inductive FirstOrder.Language.FiberAssembly.Sym (U : Type u) (Lc : Language) : ℕ → Type (max u w)

The relation symbols of the assembled language.

• row {U : Type u} {Lc : Language} : Sym U Lc 1
• own {U : Type u} {Lc : Language} : Sym U Lc 2
• lab {U : Type u} {Lc : Language} (τ : Label U) : Sym U Lc 1
• lift {U : Type u} {Lc : Language} {l : ℕ} (R : Lc.Relations (l + 1)) : Sym U Lc (l + 1)
• lift0 {U : Type u} {Lc : Language} (R : Lc.Relations 0) (τ : Label U) : Sym U Lc 1

def FirstOrder.Language.FiberAssembly.lang (U : Type u) (Lc : Language) : Language

The assembled language: relational, with the symbols of Sym.

Equations

• FirstOrder.Language.FiberAssembly.lang U Lc = { Functions := fun (x : ℕ) => PEmpty.{?u.3 + 1}, Relations := FirstOrder.Language.FiberAssembly.Sym U Lc }

instance FirstOrder.Language.FiberAssembly.instIsRelationalLang (U : Type u) (Lc : Language) : (lang U Lc).IsRelational

The generic assembly

inductive FirstOrder.Language.FiberAssembly.Carrier {U : Type u} (R : Type u) (C : R → Label U → Type u) : Type u

The assembled carrier over a row type R and a fiber family C: rows, and the points of every fiber.

• row {U R : Type u} {C : R → Label U → Type u} (r : R) : Carrier R C
• pt {U R : Type u} {C : R → Label U → Type u} (r : R) (τ : Label U) (x : C r τ) : Carrier R C

def FirstOrder.Language.FiberAssembly.relMap {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] {n : ℕ} : Sym U Lc n → (Fin n → Carrier R C) → Prop

Interpretation of each symbol, by cases on the symbol.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.FiberAssembly.relMap FirstOrder.Language.FiberAssembly.Sym.row v = ∃ (r : R), v 0 = FirstOrder.Language.FiberAssembly.Carrier.row r
• FirstOrder.Language.FiberAssembly.relMap (FirstOrder.Language.FiberAssembly.Sym.lab τ) v = ∃ (r : R) (x : C r τ), v 0 = FirstOrder.Language.FiberAssembly.Carrier.pt r τ x

@[instance_reducible]

instance FirstOrder.Language.FiberAssembly.instStructure {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] : (lang U Lc).Structure (Carrier R C)

The assembled structure.

Equations

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

Interpretation equations, one per symbol

theorem FirstOrder.Language.FiberAssembly.relMap_row {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (v : Fin 1 → Carrier R C) : Structure.RelMap Sym.row v ↔ ∃ (r : R), v 0 = Carrier.row r

theorem FirstOrder.Language.FiberAssembly.relMap_own {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (v : Fin 2 → Carrier R C) : Structure.RelMap Sym.own v ↔ ∃ (r : R) (τ : Label U) (x : C r τ), v 0 = Carrier.pt r τ x ∧ v 1 = Carrier.row r

theorem FirstOrder.Language.FiberAssembly.relMap_lab {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (τ : Label U) (v : Fin 1 → Carrier R C) : Structure.RelMap (Sym.lab τ) v ↔ ∃ (r : R) (x : C r τ), v 0 = Carrier.pt r τ x

theorem FirstOrder.Language.FiberAssembly.relMap_lift {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] {l : ℕ} (S : Lc.Relations (l + 1)) (v : Fin (l + 1) → Carrier R C) : Structure.RelMap (Sym.lift S) v ↔ ∃ (r : R) (τ : Label U) (y : Fin (l + 1) → C r τ), (∀ (i : Fin (l + 1)), v i = Carrier.pt r τ (y i)) ∧ Structure.RelMap S y

theorem FirstOrder.Language.FiberAssembly.relMap_lift0 {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (S : Lc.Relations 0) (τ : Label U) (v : Fin 1 → Carrier R C) : Structure.RelMap (Sym.lift0 S τ) v ↔ ∃ (r : R), v 0 = Carrier.row r ∧ Structure.RelMap S Fin.elim0

theorem FirstOrder.Language.FiberAssembly.not_relMap_lift_of_row {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] {l : ℕ} (S : Lc.Relations (l + 1)) (v : Fin (l + 1) → Carrier R C) (i : Fin (l + 1)) (r : R) (hv : v i = Carrier.row r) : ¬Structure.RelMap (Sym.lift S) v

Lifted relations never hold of a row argument.

theorem FirstOrder.Language.FiberAssembly.relMap_lift_same_fiber {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] {l : ℕ} (S : Lc.Relations (l + 1)) (v : Fin (l + 1) → Carrier R C) (h : Structure.RelMap (Sym.lift S) v) (i j : Fin (l + 1)) : ∃ (r : R) (τ : Label U) (x : C r τ) (y : C r τ), v i = Carrier.pt r τ x ∧ v j = Carrier.pt r τ y

Mixed-fiber tuples are false: a lifted relation holds only of arguments from one fiber, the same owner row and the same label.

theorem FirstOrder.Language.FiberAssembly.relMap_lift0_row {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (S : Lc.Relations 0) (τ : Label U) (r : R) : (Structure.RelMap (Sym.lift0 S τ) fun (x : Fin 1) => Carrier.row r) ↔ Structure.RelMap S Fin.elim0

The lift of a nullary symbol is read at the owner row; it does not require the fiber to have any point.

The prefix specialization

def FirstOrder.Language.FiberAssembly.IsAllowed {U : Type u} [LinearOrder U] (A : ℕ → Set U) (p : List U) : Prop

An allowed word: nondecreasing, with the i-th letter in A i.

Equations

• FirstOrder.Language.FiberAssembly.IsAllowed A p = (List.Pairwise (fun (x1 x2 : U) => x1 ≤ x2) p ∧ ∀ (i : ℕ) (h : i < p.length), p[i] ∈ A i)

theorem FirstOrder.Language.FiberAssembly.isAllowed_nil {U : Type u} [LinearOrder U] (A : ℕ → Set U) : IsAllowed A []

def FirstOrder.Language.FiberAssembly.Row {U : Type u} [LinearOrder U] (A : ℕ → Set U) : Type u

The rows of the prefix specialization: allowed words, the empty word included.

Equations

• FirstOrder.Language.FiberAssembly.Row A = { p : List U // FirstOrder.Language.FiberAssembly.IsAllowed A p }

def FirstOrder.Language.FiberAssembly.compIndex {U : Type u} [DecidableEq U] (p : List U) (τ : Label U) : Option U

Which component sits at (p, τ): some (last τ) if τ is a prefix of p, else none (the default component). Computable, so it reduces on concrete inputs.

Equations

• FirstOrder.Language.FiberAssembly.compIndex p τ = if ↑τ <+: p then some τ.last else none

theorem FirstOrder.Language.FiberAssembly.compIndex_of_prefix {U : Type u} [DecidableEq U] {p : List U} {τ : Label U} (h : ↑τ <+: p) : compIndex p τ = some τ.last

theorem FirstOrder.Language.FiberAssembly.compIndex_of_not_prefix {U : Type u} [DecidableEq U] {p : List U} {τ : Label U} (h : ¬↑τ <+: p) : compIndex p τ = none

def FirstOrder.Language.FiberAssembly.Comp {U : Type u} (Bstar : Type u) (B : U → Type u) : Option U → Type u

The component at an index: B_* at none, B u at some u.

Equations

• FirstOrder.Language.FiberAssembly.Comp Bstar B none = Bstar
• FirstOrder.Language.FiberAssembly.Comp Bstar B (some u) = B u

@[instance_reducible]

instance FirstOrder.Language.FiberAssembly.instCompStructure {U : Type u} (Lc : Language) (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (o : Option U) : Lc.Structure (Comp Bstar B o)

Equations

• FirstOrder.Language.FiberAssembly.instCompStructure Lc Bstar B none = FirstOrder.Language.FiberAssembly.instCompStructure._aux_1 Lc Bstar B
• FirstOrder.Language.FiberAssembly.instCompStructure Lc Bstar B (some u) = FirstOrder.Language.FiberAssembly.instCompStructure._aux_3 Lc Bstar B u

def FirstOrder.Language.FiberAssembly.prefixFiber {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) : Row A → Label U → Type u

The prefix fiber family: the component of last τ when τ is a prefix of the row, the default component otherwise.

Equations

• FirstOrder.Language.FiberAssembly.prefixFiber Bstar B A p τ = FirstOrder.Language.FiberAssembly.Comp Bstar B (FirstOrder.Language.FiberAssembly.compIndex (↑p) τ)

@[instance_reducible]

instance FirstOrder.Language.FiberAssembly.instPrefixFiberStructure {U : Type u} [LinearOrder U] (Lc : Language) (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (p : Row A) (τ : Label U) : Lc.Structure (prefixFiber Bstar B A p τ)

Equations

• FirstOrder.Language.FiberAssembly.instPrefixFiberStructure Lc Bstar B A p τ = FirstOrder.Language.FiberAssembly.instCompStructure Lc Bstar B (FirstOrder.Language.FiberAssembly.compIndex (↑p) τ)

@[reducible, inline]

abbrev FirstOrder.Language.FiberAssembly.PrefixCarrier {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) : Type u

The carrier of the prefix specialization.

Equations

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

Countability of the carrier

instance FirstOrder.Language.FiberAssembly.instCountableCarrier {U : Type u} (R : Type u) (C : R → Label U → Type u) [Countable R] [Countable U] [∀ (r : R) (τ : Label U), Countable (C r τ)] : Countable (Carrier R C)

The assembled carrier is countable when the rows, the labels, and every fiber are.

instance FirstOrder.Language.FiberAssembly.instCountableRow {U : Type u} [LinearOrder U] [Countable U] (A : ℕ → Set U) : Countable (Row A)

The rows of the prefix specialization are countable when U is.

instance FirstOrder.Language.FiberAssembly.instCountableComp {U : Type u} (Bstar : Type u) (B : U → Type u) [Countable Bstar] [∀ (u : U), Countable (B u)] (o : Option U) : Countable (Comp Bstar B o)

Components are countable when the default and every B u are.

instance FirstOrder.Language.FiberAssembly.instCountablePrefixFiber {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) [Countable Bstar] [∀ (u : U), Countable (B u)] (p : Row A) (τ : Label U) : Countable (prefixFiber Bstar B A p τ)

Countability of the symbols

instance FirstOrder.Language.FiberAssembly.instCountableSigmaSym (U : Type u) (Lc : Language) [Countable U] [Countable ((n : ℕ) × Lc.Relations n)] : Countable ((n : ℕ) × Sym U Lc n)

Symbols are countable when U and the component symbols are.