Strictly local and locally testable sets of structures

Among the members of a family of relational structures, a set is strictly k-local when a set of permitted k-factors cuts it out, and locally k-testable when membership depends only on the set of k-factors. Over words ordered by successor these are the strictly local and the locally testable stringsets, and over words ordered by precedence the strictly piecewise and the piecewise testable ones.

Main definitions

• FirstOrder.Language.IsStrictlyLocal, FirstOrder.Language.IsLocallyTestable: the strictly local and the locally testable sets of members of a family of structures.

Main statements

• FirstOrder.Language.isStrictlyLocal_iff: a set is strictly local exactly when it contains every member whose factors all occur in its members.
• FirstOrder.Language.IsStrictlyLocal.mem_of_factors_subset_union: strictly local sets are closed under any operation that adds no factor.

References

• [RL19]

def FirstOrder.Language.IsStrictlyLocal (L : Language) {ι : Type x} (M : ι → Type w) [(i : ι) → L.Structure (M i)] (k : ℕ) (S : Set ι) : Prop

A set of members of a family of structures is strictly k-local when it consists of the members all of whose k-factors a fixed set of factors permits.

Equations

• L.IsStrictlyLocal M k S = ∃ (G : Set (L.Factor k)), S = {i : ι | L.factors k (M i) ⊆ G}

def FirstOrder.Language.IsLocallyTestable (L : Language) {ι : Type x} (M : ι → Type w) [(i : ι) → L.Structure (M i)] (k : ℕ) (S : Set ι) : Prop

A set of members of a family of structures is locally k-testable when membership depends only on the set of k-factors.

Equations

• L.IsLocallyTestable M k S = Function.FactorsThrough (fun (x : ι) => x ∈ S) fun (i : ι) => L.factors k (M i)

Strictly local sets

theorem FirstOrder.Language.isStrictlyLocal_iff {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S : Set ι} : L.IsStrictlyLocal M k S ↔ ∀ (i : ι), L.factors k (M i) ⊆ ⋃ j ∈ S, L.factors k (M j) → i ∈ S

A set is strictly local exactly when it contains every member whose factors all occur in its members.

theorem FirstOrder.Language.IsStrictlyLocal.mem_of_factors_subset_union {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S : Set ι} (hS : L.IsStrictlyLocal M k S) {a b c : ι} (ha : a ∈ S) (hb : b ∈ S) (h : L.factors k (M c) ⊆ L.factors k (M a) ∪ L.factors k (M b)) : c ∈ S

Strictly local sets are closed under any operation that adds no factor.

theorem FirstOrder.Language.IsStrictlyLocal.mem_of_factors_subset {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S : Set ι} (hS : L.IsStrictlyLocal M k S) {i j : ι} (hi : i ∈ S) (h : L.factors k (M j) ⊆ L.factors k (M i)) : j ∈ S

Strictly local sets are downward closed under inclusion of factor sets.

theorem FirstOrder.Language.IsStrictlyLocal.comap {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S : Set ι} {κ : Type u_1} (hS : L.IsStrictlyLocal M k S) (π : κ → ι) : L.IsStrictlyLocal (fun (j : κ) => M (π j)) k (π ⁻¹' S)

Strictly local sets pull back along any reindexing of the family.

theorem FirstOrder.Language.IsStrictlyLocal.inter {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S T : Set ι} (hS : L.IsStrictlyLocal M k S) (hT : L.IsStrictlyLocal M k T) : L.IsStrictlyLocal M k (S ∩ T)

Locally testable sets

theorem FirstOrder.Language.IsStrictlyLocal.isLocallyTestable {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S : Set ι} (hS : L.IsStrictlyLocal M k S) : L.IsLocallyTestable M k S

theorem FirstOrder.Language.IsLocallyTestable.compl {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S : Set ι} (hS : L.IsLocallyTestable M k S) : L.IsLocallyTestable M k Sᶜ

theorem FirstOrder.Language.IsLocallyTestable.inter {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S T : Set ι} (hS : L.IsLocallyTestable M k S) (hT : L.IsLocallyTestable M k T) : L.IsLocallyTestable M k (S ∩ T)

theorem FirstOrder.Language.IsLocallyTestable.union {L : Language} {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {k : ℕ} {S T : Set ι} (hS : L.IsLocallyTestable M k S) (hT : L.IsLocallyTestable M k T) : L.IsLocallyTestable M k (S ∪ T)