Lax Lean Archive

A determined linear combination determines its constituents

Lax871432.LinearCombinationLemma · concepts/Lax871432/LinearCombinationLemma.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

    Lemma

    Let ≡\equiv be a graph isomorphism relaxation preserved under categorical products, let L\mathcal{L} be a finite family of pairwise non-isomorphic simple graphs, and let αL≠0\alpha_L \neq 0 for every L∈LL \in \mathcal{L}. If ≡\equiv determines the linear combination ∑L∈LαLhom⁡(L,−)\sum_{L \in \mathcal{L}} \alpha_L \hom(L, -) — that is, if G≡HG \equiv H implies

    ∑L∈LαLhom⁡(L,G)=∑L∈LαLhom⁡(L,H)\sum_{L \in \mathcal{L}} \alpha_L \hom(L, G) = \sum_{L \in \mathcal{L}} \alpha_L \hom(L, H)

    — then it determines each constituent hom⁡(L,−)\hom(L, -) separately.

    Concept map
    9 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 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    2import Mathlib.Data.Rat.Defs
    3import Lax871432.DistinguishingClosure
    4import Lax871432.GraphFamilies
    5import Lax871432.PreservationProperties
    6
    7/-!
    8---
    9title: A determined linear combination determines its constituents
    10type: lemma
    11---
    12Let ≡\equiv be a graph isomorphism relaxation preserved under categorical products, let
    13L\mathcal{L} be a finite family of pairwise non-isomorphic simple graphs, and let
    14αL≠0\alpha_L \neq 0 for every L∈LL \in \mathcal{L}. If ≡\equiv determines the linear combination
    15∑L∈LαLhom⁡(L,−)\sum_{L \in \mathcal{L}} \alpha_L \hom(L, -) — that is, if G≡HG \equiv H implies
    16∑L∈LαLhom⁡(L,G)=∑L∈LαLhom⁡(L,H)\sum_{L \in \mathcal{L}} \alpha_L \hom(L, G) = \sum_{L \in \mathcal{L}} \alpha_L \hom(L, H)
    17— then it determines each constituent hom⁡(L,−)\hom(L, -) separately.
    18-/
    19
    20open Lax871432.DistinguishingClosure Lax871432.GraphFamilies Lax871432.HomomorphismCounts
    21open Lax871432.IsomorphismRelaxations Lax871432.PreservationProperties
    22
    23namespace Lax871432.LinearCombinationLemma
    24
    25/-- A relaxation preserved under categorical products which determines a linear combination of
    26homomorphism counts, over pairwise non-isomorphic graphs and with nonzero coefficients,
    27determines each of its constituents. -/
    28axiom determines_of_determines_sum (R : GraphIsoRelaxation) (hprod : PreservedUnderCatProd R)
    29 {n : ℕ} {ι : Type} [Fintype ι] (L : GraphFamily n ι) (hL : L.PairwiseNonIso)
    30 (α : ι → ℚ) (hα : ∀ i, α i ≠ 0)
    31 (hdet : ∀ {V W : Type} [Finite V] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W),
    32 R.Rel G H →
    33 ∑ i, α i * (homCount (L.graph i) G : ℚ) = ∑ i, α i * (homCount (L.graph i) H : ℚ))
    34 (i : ι) : Determines R (L.graph i)
    35
    36end Lax871432.LinearCombinationLemma
    37
    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…