Isomorphism assembly and restriction for row assemblies

Over arbitrary row types and fiber families. Throughout, R, S are row types, C : R → Label U → Type, D : S → Label U → Type are fiber families with Lc-structures on every fiber, and the assembled structures are Carrier R C, Carrier S D (ModelTheory/FiberAssembly.lean).

1. Exact interpretation on canonical fiber points (relMap_lift_pt, relMap_own_pt, relMap_lab_pt, relMap_lift0_row): the lifted symbols evaluated on points of one fiber are exactly the component relations there. Uses only injectivity of the constructors.
2. Assembly (assemble): a bijection of rows e : R ≃ S together with component isomorphisms f r τ : C r τ ≃[Lc] D (e r) τ for every row and label induces an isomorphism Carrier R C ≃[lang U Lc] Carrier S D, sending row r ↦ row (e r) and pt r τ x ↦ pt (e r) τ (f r τ x). No relationality of Lc, no inhabited fibers, and no order-preservation of e are assumed: the supplied component isomorphisms carry the component nullary facts through map_rel at arity 0.
3. Restriction: an arbitrary assembled isomorphism g sends rows to rows (restrictRows g : R ≃ S) and the fiber (r, τ) onto the fiber (restrictRows g r, τ); nullary facts restrict with no fiber point required (restrict_lift0). Neither of these needs relationality. The restriction restrictFiber g r τ : C r τ ≃[Lc] D (restrictRows g r) τ to a component isomorphism requires [Lc.IsRelational], because the assembly encodes only relation symbols; it too needs no fiber point.
4. Compatibility equations: assemble_row, assemble_pt (definitional), restrictRows_apply, restrictFiber_apply, restrictRows_assemble, and restrictFiber_assemble_pt: restricting the assembled isomorphism returns the supplied component isomorphism, as an equality of the images in the carrier.

Full-profile bounds, companions, and effective presentations are outside this module.

Constructor injectivity, packaged

theorem FirstOrder.Language.FiberAssembly.Carrier.pt_inj {U R : Type u} {C : R → Label U → Type u} {r r' : R} {τ τ' : Label U} {x : C r τ} {x' : C r' τ'} (h : pt r τ x = pt r' τ' x') : r = r' ∧ τ = τ' ∧ x ≍ x'

theorem FirstOrder.Language.FiberAssembly.Carrier.pt_inj_same {U R : Type u} {C : R → Label U → Type u} {r : R} {τ : Label U} {x x' : C r τ} (h : pt r τ x = pt r τ x') : x = x'

Exact interpretation on canonical fiber points

theorem FirstOrder.Language.FiberAssembly.relMap_lift_pt {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)) (r : R) (τ : Label U) (y : Fin (l + 1) → C r τ) : (Structure.RelMap (Sym.lift S) fun (i : Fin (l + 1)) => Carrier.pt r τ (y i)) ↔ Structure.RelMap S y

A lifted relation on points of one fiber is the component relation there.

theorem FirstOrder.Language.FiberAssembly.relMap_own_pt {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (r r' : R) (τ : Label U) (x : C r τ) : Structure.RelMap Sym.own ![Carrier.pt r τ x, Carrier.row r'] ↔ r' = r

own on a fiber point and a row: the row is the owner.

theorem FirstOrder.Language.FiberAssembly.relMap_lab_pt {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (τ' : Label U) (r : R) (τ : Label U) (x : C r τ) : Structure.RelMap (Sym.lab τ') ![Carrier.pt r τ x] ↔ τ' = τ

lab τ' on a fiber point with label τ: the labels agree.

theorem FirstOrder.Language.FiberAssembly.relMap_row_row {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (r : R) : Structure.RelMap Sym.row ![Carrier.row r]

row holds of every row and of no fiber point.

theorem FirstOrder.Language.FiberAssembly.not_relMap_row_pt {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] (r : R) (τ : Label U) (x : C r τ) : ¬Structure.RelMap Sym.row ![Carrier.pt r τ x]

Assembly

noncomputable def FirstOrder.Language.FiberAssembly.assemble {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 τ)] (e : R ≃ S) (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (D (e r) τ)) : (lang U Lc).Equiv (Carrier R C) (Carrier S D)

Assembly of an isomorphism from a row bijection and component isomorphisms. No relationality, no inhabited fibers, no order-preservation.

Equations

• FirstOrder.Language.FiberAssembly.assemble e f = { toEquiv := Equiv.ofBijective (FirstOrder.Language.FiberAssembly.assembleFun✝ e f) ⋯, map_fun' := ⋯, map_rel' := ⋯ }

@[simp]

theorem FirstOrder.Language.FiberAssembly.assemble_row {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 τ)] (e : R ≃ S) (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (D (e r) τ)) (r : R) : (assemble e f) (Carrier.row r) = Carrier.row (e r)

@[simp]

theorem FirstOrder.Language.FiberAssembly.assemble_pt {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 τ)] (e : R ≃ S) (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (D (e r) τ)) (r : R) (τ : Label U) (x : C r τ) : (assemble e f) (Carrier.pt r τ x) = Carrier.pt (e r) τ ((f r τ) x)

Restriction

noncomputable def FirstOrder.Language.FiberAssembly.restrictRows {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 τ)] (g : (lang U Lc).Equiv (Carrier R C) (Carrier S D)) : R ≃ S

Restriction to rows: the row bijection of an assembled isomorphism.

Equations

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

@[simp]

theorem FirstOrder.Language.FiberAssembly.restrictRows_apply {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 τ)] (g : (lang U Lc).Equiv (Carrier R C) (Carrier S D)) (r : R) : g (Carrier.row r) = Carrier.row ((restrictRows g) r)

noncomputable def FirstOrder.Language.FiberAssembly.restrictFiber {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 τ)] [Lc.IsRelational] (g : (lang U Lc).Equiv (Carrier R C) (Carrier S D)) (r : R) (τ : Label U) : Lc.Equiv (C r τ) (D ((restrictRows g) r) τ)

Restriction to a labeled fiber: the component isomorphism induced by an assembled isomorphism. This is the one construction needing [Lc.IsRelational], because the assembly encodes only relation symbols; no fiber point is required.

Equations

• FirstOrder.Language.FiberAssembly.restrictFiber g r τ = { toEquiv := Equiv.ofBijective (FirstOrder.Language.FiberAssembly.fiberMap✝ g r τ) ⋯, map_fun' := ⋯, map_rel' := ⋯ }

@[simp]

theorem FirstOrder.Language.FiberAssembly.restrictFiber_apply {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 τ)] [Lc.IsRelational] (g : (lang U Lc).Equiv (Carrier R C) (Carrier S D)) (r : R) (τ : Label U) (x : C r τ) : g (Carrier.pt r τ x) = Carrier.pt ((restrictRows g) r) τ ((restrictFiber g r τ) x)

theorem FirstOrder.Language.FiberAssembly.restrict_lift0 {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 τ)] (g : (lang U Lc).Equiv (Carrier R C) (Carrier S D)) (r : R) (τ : Label U) (Sy : Lc.Relations 0) : Structure.RelMap Sy Fin.elim0 ↔ Structure.RelMap Sy Fin.elim0

Nullary facts restrict along an assembled isomorphism, with no fiber point required.

Compatibility of restriction with assembly

theorem FirstOrder.Language.FiberAssembly.restrictRows_assemble {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 τ)] (e : R ≃ S) (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (D (e r) τ)) : restrictRows (assemble e f) = e

theorem FirstOrder.Language.FiberAssembly.restrictFiber_assemble_pt {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 τ)] [Lc.IsRelational] (e : R ≃ S) (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (D (e r) τ)) (r : R) (τ : Label U) (x : C r τ) : Carrier.pt ((restrictRows (assemble e f)) r) τ ((restrictFiber (assemble e f) r τ) x) = Carrier.pt (e r) τ ((f r τ) x)

Restricting the assembled isomorphism returns the supplied component isomorphism: the two images of a fiber point in the carrier are equal.