Lax Lean Archive

Roberson's conjecture

Lax871432.RobersonConjecture · concepts/Lax871432/RobersonConjecture.lean · lax-871432

open

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

    Conjecture

    Roberson (2022) conjectured that every graph class closed under taking minors and disjoint unions is homomorphism distinguishing closed: for such a class F\mathcal{F}, adding any further graph to F\mathcal{F} strictly refines ≡F\equiv_{\mathcal{F}}.

    Concept map
    9 concepts
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax871432.ClosureProperties
    2import Lax871432.DistinguishingClosure
    3
    4/-!
    5---
    6title: Roberson's conjecture
    7type: conjecture
    8---
    9Roberson (2022) conjectured that every graph class closed under taking minors and disjoint
    10unions is homomorphism distinguishing closed: for such a class F\mathcal{F}, adding any
    11further graph to F\mathcal{F} strictly refines ≡F\equiv_{\mathcal{F}}.
    12
    13# Implementation notes
    14
    15The class is assumed to be nonempty. The empty class is closed under taking minors and
    16disjoint unions, but it is not homomorphism distinguishing closed: the graph with no vertices
    17has exactly one homomorphism into every graph, so it lies in cl(∅)\mathrm{cl}(\emptyset). For a
    18nonempty minor-closed class the question does not arise, since the graph with no vertices is
    19a minor of every graph and hence belongs to the class.
    20-/
    21
    22open Lax871432.ClosureProperties Lax871432.DistinguishingClosure
    23open Lax871432.GraphClasses
    24
    25namespace Lax871432.RobersonConjecture
    26
    27/-- **Roberson's conjecture.** Every nonempty, minor-closed, union-closed class of finite
    28simple graphs is homomorphism distinguishing closed. -/
    29axiom isHomDistinguishingClosed_of_isMinorClosed_of_isUnionClosed (𝓕 : GraphClass)
    30 (hne : ∃ (n : ℕ) (F : SimpleGraph (Fin n)), 𝓕.Mem F) :
    31 IsMinorClosed 𝓕 → IsUnionClosed 𝓕 → IsHomDistinguishingClosed 𝓕
    32
    33end Lax871432.RobersonConjecture
    34

    Implementation notes

    The class is assumed to be nonempty. The empty class is closed under taking minors and disjoint unions, but it is not homomorphism distinguishing closed: the graph with no vertices has exactly one homomorphism into every graph, so it lies in cl(∅)\mathrm{cl}(\emptyset). For a nonempty minor-closed class the question does not arise, since the graph with no vertices is a minor of every graph and hence belongs to the class.

    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…