Relations as structures in the language of graphs

[UPSTREAM] candidate. Mathlib makes a simple graph a structure in the language of graphs; any binary relation is one as well, with its pairs as the adjacency relation (graphStructure). A Lindström quantifier over the language of graphs, a quantifier of type ⟨2⟩, is then a graph property, an isomorphism-invariant class of binary relations, built from any property of relations that relabelling along a bijection preserves (LindstromQuantifier.ofGraphProperty). Its relativization to a set A asks it of A with the relation restricted to A (inducedGraph).

Main definitions

• FirstOrder.Language.graphStructure r: the structure in the language of graphs whose adjacency relation is r.
• FirstOrder.Language.graphStructureEquiv: a bijection carrying one relation to another is an isomorphism of these structures.
• FirstOrder.Language.inducedGraph r A: the set A with r restricted to it.
• FirstOrder.Language.LindstromQuantifier.ofGraphProperty: the type ⟨2⟩ quantifier of a graph property, a property of relations invariant under relabelling.

References

• [PW06]

@[instance_reducible]

def FirstOrder.Language.graphStructure {M : Type u} (r : M → M → Prop) : Language.graph.Structure M

The structure in the language of graphs whose adjacency relation is r.

Equations

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

@[simp]

theorem FirstOrder.Language.relMap_graphStructure {M : Type u} (r : M → M → Prop) (x y : M) : Structure.RelMap adj ![x, y] ↔ r x y

def FirstOrder.Language.graphStructureEquiv {M N : Type u} {r : M → M → Prop} {s : N → N → Prop} (e : M ≃ N) (h : ∀ (x y : M), s (e x) (e y) ↔ r x y) : Language.graph.Equiv M N

A bijection carrying r to s is an isomorphism of the structures they define.

Equations

• FirstOrder.Language.graphStructureEquiv e h = { toEquiv := e, map_fun' := ⋯, map_rel' := ⋯ }

@[reducible, inline]

abbrev FirstOrder.Language.inducedGraph {M : Type u} (r : M → M → Prop) (A : Set M) : CategoryTheory.Bundled Language.graph.Structure

The set A with r restricted to it, as a structure in the language of graphs.

Equations

• FirstOrder.Language.inducedGraph r A = { α := ↑A, str := FirstOrder.Language.graphStructure fun (a b : ↑A) => r ↑a ↑b }

def FirstOrder.Language.LindstromQuantifier.ofGraphProperty (P : {M : Type u} → (M → M → Prop) → Prop) (hP : ∀ {M N : Type u} (e : M ≃ N) (s : N → N → Prop), (P fun (x y : M) => s (e x) (e y)) ↔ P s) : Language.graph.LindstromQuantifier

The type ⟨2⟩ quantifier of a graph property P, holding of a structure whose adjacency relation has P; relabelling along a bijection preserves P.

Equations

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

theorem FirstOrder.Language.LindstromQuantifier.mem_holds_ofGraphProperty {P : {M : Type u} → (M → M → Prop) → Prop} {hP : ∀ {M N : Type u} (e : M ≃ N) (s : N → N → Prop), (P fun (x y : M) => s (e x) (e y)) ↔ P s} {M : CategoryTheory.Bundled Language.graph.Structure} : M ∈ (ofGraphProperty (fun {M : Type u} => P) hP).holds ↔ P fun (x y : ↑M) => Structure.RelMap adj ![x, y]