Lax Lean Archive

Homomorphism counts into a complement

Lax871432.ComplementCounts · concepts/Lax871432/ComplementCounts.lean · lax-871432

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

    For finite simple graphs FF and GG,

    hom⁡(F,G‾)=∑S⊆E(F)(−1)∣S∣∑L⊆Shom⁡(FS⊘L,G),\hom(F, \overline{G}) = \sum_{S \subseteq E(F)} (-1)^{|S|} \sum_{L \subseteq S} \hom(F_S \oslash L, G),

    where FSF_S is the spanning subgraph of FF with edge set SS and FS⊘LF_S \oslash L is the contraction quotient of FSF_S by LL: the graph obtained from FSF_S by contracting the edges in LL when it is loopless, and a graph with loops otherwise.

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 8 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Ring.Finset
    2import Lax871432.HomomorphismCounts
    3import Lax871432.LoopGraphs
    4
    5/-!
    6---
    7title: Homomorphism counts into a complement
    8type: theorem
    9---
    10For finite simple graphs FF and GG,
    11hom⁡(F,G‾)=∑S⊆E(F)(−1)∣S∣∑L⊆Shom⁡(FS⊘L,G),\hom(F, \overline{G}) = \sum_{S \subseteq E(F)} (-1)^{|S|} \sum_{L \subseteq S} \hom(F_S \oslash L, G),
    12
    13where FSF_S is the spanning subgraph of FF with edge set SS and FS⊘LF_S \oslash L is the
    14contraction quotient of FSF_S by LL: the graph obtained from FSF_S by contracting the edges
    15in LL when it is loopless, and a graph with loops otherwise.
    16
    17-/
    18
    19open Lax871432.HomomorphismCounts Lax871432.LoopGraphs
    20
    21open scoped Lax871432.LoopGraphs
    22
    23namespace Lax871432.ComplementCounts
    24
    25/-- **Homomorphisms into a complement**: the number of homomorphisms from `F` to `Gᶜ` is a
    26signed sum of the numbers of homomorphisms into `G` from the graphs obtained from `F` by
    27deleting the edges outside a set `S` and contracting those in a subset `L` of `S` — all of
    28them minors of `F`. -/
    29axiom homCount_compl {V W : Type*} [Finite V] [Finite W] (F : SimpleGraph V)
    30 (G : SimpleGraph W) :
    31 letI : Fintype F.edgeSet := Fintype.ofFinite _
    32 (homCount F Gᶜ : ℤ) =
    33 ∑ s : Finset F.edgeSet, (-1 : ℤ) ^ s.card *
    34 ∑ L ∈ s.powerset,
    35 (LoopGraph.homCount
    36 (((spanningSubgraph F) ((edgeSetOf F) s)) ⊘ (edgeSetOf F) L) (toLoopGraph G) : ℤ)
    37
    38end Lax871432.ComplementCounts
    39
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…