While this submission is a draft, it cannot be used by other submissions.

Treewidth, pathwidth, and treedepth of patterns

Lax461425.PatternWidths · concepts/Lax461425/PatternWidths.lean · lax-461425

definition

Loading review…

Sign in with ORCID

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 treewidth, pathwidth, and treedepth of a pattern are those of its underlying simple graph, so edge multiplicities play no role. A pattern has treewidth at most kk if it has a tree decomposition whose bags have at most k+1k + 1 vertices, and pathwidth at most kk if it has such a decomposition whose tree is a path. It has treedepth at most tt if it has an elimination forest in which every root-leaf path has at most tt vertices. The pattern without vertices has treewidth, pathwidth, and treedepth zero.

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

    Lean source view on GitHub

    1import Lax228581.Treewidth
    2import Lax183560.TreeDepth
    3import Lax183560.Pathwidth
    4import Lax461425.HomomorphismPolynomials
    5
    6/-!
    7---
    8title: Treewidth, pathwidth, and treedepth of patterns
    9type: definition
    10---
    11The treewidth, pathwidth, and treedepth of a pattern are those of its underlying simple graph,
    12so edge multiplicities play no role. A pattern has treewidth at most kk if it has a tree
    13decomposition whose bags have at most k+1k + 1 vertices, and pathwidth at most kk if it has
    14such a decomposition whose tree is a path. It has treedepth at most tt if it has an
    15elimination forest in which every root-leaf path has at most tt vertices. The pattern without
    16vertices has treewidth, pathwidth, and treedepth zero.
    17-/
    18
    19namespace Lax461425.PatternWidths
    20
    21open HomomorphismPolynomials
    22
    23/-- The pattern has treewidth at most `k`: its underlying simple graph has a tree decomposition
    24with bags of size at most `k + 1`. -/
    25def TreewidthLE (k : ℕ) (F : Pattern) : Prop :=
    26 Lax228581.Treewidth.HasTreewidthAtMost (underlying F) k
    27
    28/-- The pattern has pathwidth at most `k`: its underlying simple graph has a path
    29decomposition with bags of size at most `k + 1`. -/
    30def PathwidthLE (k : ℕ) (F : Pattern) : Prop :=
    31 Lax183560.Pathwidth.HasPathwidthAtMost (underlying F) k
    32
    33/-- The pattern has treedepth at most `t`: its underlying simple graph lies in the closure of a
    34rooted forest in which every root-leaf path has at most `t` vertices. -/
    35def TreedepthLE (t : ℕ) (F : Pattern) : Prop :=
    36 Lax183560.TreeDepth.HasTreedepthAtMost (underlying F) t
    37
    38end Lax461425.PatternWidths
    39

    Discussion

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

    Loading discussion…