Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax68.GraphTopologicalMinors

Topological graph minors

concepts/Lax68/GraphTopologicalMinors.lean · lax-68

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.

    Concept map

    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A graph H is a topological minor of G when the vertices of H are represented by distinct branch vertices of G and its edges by paths whose interiors contain no branch vertex and are pairwise disjoint. Equivalently, G contains a subdivision of H as a subgraph.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Paths
    2import Lax68.GraphMinors
    3
    4/-!
    5---
    6title: Topological graph minors
    7type: definition
    8---
    9A graph *H* is a topological minor of *G* when the vertices of *H* are
    10represented by distinct branch vertices of *G* and its edges by paths whose
    11interiors contain no branch vertex and are pairwise disjoint. Equivalently,
    12*G* contains a subdivision of *H* as a subgraph.
    13-/
    14
    15set_option autoImplicit false
    16
    17namespace Lax68.GraphTopologicalMinors
    18
    19open GraphMinors
    20
    21def walkInterior {V : Type*} {G : SimpleGraph V} {a b : V}
    22 (P : G.Walk a b) : Set V :=
    23 {x | x ∈ P.support ∧ x ≠ a ∧ x ≠ b}
    24
    25structure TopologicalMinorModel {W V : Type*}
    26 (H : SimpleGraph W) (G : SimpleGraph V) where
    27 branch : W ↪ V
    28 route :
    29 ∀ {a b : W}, H.Adj a b →
    30 G.Walk (branch a) (branch b)
    31 route_isPath :
    32 ∀ {a b : W} (h : H.Adj a b),
    33 (route h).IsPath
    34 branch_avoids_interiors :
    35 ∀ {a b : W} (h : H.Adj a b) (w : W),
    36 branch w ∉ walkInterior (route h)
    37 route_interiors_disjoint :
    38 ∀ {a b c d : W}
    39 (hab : H.Adj a b) (hcd : H.Adj c d),
    40 ¬ ((a = c ∧ b = d) ∨ (a = d ∧ b = c)) →
    41 Disjoint
    42 (walkInterior (route hab))
    43 (walkInterior (route hcd))
    44
    45def IsTopologicalMinor {W V : Type*}
    46 (H : SimpleGraph W) (G : SimpleGraph V) : Prop :=
    47 Nonempty (TopologicalMinorModel H G)
    48
    49def IsKuratowskiFree {V : Type*} (G : SimpleGraph V) : Prop :=
    50 ¬IsTopologicalMinor K5 G ∧
    51 ¬IsTopologicalMinor K33 G
    52
    53end Lax68.GraphTopologicalMinors
    54

    Builds on

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…