graph products

Stream: graph theory

[Todd Hildebrant]

I am looking to begin working on defining the graph products, but am not sure about which graph to use. I apologize if I overlooked these topics when I reviewed the README and contributing guides. Would it be best to begin with a generic product, then use the edge conditions to specify which product, or create them all separately?

I am following the wikipedia page, which uses the "useful" convention from the awesome Handbook of Product Graphs:

a graph product is a binary operation on graphs. Specifically, it is an operation that takes two graphs G1 and G2 and produces a graph H with the following properties:

• The vertex set of H is the Cartesian product V(G1) × V(G2), where V(G1) and V(G2) are the vertex sets of G1 and G2, respectively.
• Two vertices (a1,a2) and (b1,b2) of H are connected by an edge iff a condition about a1, b1 in G1 and a2, b2 in G2 is fulfilled.

Thank you for the feedback.

My current draft is

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.ZMod.Basic

variable {V₁ V₂ : Type*}

def cartAdj (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) :
  (V₁ × V₂) → (V₁ × V₂) → Prop :=
    fun u v =>
      (u.1 = v.1 ∧ G₂.Adj u.2 v.2) ∨
      (G₁.Adj u.1 v.1 ∧ u.2 = v.2)

def CartProd (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) :
  SimpleGraph (V₁ × V₂) :=
    by
      refine
        { Adj := cartAdj G₁ G₂
        , symm := ?_
        , loopless := ?_ }
      · intro u v h
        cases h with
        | inl h1 =>
            left
            refine ⟨h1.1.symm, ?_⟩
            exact G₂.symm h1.2
        | inr h2 =>
            right
            refine ⟨?_, h2.2.symm⟩
            exact G₁.symm h2.1
      · intro u h
        cases h with
        | inl h1 =>
            exact (G₂.loopless u.2) h1.2
        | inr h2 =>
            exact (G₁.loopless u.1) h2.1

def Kn (n : Nat) : SimpleGraph (Fin n) :=
  SimpleGraph.fromRel (fun a b => a ≠ b)

def CycleGraph (n : Nat) : SimpleGraph (ZMod n) :=
  SimpleGraph.fromRel (fun a b => a + 1 = b ∨ b + 1 = a)

def Kmn (m n : Nat) : SimpleGraph (Sum (Fin m) (Fin n)) :=
  SimpleGraph.fromRel (fun a b =>
    match a, b with
    | Sum.inl _, Sum.inr _ => True
    | Sum.inr _, Sum.inl _ => True
    | _, _ => False)

#check CartProd (Kn 5) (Kn 4)
#check CartProd (CycleGraph 5) (CycleGraph 4)
#check CartProd (Kmn 5 4) (Kmn 4 5)
#check (CartProd (Kn 5) (Kn 4)).Adj (0, 1) (1, 0)
#check (CartProd (CycleGraph 5) (CycleGraph 4)).Adj (0, 1) (1, 0)
#check (CartProd (Kmn 5 4) (Kmn 4 5)).Adj (Sum.inl 0, Sum.inr 0) (Sum.inr 0, Sum.inl 0)

[Vlad Tsyrklevich]

Here is an example of the box product which is the same as what you're defining https://github.com/leanprover-community/mathlib4/blob/cb7ef5d643a38bf6550738a65487ed12cc10764b/Mathlib/Combinatorics/SimpleGraph/Prod.lean#L41-L46

[Todd Hildebrant]

nice, thanks @Vlad Tsyrklevich. (Somehow I missed that file :man_facepalming: ).
I'll follow that file's approach and add some more.

[Vlad Tsyrklevich]

Note also that there are also canonical spellings for the graphs you mentioned, \top : SimpleGraph (Fin n), cycleGraph n and completeBipartiteGraph (Fin m) (Fin n)

[Kevin Buzzard]

(You can use double $$ signs to write maths in LaTeX on this Zulip BTW)