Factors of relational structures

A k-factor is a connected structure on at most k elements, presented by a set of atoms on Fin n whose Gaifman graph is connected. It occurs in a structure when some assignment realizes its atoms there, that is, when its canonical structure maps homomorphically into the structure. Homomorphisms are the weak ones of mathlib, so a factor may leave a relation unsaid, and a factor occurring in a structure occurs in every structure it maps into.

Main definitions

• FirstOrder.Language.Atom.gaifman: the Gaifman graph of a set of atoms.
• FirstOrder.Language.Factor: connected sets of atoms on at most k variables.
• FirstOrder.Language.Factor.Occurs, FirstOrder.Language.factors: occurrence, and the k-factors of a structure.

Main statements

• FirstOrder.Language.Factor.occurs_iff_nonempty_hom: a factor occurs exactly when its canonical structure maps homomorphically into the structure.
• FirstOrder.Language.factors_mono: a homomorphism carries the factors of its domain to factors of its codomain.

References

• [Lib04]
• [RL19]

def FirstOrder.Language.Atom.gaifman {L : Language} {α : Type w} (T : Set (L.Atom α)) : SimpleGraph α

The Gaifman graph of a set of atoms joins two distinct variables that an atom mentions together.

Equations

• FirstOrder.Language.Atom.gaifman T = SimpleGraph.fromRel fun (x y : α) => ∃ a ∈ T, x ∈ Set.range a.args ∧ y ∈ Set.range a.args

structure FirstOrder.Language.Factor (L : Language) (k : ℕ) : Type v

A k-factor is a connected set of atoms on at most k variables, presenting a connected structure on at most k elements.

• n : ℕ

  The number of variables.

• le : self.n ≤ k
• atoms : Set (L.Atom (Fin self.n))

  The atoms.

• preconnected : (Atom.gaifman self.atoms).Preconnected

def FirstOrder.Language.Factor.Occurs {L : Language} {k : ℕ} (M : Type w) [L.Structure M] (f : L.Factor k) : Prop

A factor occurs in a structure when some assignment realizes its atoms there.

Equations

• FirstOrder.Language.Factor.Occurs M f = (FirstOrder.Language.Atom.realizers M f.atoms).Nonempty

theorem FirstOrder.Language.Factor.occurs_iff_nonempty_hom {L : Language} {k : ℕ} {M : Type w} [L.Structure M] {f : L.Factor k} [L.IsRelational] : Occurs M f ↔ Nonempty (L.Hom (Atom.Canonical f.atoms) M)

A factor occurs exactly when its canonical structure maps homomorphically into the structure.

theorem FirstOrder.Language.Factor.Occurs.hom {L : Language} {k : ℕ} {M : Type w} {N : Type x} [L.Structure M] [L.Structure N] {f : L.Factor k} (φ : L.Hom M N) : Occurs M f → Occurs N f

A homomorphism carries an occurrence of a factor to an occurrence.

def FirstOrder.Language.factors (L : Language) (k : ℕ) (M : Type w) [L.Structure M] : Set (L.Factor k)

The k-factors of a structure are the factors occurring in it.

Equations

• L.factors k M = {f : L.Factor k | FirstOrder.Language.Factor.Occurs M f}

@[simp]

theorem FirstOrder.Language.mem_factors {L : Language} {k : ℕ} {M : Type w} [L.Structure M] {f : L.Factor k} : f ∈ L.factors k M ↔ Factor.Occurs M f

theorem FirstOrder.Language.factors_mono {L : Language} {k : ℕ} {M : Type w} {N : Type x} [L.Structure M] [L.Structure N] (φ : L.Hom M N) : L.factors k M ⊆ L.factors k N

A homomorphism carries the factors of its domain to factors of its codomain.