Gaifman graph, distances, balls and induced substructures
Lax185574.GaifmanGraph · concepts/Lax185574/GaifmanGraph.lean · lax-185574
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The Gaifman graph of a relational structure A with domain V has vertex set V. Two distinct elements are adjacent if they occur together in some tuple of some relation of A. For a structure with unary and binary relations, these are the pairs uv such that (u, v) or (v, u) lies in a binary relation. The distance dist^A(u, v) is the distance in the Gaifman graph, and Ball^A_r(ā) is the set of elements at distance at most r from some entry of the tuple ā.
For a set B of elements of a relational structure A, the induced substructure A[B] has domain B, and each relation of A is restricted to B. The paper uses A[B] without defining it.
Concept map
In the paper
- page 14 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Basic |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Walk.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Gaifman graph, distances, balls and induced substructures |
| 7 | type: definition |
| 8 | --- |
| 9 | The *Gaifman graph* of a relational structure A with domain V has |
| 10 | vertex set V. Two distinct elements are adjacent if they occur together |
| 11 | in some tuple of some relation of A. For a structure with unary and |
| 12 | binary relations, these are the pairs uv such that (u, v) or (v, u) lies |
| 13 | in a binary relation. The distance dist^A(u, v) is the distance in the |
| 14 | Gaifman graph, and Ball^A_r(ā) is the set of elements at distance at |
| 15 | most r from some entry of the tuple ā. |
| 16 | |
| 17 | For a set B of elements of a relational structure A, the *induced |
| 18 | substructure* A[B] has domain B, and each relation of A is restricted |
| 19 | to B. The paper uses A[B] without defining it. |
| 20 | |
| 21 | # Formalization notes |
| 22 | |
| 23 | "At distance at most r" is witnessed by a walk of length at most r, as |
| 24 | in `Lax3.ColoredGraphs`. Elements in different components are therefore |
| 25 | at infinite distance. The induced substructure is defined for relational |
| 26 | languages, where every subset is closed under the (absent) functions. |
| 27 | Its domain is the subtype of `B`. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax185574.GaifmanGraph |
| 31 | |
| 32 | open FirstOrder FirstOrder.Language |
| 33 | |
| 34 | universe u v z |
| 35 | |
| 36 | variable {L : Language.{u, v}} {V : Type z} [L.Structure V] |
| 37 | |
| 38 | variable (L) in |
| 39 | /-- The Gaifman graph: distinct elements are adjacent if they occur |
| 40 | together in a tuple of some relation. -/ |
| 41 | def gaifmanGraph : SimpleGraph V := |
| 42 | SimpleGraph.fromRel fun a b => |
| 43 | ∃ (l : ℕ) (R : L.Relations l) (x : Fin l → V), |
| 44 | Structure.RelMap R x ∧ a ∈ Set.range x ∧ b ∈ Set.range x |
| 45 | |
| 46 | /-- The vertices `u` and `v` of the graph `G` are within distance `d`: |
| 47 | some walk from `u` to `v` has length at most `d`. -/ |
| 48 | def WithinDist {W : Type*} (G : SimpleGraph W) (d : ℕ) (u v : W) : Prop := |
| 49 | ∃ p : G.Walk u v, p.length ≤ d |
| 50 | |
| 51 | variable (L) in |
| 52 | /-- `Ball^A_r(ā)`: the elements within distance `r` of some entry of the |
| 53 | tuple `a` in the Gaifman graph. -/ |
| 54 | def ball (r : ℕ) {k : ℕ} (a : Fin k → V) : Set V := |
| 55 | {b | ∃ i, WithinDist (gaifmanGraph L (V := V)) r (a i) b} |
| 56 | |
| 57 | /-- The induced substructure `A[B]` of a relational structure: the |
| 58 | relations of `A`, restricted to `B`. -/ |
| 59 | @[implicit_reducible] |
| 60 | def induced [L.IsRelational] (B : Set V) : L.Structure B where |
| 61 | funMap f := isEmptyElim f |
| 62 | RelMap R x := Structure.RelMap R (fun i => (x i : V)) |
| 63 | |
| 64 | end Lax185574.GaifmanGraph |
| 65 |
Formalization notes
"At distance at most r" is witnessed by a walk of length at most r, as in . Elements in different components are therefore at infinite distance. The induced substructure is defined for relational languages, where every subset is closed under the (absent) functions. Its domain is the subtype of .
Builds on
none
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments