Lax Lean Archive

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

Independent blow-up classes are hereditary

Lax263307.BlowUpClasses · concepts/Lax263307/BlowUpClasses.lean · lax-263307

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 independent blow-up closure of a graph class consists of finite graphs whose vertices project to a member of that class, with adjacency exactly determined by adjacency of the projected vertices. This closure is hereditary. The explicitly constructed copy graphs belong to it after relabeling.

    Concept map
    5 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 copy_graph_mem proven

    2 hereditary_closure proven

    Lean source view on GitHub

    1import Lax263307.GraphClasses
    2import Lax263307.IndependentBlowUp
    3
    4/-!
    5---
    6title: Independent blow-up classes are hereditary
    7type: theorem
    8---
    9The independent blow-up closure of a graph class consists of finite graphs
    10whose vertices project to a member of that class, with adjacency exactly
    11determined by adjacency of the projected vertices. This closure is hereditary.
    12The explicitly constructed copy graphs belong to it after relabeling.
    13
    14# Formalization notes
    15
    16Projection fibres are independent, and between two fibres all edges or no
    17edges are present. Empty fibres are allowed, matching the zero multiplicities
    18in the weighted reduction. With this convention the closure is hereditary
    19for every original class. For a hereditary original class it agrees with
    20the paper's convention of nonempty fibres: delete the unused host vertices
    21before constructing the blow-up.
    22
    23# Attribution
    24
    25Bonnet–Chang, the hereditary-closure assertion in Lemma 16.
    26-/
    27
    28namespace Lax263307.BlowUpClasses
    29
    30open GraphClasses IndependentBlowUp
    31
    32/-- Graphs obtained by independent blow-ups of members, allowing empty fibres. -/
    33def blowUpClass (C : GraphClass) : GraphClass :=
    34 fun m => {H | ∃ (n : ℕ) (G : SimpleGraph (Fin n)), G ∈ C n ∧
    35 ∃ projection : Fin m → Fin n,
    36 ∀ u v, H.Adj u v ↔ G.Adj (projection u) (projection v)}
    37
    38/-- Restricting an independent blow-up to any induced subgraph remains a blow-up. -/
    39axiom hereditary_closure (C : GraphClass) : IsHereditary (blowUpClass C)
    40
    41/-- Relabeling the explicit copy graph places it in the blow-up closure. -/
    42axiom copy_graph_mem (C : GraphClass) {n : ℕ} (G : SimpleGraph (Fin n))
    43 (member : G ∈ C n) (copies : Fin n → ℕ) (m : ℕ) (labeling : Fin m ≃ Vertex copies) :
    44 (graph G copies).comap labeling ∈ blowUpClass C m
    45
    46end Lax263307.BlowUpClasses
    47
    Show ProofShow Proof
    Formalization notes

    Projection fibres are independent, and between two fibres all edges or no edges are present. Empty fibres are allowed, matching the zero multiplicities in the weighted reduction. With this convention the closure is hereditary for every original class. For a hereditary original class it agrees with the paper's convention of nonempty fibres: delete the unused host vertices before constructing the blow-up.

    Attribution

    Bonnet–Chang, the hereditary-closure assertion in Lemma 16.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…