Extending a finite matching to a profile-preserving row permutation

The generic lemma exists_equiv_of_matching (a finite compatible matching respecting an equivalence relation extends to a permutation respecting it and fixing everything outside the sources and targets) lives in Scott/FiniteMatching.lean; it has no fiber content.

Specialization (exists_profilePerm): SameProfile r s (isomorphic fibers at every label) is an equivalence relation on rows, so a finite compatible matching of rows with the same profiles extends to a profile-preserving permutation of all rows. Nothing here uses countability, relationality, or any structure hypothesis.

Specialization to rows with the same profile

def FirstOrder.Language.FiberAssembly.SameProfile {U : Type u} [LinearOrder U] (Lc : Language) (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (A : ℕ → Set U) (r s : Row A) : Prop

Two rows have the same profile when their fibers are isomorphic at every label.

Equations

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

theorem FirstOrder.Language.FiberAssembly.sameProfile_equivalence {U : Type u} [LinearOrder U] {Lc : Language} {Bstar : Type u} {B : U → Type u} [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] {A : ℕ → Set U} : Equivalence (SameProfile Lc Bstar B A)

theorem FirstOrder.Language.FiberAssembly.exists_profilePerm {U : Type u} [LinearOrder U] {Lc : Language} {Bstar : Type u} {B : U → Type u} [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] {A : ℕ → Set U} {m : ℕ} (r s : Fin m → Row A) (hcomp : ∀ (j j' : Fin m), r j = r j' ↔ s j = s j') (hp : ∀ (j : Fin m), SameProfile Lc Bstar B A (r j) (s j)) : ∃ (e : Row A ≃ Row A), (∀ (j : Fin m), e (r j) = s j) ∧ (∀ (t : Row A), SameProfile Lc Bstar B A t (e t)) ∧ ∀ (t : Row A), (∀ (j : Fin m), t ≠ r j ∧ t ≠ s j) → e t = t

Profile-preserving row permutation. A finite compatible matching of rows with the same profiles extends to a permutation of all rows preserving profiles and fixing every row outside the sources and targets.