Lax Lean Archive

The Chandra–Merlin theorem

Lax420092.ChandraMerlin · concepts/Lax420092/ChandraMerlin.lean · lax-420092

proven

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

    Theorem

    The left query of a pair is contained in the right one exactly when there is a homomorphism from the right query to the canonical database of the left one: a map of the universe to itself, fixing the constants, that sends every atom of the right query to an atom of the left query. This is the theorem of Chandra and Merlin (1977), at the schema of graph databases.

    Concept map
    11 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Interpretations
    3import Lax904597.Classes
    4import Lax799700.Problems
    5import Lax420092.QueryDatabases
    6import Lax420092.Evaluation
    7import Lax420092.QueryPairs
    8import Lax420092.PackagedInstances
    9
    10/-!
    11---
    12title: The Chandra–Merlin theorem
    13type: theorem
    14---
    15The left query of a pair is contained in the right one exactly when there is
    16a homomorphism from the right query to the canonical database of the left
    17one: a map of the universe to itself, fixing the constants, that sends every
    18atom of the right query to an atom of the left query. This is the theorem of
    19Chandra and Merlin (1977), at the schema of graph databases.
    20-/
    21
    22namespace Lax420092.ChandraMerlin
    23
    24open FirstOrder FirstOrder.Language
    25open Lax904597.Problems Lax904597.Interpretations Lax904597.Classes Lax799700.Problems
    26open Lax420092.QueryDatabases Lax420092.Evaluation Lax420092.QueryPairs Lax420092.PackagedInstances
    27
    28/-- The Chandra–Merlin theorem. -/
    29axiom queryContained_iff_hom : ∀ (A : Type) [queryPair.Structure A],
    30 QueryContained A ↔ CQHom (PairVar (A := A)) (RAtom (A := A)) (LAtom (A := A))
    31
    32end Lax420092.ChandraMerlin
    33
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…