Lax Lean Archive

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

Independent sets lift and project through a blow-up

Lax263307.BlowUpIndependentSets · concepts/Lax263307/BlowUpIndependentSets.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

    An independent set of the original graph lifts to an independent set containing all its copies. An independent set of copies projects to an independent set of the original graph. The lift of II has size ∑v∈Itv\sum_{v\in I}t_v, and every set of copies KK satisfies ∣K∣≤∑v∈project⁡(K)tv|K|\le\sum_{v\in\operatorname{project}(K)}t_v. The blow-up graph has ∑vtv\sum_v t_v vertices.

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

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

    1 lift_cardinality proven

    2 lift_independent proven

    3 order_eq proven

    4 project_independent proven

    5 projection_capacity proven

    Lean source view on GitHub

    1import Lax263307.IndependentBlowUp
    2
    3/-!
    4---
    5title: Independent sets lift and project through a blow-up
    6type: theorem
    7---
    8An independent set of the original graph lifts to an independent set
    9containing all its copies. An independent set of copies projects to an
    10independent set of the original graph. The lift of II has size
    11∑v∈Itv\sum_{v\in I}t_v, and every set of copies KK satisfies
    12∣K∣≤∑v∈project⁡(K)tv|K|\le\sum_{v\in\operatorname{project}(K)}t_v.
    13The blow-up graph has ∑vtv\sum_v t_v vertices.
    14
    15# Attribution
    16
    17Bonnet–Chang, Section 6, the independent blow-up construction.
    18-/
    19
    20namespace Lax263307.BlowUpIndependentSets
    21
    22open IndependentBlowUp
    23
    24/-- Taking all copies preserves independence. -/
    25axiom lift_independent {n : ℕ} (G : SimpleGraph (Fin n)) (copies : Fin n → ℕ)
    26 (I : Finset (Fin n)) (independent : G.IsIndepSet (I : Set (Fin n))) :
    27 (graph G copies).IsIndepSet (lift copies I : Set (Vertex copies))
    28
    29/-- Projecting any independent set of copies preserves independence. -/
    30axiom project_independent {n : ℕ} (G : SimpleGraph (Fin n)) (copies : Fin n → ℕ)
    31 (K : Finset (Vertex copies)) (independent : (graph G copies).IsIndepSet (K : Set (Vertex copies))) :
    32 G.IsIndepSet (project K : Set (Fin n))
    33
    34/-- The lift contains exactly the sum of the selected vertices' multiplicities. -/
    35axiom lift_cardinality {n : ℕ} (copies : Fin n → ℕ) (I : Finset (Fin n)) :
    36 (lift copies I).card = ∑ v ∈ I, copies v
    37
    38/-- A set of copies is contained in the complete lift of its projection. -/
    39axiom projection_capacity {n : ℕ} (copies : Fin n → ℕ) (K : Finset (Vertex copies)) :
    40 K.card ≤ ∑ v ∈ project K, copies v
    41
    42/-- The blow-up order is exactly the total number of copies. -/
    43axiom order_eq {n : ℕ} (copies : Fin n → ℕ) :
    44 Fintype.card (Vertex copies) = ∑ v, copies v
    45
    46end Lax263307.BlowUpIndependentSets
    47
    Show ProofShow ProofShow ProofShow ProofShow Proof

    Attribution

    Bonnet–Chang, Section 6, the independent blow-up construction.

    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…