Fiber isomorphisms carrying a tuple

Given a row bijection e with fiber isomorphisms f₀ r τ : C r τ ≃[Lc] C (e r) τ, and tuples a, b matched along e with the owner rows present, the fiber isomorphisms are adjusted on the finitely many occupied fibers so that the assembled automorphism carries a to b.

• FiberCover a: one enumeration of all positions of a in each fiber (repeated values kept; coverage is by position). FiberCover.ofTuple constructs one from any tuple, with no countability; FiberCover.pos_iff says 0 < k r τ iff the fiber contains a coordinate, so the occupied fibers form a finite set (FiberCover.occupied_finite).
• The orbit-rank facts for empty tuples (orbitRank_elim0, orbitRank_of_length_zero) live in Scott/OrbitRank.lean; generic rank users need no fiber machinery.
• exists_fiber_isos_carrying: if a ≡_β b, and for every fiber the complete source tuple of the cover has orbit rank at most β, then there are fiber isomorphisms f with assemble e f ∘ a = b; f agrees with f₀ on unoccupied fibers.

For an occupied fiber the pointed restriction lemma gives the level-β equivalence of the source tuple with the matched target tuple (the owner row is present); the target tuple is pulled back through f₀, the orbit-rank bound with [Lc.IsRelational] and countability gives an automorphism of the source component moving the source tuple onto it, and composing with f₀ gives the adjusted isomorphism. The premise on unoccupied fibers is automatic by orbitRank_elim0, not vacuous: the hypothesis still quantifies over them.

Fiber covers

structure FirstOrder.Language.FiberAssembly.FiberCover {U R : Type u'} {C : R → Label U → Type u'} {n : ℕ} (a : Fin n → Carrier R C) : Type u'

One enumeration of all positions of a in each fiber; repeated values are kept and coverage is by position.

• k : R → Label U → ℕ

  The length of the covering enumeration (positions may be enumerated more than once).

• ι (r : R) (τ : Label U) : Fin (self.k r τ) → Fin n

  The enumeration of positions.

• inFiber (r : R) (τ : Label U) (j : Fin (self.k r τ)) : InFiber a r τ (self.ι r τ j)

  Every enumerated position lies in the fiber.

• covers (r : R) (τ : Label U) (i : Fin n) : InFiber a r τ i → ∃ (j : Fin (self.k r τ)), self.ι r τ j = i

  Every position in the fiber is enumerated.

noncomputable def FirstOrder.Language.FiberAssembly.FiberCover.ofTuple {U R : Type u'} {C : R → Label U → Type u'} {n : ℕ} (a : Fin n → Carrier R C) : FiberCover a

A cover exists for every tuple, with no countability assumption.

Equations

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

theorem FirstOrder.Language.FiberAssembly.FiberCover.pos_iff {U R : Type u'} {C : R → Label U → Type u'} {n : ℕ} {a : Fin n → Carrier R C} (cov : FiberCover a) (r : R) (τ : Label U) : 0 < cov.k r τ ↔ ∃ (i : Fin n), InFiber a r τ i

A fiber has a positive count iff it contains a coordinate of the tuple.

theorem FirstOrder.Language.FiberAssembly.FiberCover.occupied_finite {U R : Type u'} {C : R → Label U → Type u'} {n : ℕ} {a : Fin n → Carrier R C} (cov : FiberCover a) : {p : R × Label U | 0 < cov.k p.1 p.2}.Finite

The occupied fibers form a finite set.

noncomputable def FirstOrder.Language.FiberAssembly.FiberCover.srcTuple {U R : Type u'} {C : R → Label U → Type u'} {n : ℕ} {a : Fin n → Carrier R C} (cov : FiberCover a) (r : R) (τ : Label U) : Fin (cov.k r τ) → C r τ

The complete source tuple of a fiber.

Equations

• cov.srcTuple r τ j = FirstOrder.Language.FiberAssembly.elt ⋯

noncomputable def FirstOrder.Language.FiberAssembly.FiberCover.tgtTuple {U R : Type u'} {C : R → Label U → Type u'} {n : ℕ} {a : Fin n → Carrier R C} (cov : FiberCover a) {e : R ≃ R} {b : Fin n → Carrier R C} (hm : Matched e a b) (r : R) (τ : Label U) : Fin (cov.k r τ) → C (e r) τ

The matched target tuple of a fiber, at the same positions.

Equations

• cov.tgtTuple hm r τ j = hm.eltB ⋯

theorem FirstOrder.Language.FiberAssembly.matched_assemble {U : Type u'} {Lc : Language} {R : Type u'} {C : R → Label U → Type u'} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] {S : Type u'} {D : S → Label U → Type u'} [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] (e : R ≃ S) (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (D (e r) τ)) {n : ℕ} (a : Fin n → Carrier R C) : Matched e a (⇑(assemble e f) ∘ a)

A tuple is matched, along e, with its image under an assembled isomorphism.

Adjusting the fiber isomorphisms

theorem FirstOrder.Language.FiberAssembly.exists_fiber_isos_carrying {U : Type u'} {Lc : Language} {R : Type u'} {C : R → Label U → Type u'} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [Lc.IsRelational] [∀ (r : R) (τ : Label U), Countable (C r τ)] (β : Ordinal.{u'}) (e : R ≃ R) (f₀ : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (C (e r) τ)) {n : ℕ} {a b : Fin n → Carrier R C} (hm : Matched e a b) (howners : ∀ (i : Fin n) (r : R) (τ : Label U), InFiber a r τ i → ∃ (j : Fin n), a j = Carrier.row r) (hbf : BFEquiv β n a b) (cov : FiberCover a) (horb : ∀ (r : R) (τ : Label U), orbitRank (cov.srcTuple r τ) ≤ β) : ∃ (f : (r : R) → (τ : Label U) → Lc.Equiv (C r τ) (C (e r) τ)), ⇑(assemble e f) ∘ a = b ∧ ∀ (r : R) (τ : Label U), ¬0 < cov.k r τ → f r τ = f₀ r τ

Fiber isomorphisms carrying the tuple. Given fiber isomorphisms f₀ along e, tuples a ≡_β b matched along e with owner rows present, a cover of a, and for every fiber an orbit-rank bound ≤ β on the complete source tuple, there are fiber isomorphisms f with assemble e f ∘ a = b, agreeing with f₀ on unoccupied fibers.