Lax Lean Archive

Atomic types of vertices and of pairs

Lax185574.AtomicTypes · concepts/Lax185574/AtomicTypes.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The atomic type of a tuple v̄ over a set Y of elements of a structure A is atp^A(v̄/Y) ≔ tp^A_0(v̄/Y), and ATypes^A(X/Y) ≔ Types^A_{1,0}(X/Y) is the set of atomic types over Y of the elements of X.

    For a graph, Π = {(x = y), (x ≠ y) ∧ E(x, y), (x ≠ y) ∧ ¬E(x, y)} is the set of the three possible atomic types of a pair of vertices. For an s-tuple p̄ = (p₁, …, p_s) of vertices and a vertex v, the atomic type atp(v/p̄) is identified with the s-tuple in Π^s whose i-th component is the atomic type of the pair (v, pᵢ).

    Concept map
    2 concepts; 7 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 20 of this submission's paper
    • page 14 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.FirstOrderTypes
    2import Mathlib.ModelTheory.Graph
    3
    4/-!
    5---
    6title: Atomic types of vertices and of pairs
    7type: definition
    8---
    9The *atomic type* of a tuple v̄ over a set Y of elements of a structure A
    10is atp^A(v̄/Y) ≔ tp^A_0(v̄/Y), and ATypes^A(X/Y) ≔ Types^A_{1,0}(X/Y) is
    11the set of atomic types over Y of the elements of X.
    12
    13For a graph, Π = {(x = y), (x ≠ y) ∧ E(x, y), (x ≠ y) ∧ ¬E(x, y)} is the
    14set of the three possible atomic types of a pair of vertices. For an
    15s-tuple p̄ = (p₁, …, p_s) of vertices and a vertex v, the atomic type
    16atp(v/p̄) is identified with the s-tuple in Π^s whose i-th component is
    17the atomic type of the pair (v, pᵢ).
    18
    19# Formalization notes
    20
    21The number |ATypes^G(X/Y)| is `atomicTypeCount`. It is literally the
    22number of types of quantifier rank 0 of single vertices of X over Y in
    23the structure of the graph G, as defined in `FirstOrderTypes`.
    24
    25The three atomic types of a pair form the type `PairType`, and
    26atp(v/p̄) is `atomicTypeOver G p v`. The partition 𝒫_S of V(G) into
    27atomic types over a set S is `Partitions.atomicTypes`. Two vertices have
    28the same atomic type over a tuple p̄ exactly when they lie in the same
    29part of 𝒫_S for the set S of entries of p̄.
    30-/
    31
    32namespace Lax185574.AtomicTypes
    33
    34open FirstOrder FirstOrder.Language
    35open Lax185574.FirstOrderTypes
    36
    37universe u
    38
    39variable {V : Type u}
    40
    41/-- `|ATypes^G(X/Y)|`: the number of atomic types over `Y`, in the graph
    42`G`, of the vertices of `X`. -/
    43noncomputable def atomicTypeCount (G : SimpleGraph V) (X Y : Set V) : ℕ :=
    44 @typeCountOver Language.graph V G.structure 1 0 X Y
    45
    46/-- The three atomic types of a pair of vertices in a graph, the set Π. -/
    47inductive PairType
    48 /-- The type `x = y`. -/
    49 | eq
    50 /-- The type `x ≠ y ∧ E(x, y)`. -/
    51 | adj
    52 /-- The type `x ≠ y ∧ ¬E(x, y)`. -/
    53 | nonAdj
    54 deriving DecidableEq
    55
    56/-- There are three atomic types of pairs. -/
    57instance : Fintype PairType :=
    58 ⟨{.eq, .adj, .nonAdj}, fun x => by cases x <;> decide⟩
    59
    60open Classical in
    61/-- The atomic type of the pair `(u, v)` in the graph `G`. -/
    62noncomputable def pairType (G : SimpleGraph V) (u v : V) : PairType :=
    63 if u = v then .eq else if G.Adj u v then .adj else .nonAdj
    64
    65/-- `atp(v/p̄)`, as an element of `Π^s`: its `i`-th component is the
    66atomic type of the pair `(v, pᵢ)`. -/
    67noncomputable def atomicTypeOver (G : SimpleGraph V) {s : ℕ} (p : Fin s → V)
    68 (v : V) : Fin s → PairType :=
    69 fun i => pairType G v (p i)
    70
    71end Lax185574.AtomicTypes
    72
    Formalization notes

    The number |ATypes^G(X/Y)| is atomicTypeCountatomicTypeCount. It is literally the number of types of quantifier rank 0 of single vertices of X over Y in the structure of the graph G, as defined in FirstOrderTypesFirstOrderTypes.

    The three atomic types of a pair form the type PairTypePairType, and atp(v/p̄) is atomicTypeOverGpvatomicTypeOver G p v. The partition 𝒫_S of V(G) into atomic types over a set S is Partitions.atomicTypesPartitions.atomicTypes. Two vertices have the same atomic type over a tuple p̄ exactly when they lie in the same part of 𝒫_S for the set S of entries of p̄.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…