Companion carriers: allowed paths, prefixes, and the path row

The companion of the prefix specialization along an infinite allowed path π is the generic carrier over the rows Row A ⊕ Unit: the finite allowed rows keep their fibers, and the extra row ρ_π follows the same prefix rule along π (pathFiber, CompanionCarrier).

• IsAllowedPath A π: π is nondecreasing with π n ∈ A n. Allowedness is a hypothesis where a prefix must be a row; the constructor does not bake in approximation or non-defaultness of the components along the path.
• pathPrefix π k: the prefix [π 0, …, π (k - 1)]; prefixRow hπ k is it as an allowed row. Prefixes of different lengths are distinct.
• IsPathPrefix π τ: a label lies on the path; pathIndex π τ is some (last τ) then and none otherwise.
• Fiber-index equations: compIndex (pathPrefix π k) τ = pathIndex π τ for labels of length ≤ k and = none for longer labels (compIndex_pathPrefix_of_le, compIndex_pathPrefix_of_lt); consecutive prefixes differ only at the single label prefixLabel π k (compIndex_pathPrefix_succ_of_ne, with the length-based case split as compIndex_pathPrefix_succ_of_length_ne), where the longer prefix gives some (π k) and the shorter gives none. Hence ρ_π and π|ₖ have equal fibers at every label of length ≤ k (pathFiber_inl_prefixRow_of_le).
• Countability of the companion carrier from countable letters, default, and components.

Nothing about equivalence, isomorphism, or ranks is proved here.

Prefixes of a path (no order structure needed)

def FirstOrder.Language.FiberAssembly.pathPrefix {U : Type u} (π : ℕ → U) (k : ℕ) : List U

The prefix [π 0, …, π (k - 1)] of a path.

Equations

• FirstOrder.Language.FiberAssembly.pathPrefix π k = List.ofFn fun (i : Fin k) => π ↑i

@[simp]

theorem FirstOrder.Language.FiberAssembly.pathPrefix_length {U : Type u} (π : ℕ → U) (k : ℕ) : (pathPrefix π k).length = k

@[simp]

theorem FirstOrder.Language.FiberAssembly.pathPrefix_zero {U : Type u} (π : ℕ → U) : pathPrefix π 0 = []

theorem FirstOrder.Language.FiberAssembly.pathPrefix_succ {U : Type u} (π : ℕ → U) (k : ℕ) : pathPrefix π (k + 1) = pathPrefix π k ++ [π k]

@[simp]

theorem FirstOrder.Language.FiberAssembly.pathPrefix_getElem {U : Type u} (π : ℕ → U) (k i : ℕ) (h : i < (pathPrefix π k).length) : (pathPrefix π k)[i] = π i

theorem FirstOrder.Language.FiberAssembly.pathPrefix_ne_nil {U : Type u} (π : ℕ → U) (k : ℕ) : pathPrefix π (k + 1) ≠ []

theorem FirstOrder.Language.FiberAssembly.pathPrefix_prefix {U : Type u} (π : ℕ → U) {j k : ℕ} (h : j ≤ k) : pathPrefix π j <+: pathPrefix π k

A shorter prefix is a prefix of a longer one.

theorem FirstOrder.Language.FiberAssembly.eq_pathPrefix_of_prefix {U : Type u} (π : ℕ → U) {l : List U} {k : ℕ} (h : l <+: pathPrefix π k) : l = pathPrefix π l.length

A list that is a prefix of pathPrefix π k is the prefix of its own length.

Labels on the path

def FirstOrder.Language.FiberAssembly.IsPathPrefix {U : Type u} (π : ℕ → U) (τ : Label U) : Prop

A label lies on the path: it is the path prefix of its own length.

Equations

• FirstOrder.Language.FiberAssembly.IsPathPrefix π τ = (↑τ = FirstOrder.Language.FiberAssembly.pathPrefix π (↑τ).length)

@[instance_reducible]

instance FirstOrder.Language.FiberAssembly.instDecidableIsPathPrefixOfDecidableEq {U : Type u} [DecidableEq U] (π : ℕ → U) (τ : Label U) : Decidable (IsPathPrefix π τ)

Equations

• FirstOrder.Language.FiberAssembly.instDecidableIsPathPrefixOfDecidableEq π τ = FirstOrder.Language.FiberAssembly.instDecidableIsPathPrefixOfDecidableEq._aux_1 π τ

theorem FirstOrder.Language.FiberAssembly.isPathPrefix_iff_prefix {U : Type u} {π : ℕ → U} {τ : Label U} {k : ℕ} (h : (↑τ).length ≤ k) : IsPathPrefix π τ ↔ ↑τ <+: pathPrefix π k

For labels no longer than k, lying on the path is being a prefix of π|ₖ.

theorem FirstOrder.Language.FiberAssembly.not_prefix_pathPrefix_of_lt {U : Type u} {π : ℕ → U} {τ : Label U} {k : ℕ} (h : k < (↑τ).length) : ¬↑τ <+: pathPrefix π k

A label longer than k is not a prefix of π|ₖ.

def FirstOrder.Language.FiberAssembly.prefixLabel {U : Type u} (π : ℕ → U) (k : ℕ) : Label U

The prefix of length k + 1, as a label.

Equations

• FirstOrder.Language.FiberAssembly.prefixLabel π k = ⟨FirstOrder.Language.FiberAssembly.pathPrefix π (k + 1), ⋯⟩

@[simp]

theorem FirstOrder.Language.FiberAssembly.prefixLabel_val {U : Type u} (π : ℕ → U) (k : ℕ) : ↑(prefixLabel π k) = pathPrefix π (k + 1)

theorem FirstOrder.Language.FiberAssembly.prefixLabel_last {U : Type u} (π : ℕ → U) (k : ℕ) : (prefixLabel π k).last = π k

theorem FirstOrder.Language.FiberAssembly.isPathPrefix_prefixLabel {U : Type u} (π : ℕ → U) (k : ℕ) : IsPathPrefix π (prefixLabel π k)

theorem FirstOrder.Language.FiberAssembly.not_isPathPrefix_prefixLabel_of_ne {U : Type u} {π σ : ℕ → U} {k₀ k : ℕ} (h : π k₀ ≠ σ k₀) (hk : k₀ ≤ k) : ¬IsPathPrefix σ (prefixLabel π k)

A prefix label of π is not on σ when the two paths differ at an earlier position.

def FirstOrder.Language.FiberAssembly.pathIndex {U : Type u} [DecidableEq U] (π : ℕ → U) (τ : Label U) : Option U

The component index along the path: some (last τ) on the path, none off it.

Equations

• FirstOrder.Language.FiberAssembly.pathIndex π τ = if FirstOrder.Language.FiberAssembly.IsPathPrefix π τ then some τ.last else none

theorem FirstOrder.Language.FiberAssembly.pathIndex_of_isPathPrefix {U : Type u} [DecidableEq U] {π : ℕ → U} {τ : Label U} (h : IsPathPrefix π τ) : pathIndex π τ = some τ.last

theorem FirstOrder.Language.FiberAssembly.pathIndex_of_not_isPathPrefix {U : Type u} [DecidableEq U] {π : ℕ → U} {τ : Label U} (h : ¬IsPathPrefix π τ) : pathIndex π τ = none

theorem FirstOrder.Language.FiberAssembly.pathIndex_prefixLabel {U : Type u} [DecidableEq U] (π : ℕ → U) (k : ℕ) : pathIndex π (prefixLabel π k) = some (π k)

Fiber-index equations

theorem FirstOrder.Language.FiberAssembly.compIndex_pathPrefix_of_le {U : Type u} [DecidableEq U] {π : ℕ → U} {τ : Label U} {k : ℕ} (h : (↑τ).length ≤ k) : compIndex (pathPrefix π k) τ = pathIndex π τ

Short labels: the prefix row π|ₖ indexes a label of length ≤ k exactly as the path does.

theorem FirstOrder.Language.FiberAssembly.compIndex_pathPrefix_of_lt {U : Type u} [DecidableEq U] {π : ℕ → U} {τ : Label U} {k : ℕ} (h : k < (↑τ).length) : compIndex (pathPrefix π k) τ = none

Long labels: the prefix row π|ₖ gives the default at every label longer than k.

theorem FirstOrder.Language.FiberAssembly.compIndex_pathPrefix_succ_of_length_ne {U : Type u} [DecidableEq U] {π : ℕ → U} {τ : Label U} {k : ℕ} (h : (↑τ).length ≠ k + 1) : compIndex (pathPrefix π (k + 1)) τ = compIndex (pathPrefix π k) τ

Consecutive prefixes agree at every label whose length is not k + 1 (a corollary of compIndex_pathPrefix_succ_of_ne, kept for the length-based case split).

theorem FirstOrder.Language.FiberAssembly.compIndex_pathPrefix_succ_of_ne {U : Type u} [DecidableEq U] {π : ℕ → U} {τ : Label U} {k : ℕ} (h : τ ≠ prefixLabel π k) : compIndex (pathPrefix π (k + 1)) τ = compIndex (pathPrefix π k) τ

Consecutive prefixes differ only at the single label prefixLabel π k: at every other label, including off-path labels of length k + 1, they agree.

theorem FirstOrder.Language.FiberAssembly.compIndex_pathPrefix_succ_prefixLabel {U : Type u} [DecidableEq U] (π : ℕ → U) (k : ℕ) : compIndex (pathPrefix π (k + 1)) (prefixLabel π k) = some (π k)

At the label of length k + 1 on the path, the longer prefix gives some (π k).

theorem FirstOrder.Language.FiberAssembly.compIndex_pathPrefix_prefixLabel {U : Type u} [DecidableEq U] (π : ℕ → U) (k : ℕ) : compIndex (pathPrefix π k) (prefixLabel π k) = none

At the label of length k + 1 on the path, the shorter prefix gives the default.

Allowed paths and prefix rows

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

An allowed path: nondecreasing, with the n-th letter allowed at position n.

Equations

• FirstOrder.Language.FiberAssembly.IsAllowedPath A π = (Monotone π ∧ ∀ (n : ℕ), π n ∈ A n)

theorem FirstOrder.Language.FiberAssembly.isAllowed_pathPrefix {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (k : ℕ) : IsAllowed A (pathPrefix π k)

Prefixes of an allowed path are allowed rows.

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

The prefix of length k as an allowed row.

Equations

• FirstOrder.Language.FiberAssembly.prefixRow hπ k = ⟨FirstOrder.Language.FiberAssembly.pathPrefix π k, ⋯⟩

@[simp]

theorem FirstOrder.Language.FiberAssembly.prefixRow_val {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (k : ℕ) : ↑(prefixRow hπ k) = pathPrefix π k

theorem FirstOrder.Language.FiberAssembly.prefixRow_injective {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) : Function.Injective (prefixRow hπ)

Prefixes of different lengths are different rows.

The companion carrier

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

The fibers of the companion: finite rows as in the base, the path row by the prefix rule along π.

Equations

• FirstOrder.Language.FiberAssembly.pathFiber Bstar B A π (Sum.inl r) x✝ = FirstOrder.Language.FiberAssembly.prefixFiber Bstar B A r x✝
• FirstOrder.Language.FiberAssembly.pathFiber Bstar B A π (Sum.inr val) x✝ = FirstOrder.Language.FiberAssembly.Comp Bstar B (FirstOrder.Language.FiberAssembly.pathIndex π x✝)

@[simp]

theorem FirstOrder.Language.FiberAssembly.pathFiber_inl {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) (π : ℕ → U) (r : Row A) (τ : Label U) : pathFiber Bstar B A π (Sum.inl r) τ = prefixFiber Bstar B A r τ

@[simp]

theorem FirstOrder.Language.FiberAssembly.pathFiber_inr {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) (π : ℕ → U) (τ : Label U) : pathFiber Bstar B A π (Sum.inr ()) τ = Comp Bstar B (pathIndex π τ)

@[instance_reducible]

instance FirstOrder.Language.FiberAssembly.instPathFiberStructure {U : Type u} [LinearOrder U] {Lc : Language} (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) (π : ℕ → U) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (r : Row A ⊕ Unit) (τ : Label U) : Lc.Structure (pathFiber Bstar B A π r τ)

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.FiberAssembly.instPathFiberStructure Bstar B A π (Sum.inl r) x✝ = FirstOrder.Language.FiberAssembly.instPrefixFiberStructure Lc Bstar B A r x✝

@[reducible, inline]

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

The companion carrier along π.

Equations

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

theorem FirstOrder.Language.FiberAssembly.pathFiber_inl_prefixRow_of_le {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) (π : ℕ → U) {hπ : IsAllowedPath A π} {k : ℕ} {τ : Label U} (h : (↑τ).length ≤ k) : pathFiber Bstar B A π (Sum.inl (prefixRow hπ k)) τ = pathFiber Bstar B A π (Sum.inr ()) τ

The path row and a prefix row π|ₖ have the same fiber at every label of length ≤ k.

instance FirstOrder.Language.FiberAssembly.instCountableCompanion {U : Type u} [LinearOrder U] (Bstar : Type u) (B : U → Type u) (A : ℕ → Set U) (π : ℕ → U) [Countable U] [Countable Bstar] [∀ (u : U), Countable (B u)] : Countable (CompanionCarrier Bstar B A π)

The companion carrier is countable when the letters, the default, and the components are.