Sortwise actions on relational structures (AHK umbrella #103, R1a)

The combinatorial layer of the generic Aldous–Hoover–Kallenberg carrier (issue #104), generalizing the finite-restriction / relabelling / padding operations of Graphon/InfiniteGraph.lean to arbitrary multi-sorted relational signatures. No topology or measure theory yet — the Boolean-product equivalence and the standard-Borel / cylinder layer are R1b; the projective extension is R2.

Everything is built from the sortwise pullback RelStructure.comap of R0:

• RelCoord.map_id / RelCoord.map_comp, RelStructure.comap_id / RelStructure.comap_comp — functoriality of the coordinate pushforward and the structure pullback;
• RelStructure.restrict — restriction to a sub-carrier along a sortwise family of embeddings; RelStructure.relabel — relabelling by a sortwise family of permutations;
• RelStructure.restrictFin n — the induced structure on the first n s vertices of each sort (the restrictFin analog); RelStructure.restrictLE — restriction between size vectors n ≤ m;
• RelStructure.pad — padding a finite structure into a larger carrier along sortwise embeddings (the padFin analog: the padded structure holds only on tuples all of whose arguments come from the sub-carrier), with RelStructure.restrict_pad (padding is a section of restriction — the restrictFin_padFin analog);
• RelStructure.restrictLE_restrictFin / RelStructure.restrictLE_restrictLE — restrictions compose (the restrictFin_comap analog).

Functoriality

@[simp]

theorem RelSignature.RelCoord.map_id {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : map (fun (x : S.Srt) => id) c = c

theorem RelSignature.RelCoord.map_comp {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {X : S.Srt → Type u_3} (f : (s : S.Srt) → V s → W s) (g : (s : S.Srt) → W s → X s) (c : S.RelCoord V) : map (fun (s : S.Srt) => g s ∘ f s) c = map g (map f c)

@[simp]

theorem RelSignature.RelStructure.comap_id {S : RelSignature} {V : S.Srt → Type u_1} (σ : S.RelStructure V) : comap (fun (x : S.Srt) => id) σ = σ

theorem RelSignature.RelStructure.comap_comp {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {X : S.Srt → Type u_3} (f : (s : S.Srt) → V s → W s) (g : (s : S.Srt) → W s → X s) (σ : S.RelStructure X) : comap (fun (s : S.Srt) => g s ∘ f s) σ = comap f (comap g σ)

Restriction and relabelling

def RelSignature.RelStructure.restrict {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) : S.RelStructure W → S.RelStructure V

Restriction to a sub-carrier along a sortwise family of embeddings.

Equations

• RelSignature.RelStructure.restrict e = RelSignature.RelStructure.comap fun (s : S.Srt) => ⇑(e s)

def RelSignature.RelStructure.relabel {S : RelSignature} {V : S.Srt → Type u_1} (σ : (s : S.Srt) → Equiv.Perm (V s)) : S.RelStructure V → S.RelStructure V

Relabelling by a sortwise family of permutations.

Equations

• RelSignature.RelStructure.relabel σ = RelSignature.RelStructure.comap fun (s : S.Srt) => ⇑(σ s)

theorem RelSignature.RelStructure.restrict_relabel {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) (ρ : (s : S.Srt) → Equiv.Perm (W s)) (X : S.RelStructure W) : restrict e (relabel ρ X) = restrict (fun (s : S.Srt) => (e s).trans (Equiv.toEmbedding (ρ s))) X

The moved-window law: restriction along e after an arbitrary relabeling is restriction along the moved window (e s).trans (ρ s).toEmbedding. Definitional. A mixed permutation does not commute with restriction to the same half — but it does move the restricted window, and this is the form the mixed-window marginal theorem consumes.

def RelSignature.RelStructure.restrictFin {S : RelSignature} (n : S.Srt → ℕ) : S.RelStructure S.Vinfinite → S.RelStructure (Vfinite n)

Finite restriction: the structure induced on the first n s vertices of each sort.

Equations

• RelSignature.RelStructure.restrictFin n = RelSignature.RelStructure.comap fun (s : S.Srt) => ⇑Fin.valEmbedding

def RelSignature.RelStructure.restrictLE {S : RelSignature} {n m : S.Srt → ℕ} (h : ∀ (s : S.Srt), n s ≤ m s) : S.RelStructure (Vfinite m) → S.RelStructure (Vfinite n)

Restriction between size vectors n ≤ m.

Equations

• RelSignature.RelStructure.restrictLE h = RelSignature.RelStructure.comap fun (s : S.Srt) => ⇑(Fin.castLEEmb ⋯)

Padding

noncomputable def RelSignature.RelStructure.pad {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) : S.RelStructure V → S.RelStructure W

Padding a finite structure into a larger carrier along a sortwise family of embeddings: the padded structure holds on a tuple exactly when every argument comes from the sub-carrier (is in the range of the embedding) and the original structure holds on the pulled-back tuple. This is the relational analog of SimpleGraph.map along an embedding (padFin).

Equations

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

@[simp]

theorem RelSignature.RelStructure.restrict_pad {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) (σ : S.RelStructure V) : restrict e (pad e σ) = σ

Restriction undoes padding (restrictFin_padFin analog): padding a structure along a sortwise embedding family and then restricting back recovers the original structure.

Restrictions compose

theorem RelSignature.RelStructure.restrictLE_restrictLE {S : RelSignature} {n m k : S.Srt → ℕ} (hnm : ∀ (s : S.Srt), n s ≤ m s) (hmk : ∀ (s : S.Srt), m s ≤ k s) (σ : S.RelStructure (Vfinite k)) : restrictLE hnm (restrictLE hmk σ) = restrictLE ⋯ σ

Restrictions between size vectors compose (the restrictFin_comap analog).

theorem RelSignature.RelStructure.restrictLE_restrictFin {S : RelSignature} {n m : S.Srt → ℕ} (h : ∀ (s : S.Srt), n s ≤ m s) (σ : S.RelStructure S.Vinfinite) : restrictLE h (restrictFin m σ) = restrictFin n σ

A finite restriction factors through any coarser one (the restrictFin_comap analog): restricting the m-restriction down to n ≤ m equals the direct n-restriction.

@[simp]

theorem RelSignature.RelStructure.restrictFin_pad {S : RelSignature} (n : S.Srt → ℕ) (σ : S.RelStructure (Vfinite n)) : restrictFin n (pad (fun (s : S.Srt) => Fin.valEmbedding) σ) = σ

Finite restriction is restrict along the value embeddings, so padding along them is a section of restrictFin.

theorem RelSignature.restrict_comp_pad {S : RelSignature} {U : S.Srt → Type u_1} {V : S.Srt → Type u_2} {W : S.Srt → Type u_3} (e : (s : S.Srt) → V s ↪ W s) (g : (s : S.Srt) → U s ↪ V s) (σ : S.RelStructure V) : RelStructure.restrict (fun (s : S.Srt) => (g s).trans (e s)) (RelStructure.pad e σ) = RelStructure.restrict g σ

Restriction of a padding along composable embeddings: padding along e then restricting along g ∘ e recovers restriction along g (generalizes restrict_pad, the case g = id).

theorem RelSignature.restrictFin_pad_diag {S : RelSignature} {n : S.Srt → ℕ} {N : ℕ} (h : ∀ (s : S.Srt), n s ≤ N) (σ : S.RelStructure (Vfinite fun (x : S.Srt) => N)) : RelStructure.restrictFin n (RelStructure.pad (fun (x : S.Srt) => Fin.valEmbedding) σ) = RelStructure.restrictLE h σ

The finite restriction of a diagonal padding is a restriction between size vectors.