Atoms over variables

An atom R(x₁, …, xₙ) applies a relation symbol to variables, and an assignment realizes a set of atoms when it makes each of them true. A set of atoms presents a structure on its variables, its canonical structure, in which a relation holds of exactly the tuples its atoms list. The assignments realizing a set of atoms in a structure are the homomorphisms out of its canonical structure, so one set of atoms entails another along a map of variables in every structure exactly when the map carries the atoms of the second into the first. This is Chandra and Merlin's theorem on the containment of conjunctive queries.

Main definitions

• FirstOrder.Language.Atom: atoms, renamed by Atom.map, permuted by Equiv.Perm, and read as atomic formulas by Atom.toFormula.
• FirstOrder.Language.Atom.realizers: the assignments realizing a set of atoms.
• FirstOrder.Language.Atom.Canonical: the structure a set of atoms presents on its variables.

Main statements

• FirstOrder.Language.Atom.Canonical.homEquiv: the homomorphisms out of the canonical structure are the realizing assignments.
• FirstOrder.Language.Atom.forall_realizers_subset_preimage_iff: entailment along a map in every structure is inclusion of the renamed atoms.

References

• [CM77]

structure FirstOrder.Language.Atom (L : Language) (α : Type w) : Type (max v w)

An atom R(x₁, …, xₙ) applies a relation symbol to variables.

• arity : ℕ
• rel : L.Relations self.arity

  The relation symbol.

• args : Fin self.arity → α

  The variables the relation symbol is applied to.

def FirstOrder.Language.Atom.map {L : Language} {α : Type w} {β : Type x} (f : α → β) (a : L.Atom α) : L.Atom β

a.map f renames the variables of a along f.

Equations

• FirstOrder.Language.Atom.map f a = { arity := a.arity, rel := a.rel, args := f ∘ a.args }

@[simp]

theorem FirstOrder.Language.Atom.map_id {L : Language} {α : Type w} (a : L.Atom α) : map id a = a

@[simp]

theorem FirstOrder.Language.Atom.map_id' {L : Language} {α : Type w} : map id = id

@[simp]

theorem FirstOrder.Language.Atom.map_map {L : Language} {α : Type w} {β : Type x} {γ : Type u_1} (f : α → β) (g : β → γ) (a : L.Atom α) : map g (map f a) = map (g ∘ f) a

def FirstOrder.Language.Atom.Realize {L : Language} {α : Type w} {M : Type y} [L.Structure M] (a : L.Atom α) (v : α → M) : Prop

An assignment realizes an atom when the relation holds of the values of its variables.

Equations

• a.Realize v = FirstOrder.Language.Structure.RelMap a.rel (v ∘ a.args)

@[simp]

theorem FirstOrder.Language.Atom.realize_mk {L : Language} {α : Type w} {M : Type y} [L.Structure M] {n : ℕ} (R : L.Relations n) (xs : Fin n → α) (v : α → M) : { arity := n, rel := R, args := xs }.Realize v ↔ Structure.RelMap R (v ∘ xs)

@[simp]

theorem FirstOrder.Language.Atom.realize_map {L : Language} {α : Type w} {β : Type x} {M : Type y} [L.Structure M] {f : α → β} {a : L.Atom α} {v : β → M} : (map f a).Realize v ↔ a.Realize (v ∘ f)

def FirstOrder.Language.Atom.toFormula {L : Language} {α : Type w} (a : L.Atom α) : L.Formula α

An atom as an atomic formula.

Equations

• a.toFormula = a.rel.formula (FirstOrder.Language.var ∘ a.args)

@[simp]

theorem FirstOrder.Language.Atom.realize_toFormula {L : Language} {α : Type w} {M : Type y} [L.Structure M] {a : L.Atom α} {v : α → M} : a.toFormula.Realize v ↔ a.Realize v

@[instance_reducible]

instance FirstOrder.Language.Atom.instMulActionPerm {L : Language} {α : Type w} : MulAction (Equiv.Perm α) (L.Atom α)

Permutations of the variables act on atoms by renaming.

Equations

• FirstOrder.Language.Atom.instMulActionPerm = { smul := fun (σ : Equiv.Perm α) (a : L.Atom α) => FirstOrder.Language.Atom.map (⇑σ) a, mul_smul := ⋯, one_smul := ⋯ }

theorem FirstOrder.Language.Atom.smul_def {L : Language} {α : Type w} (σ : Equiv.Perm α) (a : L.Atom α) : σ • a = map (⇑σ) a

def FirstOrder.Language.Atom.realizers {L : Language} {α : Type w} (M : Type y) [L.Structure M] (T : Set (L.Atom α)) : Set (α → M)

The assignments that realize every atom of a set.

Equations

• FirstOrder.Language.Atom.realizers M T = upperPolar (fun (a : L.Atom α) (v : α → M) => a.Realize v) T

theorem FirstOrder.Language.Atom.mem_realizers {L : Language} {α : Type w} {M : Type y} [L.Structure M] {T : Set (L.Atom α)} {v : α → M} : v ∈ realizers M T ↔ ∀ a ∈ T, a.Realize v

theorem FirstOrder.Language.Atom.realizers_union {L : Language} {α : Type w} {M : Type y} [L.Structure M] (T₁ T₂ : Set (L.Atom α)) : realizers M (T₁ ∪ T₂) = realizers M T₁ ∩ realizers M T₂

theorem FirstOrder.Language.Atom.realizers_anti {L : Language} {α : Type w} {M : Type y} [L.Structure M] : Antitone (realizers M)

theorem FirstOrder.Language.Atom.mem_realizers_image_map {L : Language} {α : Type w} {β : Type x} {M : Type y} [L.Structure M] {T : Set (L.Atom α)} {f : α → β} {v : β → M} : v ∈ realizers M (map f '' T) ↔ v ∘ f ∈ realizers M T

theorem FirstOrder.Language.Atom.mem_realizers_smul {L : Language} {α : Type w} {M : Type y} [L.Structure M] {T : Set (L.Atom α)} {v : α → M} {σ : Equiv.Perm α} : v ∈ realizers M (σ • T) ↔ v ∘ ⇑σ ∈ realizers M T

theorem FirstOrder.Language.Atom.comp_mem_realizers {L : Language} {α : Type w} {M : Type y} [L.Structure M] {T : Set (L.Atom α)} {v : α → M} {N : Type u_1} [L.Structure N] (φ : L.Hom M N) (hv : v ∈ realizers M T) : ⇑φ ∘ v ∈ realizers N T

A homomorphism carries an assignment realizing a set of atoms to one realizing it.

def FirstOrder.Language.Atom.Canonical {L : Language} {α : Type w} : Set (L.Atom α) → Type w

The structure a set of atoms presents on its variables.

Equations

• FirstOrder.Language.Atom.Canonical x✝ = α

def FirstOrder.Language.Atom.Canonical.of {L : Language} {α : Type w} (T : Set (L.Atom α)) : α → Canonical T

A variable, as an element of the canonical structure.

Equations

• FirstOrder.Language.Atom.Canonical.of T = id

@[instance_reducible]

instance FirstOrder.Language.Atom.Canonical.instStructure {L : Language} {α : Type w} [L.IsRelational] (T : Set (L.Atom α)) : L.Structure (Canonical T)

Equations

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

theorem FirstOrder.Language.Atom.Canonical.of_comp_mem_realizers_iff {L : Language} {α : Type w} {β : Type x} {T : Set (L.Atom α)} [L.IsRelational] {B : Set (L.Atom β)} {f : α → β} : of B ∘ f ∈ realizers (Canonical B) T ↔ map f '' T ⊆ B

A map of variables realizes a set of atoms in the canonical structure of another exactly when it carries the first into the second.

theorem FirstOrder.Language.Atom.Canonical.of_mem_realizers {L : Language} {α : Type w} [L.IsRelational] (T : Set (L.Atom α)) : of T ∈ realizers (Canonical T) T

def FirstOrder.Language.Atom.Canonical.homEquiv {L : Language} {α : Type w} {M : Type y} [L.Structure M] [L.IsRelational] (T : Set (L.Atom α)) : L.Hom (Canonical T) M ≃ ↑(realizers M T)

The homomorphisms out of the canonical structure are the realizing assignments.

Equations

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

theorem FirstOrder.Language.Atom.forall_realizers_subset_preimage_iff {L : Language} {α : Type w} {β : Type x} {T : Set (L.Atom α)} [L.IsRelational] {B : Set (L.Atom β)} {f : α → β} : (∀ (M : Type x) [inst : L.Structure M], realizers M B ⊆ (fun (x : β → M) => x ∘ f) ⁻¹' realizers M T) ↔ map f '' T ⊆ B

One set of atoms entails another along a map of variables in every structure exactly when the map carries the atoms of the second into the first.