graph, expander graph, cayley graph, ...

Stream: Is there code for X?

[david]

Hi, I am currently writing a paper that contains ideas including expander graph, Cayley graph, expander codes ... So I would like to use this opportunity to develop some lean code along this direction. Is there any suggested code related to graphs, such as expander graph, Cayley graph?

Also, since the proof in this context often contains 2 parts. One part on construction, the other part on proof. Is there some "template" (i.e. some other problem with similar 2 part format) I could refer to?

[Yaël Dillies]

Graph theory is at baby stage in mathlib right now. Some of us are doing stuff related to them, but no Cayley or expander graph as far as I know.
The 2 parts proofs you are talking about are ubiquitous, so I don't really know what to point you to.

[david]

Thank you! Sorry, I am a beginner, so I'm still navigating. Can you point to any example that you wrote or any example you found easy for a beginner to digest?

[Eric Wieser]

Can you expand a little on what you mean by "a two part proof", perhaps with an example?

[david]

I was originally thinking about some combinatorial construction, but while writing, I realized maybe docs#list.sorted_merge_sort would serve as an example, where part1 = construct the algorithm and part2 = proof the algorithm actually sort correctly. I will first try to understand it. Thanks!

[Kyle Miller]

@david Here's a quick attempt at formalizing the definitions of Schreier graphs and Cayley graphs:

import algebra.group
import group_theory.group_action.basic

universes u v

structure digraph (V : Type u) (E : Type v) :=
(edges : V → V → set E)

def symmetric_subset (G : Type u) [group G] (S : set G) : Prop :=
∀ g ∈ S, g⁻¹ ∈ S

def schreier_graph (G : Type u) [group G]
  (S : set G)
  (X : Type v) [mul_action G X] : digraph X G :=
{ edges := λ x y, {g : G | g ∈ S ∧ g • x = y} }

namespace schreier_graph
variables {G : Type u} [group G]
variables {S : set G}
variables {X : Type v} [mul_action G X]

lemma edge_mem (g : G) (x y : X)
  (h : g ∈ (schreier_graph G S X).edges x y) : g ∈ S :=
h.1

lemma edge_gen (g : G) (x y : X)
  (h : g ∈ (schreier_graph G S X).edges x y) : g • x = y :=
h.2

lemma edge_comm (g : G) (x y : X)
  (sym : symmetric_subset G S) :
  g ∈ (schreier_graph G S X).edges x y ↔ g⁻¹ ∈ (schreier_graph G S X).edges y x  :=
begin
  simp only [schreier_graph, set.mem_set_of_eq],
  split;
  { rintro ⟨h, rfl⟩,
    have := sym _ h,
    simpa using this },
end

end schreier_graph

def cayley_graph (G : Type u) [group G] (S : set G) : digraph G G := schreier_graph G S G

namespace cayley_graph
variables {G : Type u} [group G] {S : set G}

lemma edge_mem (v w g : G)
  (h : g ∈ (cayley_graph G S).edges v w) : g ∈ S :=
h.1

lemma mem_iff (v w g : G) :
  g ∈ (cayley_graph G S).edges v w ↔ g ∈ S ∧ g * v = w := iff.rfl

lemma apply (v g : G) (h : g ∈ S) : g ∈ (cayley_graph G S).edges v (g * v) :=
begin
  rw mem_iff,
  simp [h],
end

end cayley_graph

[Kyle Miller]

They're directed graphs (with a definition similar to docs#quiver) with edges labeled by group elements from a generating set.

[david]

@Kyle Miller Thank you that was extremely helpful!

[Kevin Buzzard]

@David your description of an argument being a construction and a proof just looks like a definition and a proof in Lean. The way to learn this software is to dive in and formalise some mathematics. See if you can prove some basic lemmas from your paper using the definitions which Kyle haa provided and feel free to ask in #new members if you have any problems

[Bhavik Mehta]

@Alena Gusakov was also interested in Cayley graphs, perhaps she has some things too?