Lax Lean Archive

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

Independent blow-ups and projection

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

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.

    Natural Language Statement

    Definition

    For a graph GG and nonnegative integer multiplicities tvt_v, replace vertex vv by an independent set of tvt_v copies. Copies of distinct vertices are adjacent exactly when their original vertices are adjacent. Zero multiplicities omit vertices. Lift a vertex set by taking all of its copies; project a set of copies by taking the vertices represented by at least one selected copy.

    Concept map
    3 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax263307.WeightedIndependentSet
    2import Mathlib.Combinatorics.SimpleGraph.Maps
    3import Mathlib.Data.Finset.Sigma
    4import Mathlib.Data.Fintype.BigOperators
    5
    6/-!
    7---
    8title: Independent blow-ups and projection
    9type: definition
    10---
    11For a graph GG and nonnegative integer multiplicities tvt_v, replace vertex
    12vv by an independent set of tvt_v copies. Copies of distinct vertices are
    13adjacent exactly when their original vertices are adjacent. Zero multiplicities
    14omit vertices. Lift a vertex set by taking all of its copies; project a set
    15of copies by taking the vertices represented by at least one selected copy.
    16
    17# Formalization notes
    18
    19A copy is a pair (v,i)(v,i) with 0≤i<tv0\le i<t_v. This dependent pair type has
    20exactly ∑vtv\sum_v t_v elements and admits the usual finite-type instances.
    21The blow-up graph is the comap of GG along the projection to vv.
    22The cardinality approximation predicate compares the returned independent
    23set with every independent set in this finite graph.
    24-/
    25
    26namespace Lax263307.IndependentBlowUp
    27
    28/-- The vertices of an independent blow-up, including possibly empty fibres. -/
    29abbrev Vertex {n : ℕ} (copies : Fin n → ℕ) := (v : Fin n) × Fin (copies v)
    30
    31/-- Copies are adjacent precisely when their original vertices are adjacent. -/
    32def graph {n : ℕ} (G : SimpleGraph (Fin n)) (copies : Fin n → ℕ) :
    33 SimpleGraph (Vertex copies) := G.comap fun v => v.1
    34
    35/-- All copies of a given original vertex set. -/
    36def lift {n : ℕ} (copies : Fin n → ℕ) (I : Finset (Fin n)) : Finset (Vertex copies) :=
    37 I.sigma fun _ => Finset.univ
    38
    39/-- Vertices represented by at least one selected copy. -/
    40def project {n : ℕ} {copies : Fin n → ℕ} (K : Finset (Vertex copies)) : Finset (Fin n) :=
    41 K.image fun v => v.1
    42
    43/-- The usual multiplicative cardinality guarantee on the blow-up graph. -/
    44def IsCardinalityApproximation {n : ℕ} (G : SimpleGraph (Fin n))
    45 (copies : Fin n → ℕ) (δ : ℚ) (K : Finset (Vertex copies)) : Prop :=
    46 (graph G copies).IsIndepSet (K : Set (Vertex copies)) ∧
    47 ∀ J : Finset (Vertex copies), (graph G copies).IsIndepSet (J : Set (Vertex copies)) →
    48 (1 - δ) * (J.card : ℚ) ≤ K.card
    49
    50end Lax263307.IndependentBlowUp
    51
    Formalization notes

    A copy is a pair (v,i)(v,i) with 0≤i<tv0\le i<t_v. This dependent pair type has exactly ∑vtv\sum_v t_v elements and admits the usual finite-type instances. The blow-up graph is the comap of GG along the projection to vv. The cardinality approximation predicate compares the returned independent set with every independent set in this finite graph.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…