Lax Lean Archive

Products of graphs

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

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

    Two products of simple graphs, both on the product V(G)×V(H)V(G) \times V(H) of the vertex sets.

    In the categorical product G×HG \times H, the pairs ghgh and g′h′g'h' are adjacent when gg′∈E(G)gg' \in E(G) and hh′∈E(H)hh' \in E(H). It is the product in the category of graphs and graph homomorphisms, whence hom⁡(F,G×H)=hom⁡(F,G)hom⁡(F,H)\hom(F, G \times H) = \hom(F, G)\hom(F, H); it also goes by tensor, Kronecker, weak or conjunction product.

    In the lexicographic product G⋅HG \cdot H, the pairs ghgh and g′h′g'h' are adjacent when gg′∈E(G)gg' \in E(G), or else g=g′g = g' and hh′∈E(H)hh' \in E(H).

    Concept map
    1 concept; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Prod
    2
    3/-!
    4---
    5title: Products of graphs
    6type: definition
    7---
    8Two products of simple graphs, both on the product V(G)×V(H)V(G) \times V(H) of the vertex sets.
    9
    10In the *categorical product* G×HG \times H, the pairs ghgh and g′h′g'h' are adjacent when
    11gg′∈E(G)gg' \in E(G) **and** hh′∈E(H)hh' \in E(H). It is the product in the category of graphs and graph
    12homomorphisms, whence hom⁡(F,G×H)=hom⁡(F,G)hom⁡(F,H)\hom(F, G \times H) = \hom(F, G)\hom(F, H); it also goes by tensor,
    13Kronecker, weak or conjunction product.
    14
    15In the *lexicographic product* G⋅HG \cdot H, the pairs ghgh and g′h′g'h' are adjacent when
    16gg′∈E(G)gg' \in E(G), or else g=g′g = g' and hh′∈E(H)hh' \in E(H).
    17-/
    18
    19namespace Lax871432.GraphProducts
    20
    21variable {α β : Type*}
    22
    23/-- The *categorical product* of simple graphs: it relates `(a₁, b₁)` and `(a₂, b₂)` when `G`
    24relates `a₁` and `a₂` and `H` relates `b₁` and `b₂`. Contrast with `SimpleGraph.boxProd`. -/
    25def catProd (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α × β) where
    26 Adj x y := G.Adj x.1 y.1 ∧ H.Adj x.2 y.2
    27 symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.symm⟩⟩
    28 loopless := ⟨fun _ h => G.irrefl h.1⟩
    29
    30@[inherit_doc]
    31scoped infixl:70 " ×g " => catProd
    32
    33/-- The *lexicographic product* of simple graphs: it relates `(a₁, b₁)` and `(a₂, b₂)` when `G`
    34relates `a₁` and `a₂`, or when `a₁ = a₂` and `H` relates `b₁` and `b₂`. -/
    35def lexProd (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α × β) where
    36 Adj x y := G.Adj x.1 y.1 ∨ (x.1 = y.1 ∧ H.Adj x.2 y.2)
    37 symm := ⟨fun _ _ h => h.imp SimpleGraph.Adj.symm fun h' => ⟨h'.1.symm, h'.2.symm⟩⟩
    38 loopless := ⟨fun _ h => h.elim (G.irrefl ·) fun h' => H.irrefl h'.2⟩
    39
    40end Lax871432.GraphProducts
    41
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…