Definition of Cayley graphs

This file defines and proves several fact about Cayley graphs. A Cayley graph over type M with generators s : Set M is a graph in which two vertices u ≠ v are adjacent if and only if there is some g ∈ s such that u * g = v or v * g = u. The elements of s are called generators.

Main declarations

• SimpleGraph.mulCayley s: the Cayley graph over M induced by [Mul M] with generators s.
• SimpleGraph.addCayley s: the Cayley graph over M induced by [Add M] with generators s.

TODOS

• Add API describing behaviour w/r/t MulOpposite.
• Add lemma showing this graph is the same as SimpleGraph.circulantGraph in appropriate settings.

def SimpleGraph.mulCayley {M : Type u_1} (s : Set M) [Mul M] : SimpleGraph M

The Cayley graph induced by an operation [Mul M] with generators s

Equations

• SimpleGraph.mulCayley s = SimpleGraph.fromRel fun (x1 x2 : M) => ∃ g ∈ s, x1 * g = x2

def SimpleGraph.addCayley {M : Type u_1} (s : Set M) [Add M] : SimpleGraph M

The Cayley graph induced by an operation [Add M] with generators s

Equations

• SimpleGraph.addCayley s = SimpleGraph.fromRel fun (x1 x2 : M) => ∃ g ∈ s, x1 + g = x2

theorem SimpleGraph.mulCayley_adj' {M : Type u_1} (s : Set M) [Mul M] (u v : M) : (mulCayley s).Adj u v ↔ u ≠ v ∧ ∃ g ∈ s, u * g = v ∨ u = v * g

See mulCayley_adj for the more convenient form in a Group.

theorem SimpleGraph.addCayley_adj' {M : Type u_1} (s : Set M) [Add M] (u v : M) : (addCayley s).Adj u v ↔ u ≠ v ∧ ∃ g ∈ s, u + g = v ∨ u = v + g

See addCayley_adj for the more convenient form in an AddGroup.

theorem SimpleGraph.mulCayley_le_iff {M : Type u_1} (s : Set M) [Mul M] (G : SimpleGraph M) : mulCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a

theorem SimpleGraph.addCayley_le_iff {M : Type u_1} (s : Set M) [Add M] (G : SimpleGraph M) : addCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a + g ≠ a → G.Adj (a + g) a

@[implicit_reducible]

instance SimpleGraph.instDecidableRelAdjMulCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet {M : Type u_1} (s : Set M) [Mul M] [Fintype M] [DecidableEq M] [DecidablePred fun (x : M) => x ∈ s] : DecidableRel (mulCayley s).Adj

Equations

• SimpleGraph.instDecidableRelAdjMulCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet s u v = decidable_of_iff (u ≠ v ∧ ∃ g ∈ s, u * g = v ∨ u = v * g) ⋯

@[implicit_reducible]

instance SimpleGraph.instDecidableRelAdjAddCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet {M : Type u_1} (s : Set M) [Add M] [Fintype M] [DecidableEq M] [DecidablePred fun (x : M) => x ∈ s] : DecidableRel (addCayley s).Adj

Equations

• SimpleGraph.instDecidableRelAdjAddCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet s u v = decidable_of_iff (u ≠ v ∧ ∃ g ∈ s, u + g = v ∨ u = v + g) ⋯

theorem SimpleGraph.mulCayley_gc (M : Type u_1) [Mul M] : GaloisConnection (fun (x : Set M) => mulCayley x) fun (x : SimpleGraph M) => {g : M | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a}

mulCayley is a left (order-)adjoint.

theorem SimpleGraph.addCayley_gc (M : Type u_1) [Add M] : GaloisConnection (fun (x : Set M) => addCayley x) fun (x : SimpleGraph M) => {g : M | ∀ (a : M), a + g ≠ a → x.Adj (a + g) a}

theorem SimpleGraph.mulCayley_monotone {M : Type u_1} [Mul M] : Monotone fun (x : Set M) => mulCayley x

theorem SimpleGraph.addCayley_monotone {M : Type u_1} [Add M] : Monotone fun (x : Set M) => addCayley x

theorem SimpleGraph.mulCayley_mono {M : Type u_1} [Mul M] {U V : Set M} (hUV : U ⊆ V) : mulCayley U ≤ mulCayley V

theorem SimpleGraph.addCayley_mono {M : Type u_1} [Add M] {U V : Set M} (hUV : U ⊆ V) : addCayley U ≤ addCayley V

@[simp]

theorem SimpleGraph.mulCayley_empty {M : Type u_1} [Mul M] : mulCayley ∅ = ⊥

@[simp]

theorem SimpleGraph.addCayley_empty {M : Type u_1} [Add M] : addCayley ∅ = ⊥

@[simp]

theorem SimpleGraph.mulCayley_union {M : Type u_1} [Mul M] (s₁ s₂ : Set M) : mulCayley (s₁ ∪ s₂) = mulCayley s₁ ⊔ mulCayley s₂

@[simp]

theorem SimpleGraph.addCayley_union {M : Type u_1} [Add M] (s₁ s₂ : Set M) : addCayley (s₁ ∪ s₂) = addCayley s₁ ⊔ addCayley s₂

@[simp]

theorem SimpleGraph.mulCayley_adj_mul_iff_right {M : Type u_1} [Semigroup M] [IsLeftCancelMul M] {s : Set M} {u v d : M} : (mulCayley s).Adj (d * u) (d * v) ↔ (mulCayley s).Adj u v

@[simp]

theorem SimpleGraph.addCayley_adj_add_iff_right {M : Type u_1} [AddSemigroup M] [IsLeftCancelAdd M] {s : Set M} {u v d : M} : (addCayley s).Adj (d + u) (d + v) ↔ (addCayley s).Adj u v

@[simp]

theorem SimpleGraph.mulCayley_erase_one {M : Type u_1} (s : Set M) [MulOneClass M] : mulCayley (s \ {1}) = mulCayley s

@[simp]

theorem SimpleGraph.addCayley_erase_zero {M : Type u_1} (s : Set M) [AddZeroClass M] : addCayley (s \ {0}) = addCayley s

@[simp]

theorem SimpleGraph.mulCayley_insert_one {M : Type u_1} (s : Set M) [MulOneClass M] : mulCayley (insert 1 s) = mulCayley s

@[simp]

theorem SimpleGraph.addCayley_insert_zero {M : Type u_1} (s : Set M) [AddZeroClass M] : addCayley (insert 0 s) = addCayley s

@[simp]

theorem SimpleGraph.mulCayley_singleton_one {M : Type u_1} [MulOneClass M] : mulCayley {1} = ⊥

@[simp]

theorem SimpleGraph.addCayley_singleton_zero {M : Type u_1} [AddZeroClass M] : addCayley {0} = ⊥

theorem SimpleGraph.mulCayley_adj {M : Type u_1} (s : Set M) [Group M] (u v : M) : (mulCayley s).Adj u v ↔ u ≠ v ∧ (u⁻¹ * v ∈ s ∨ v⁻¹ * u ∈ s)

theorem SimpleGraph.addCayley_adj {M : Type u_1} (s : Set M) [AddGroup M] (u v : M) : (addCayley s).Adj u v ↔ u ≠ v ∧ (-u + v ∈ s ∨ -v + u ∈ s)

@[simp]

theorem SimpleGraph.mulCayley_inv {M : Type u_1} (s : Set M) [Group M] : mulCayley s⁻¹ = mulCayley s

@[simp]

theorem SimpleGraph.addCayley_neg {M : Type u_1} (s : Set M) [AddGroup M] : addCayley (-s) = addCayley s

@[implicit_reducible]

instance SimpleGraph.instDecidableRelAdjMulCayleyOfDecidableEqOfDecidablePredMemSet {M : Type u_1} (s : Set M) [Group M] [DecidableEq M] [DecidablePred fun (x : M) => x ∈ s] : DecidableRel (mulCayley s).Adj

Equations

• SimpleGraph.instDecidableRelAdjMulCayleyOfDecidableEqOfDecidablePredMemSet s u v = decidable_of_iff (u ≠ v ∧ (u⁻¹ * v ∈ s ∨ v⁻¹ * u ∈ s)) ⋯

@[implicit_reducible]

instance SimpleGraph.instDecidableRelAdjAddCayleyOfDecidableEqOfDecidablePredMemSet {M : Type u_1} (s : Set M) [AddGroup M] [DecidableEq M] [DecidablePred fun (x : M) => x ∈ s] : DecidableRel (addCayley s).Adj

Equations

• SimpleGraph.instDecidableRelAdjAddCayleyOfDecidableEqOfDecidablePredMemSet s u v = decidable_of_iff (u ≠ v ∧ (-u + v ∈ s ∨ -v + u ∈ s)) ⋯

@[simp]

theorem SimpleGraph.mulCayley_univ {M : Type u_1} [Group M] : mulCayley Set.univ = ⊤

@[simp]

theorem SimpleGraph.addCayley_univ {M : Type u_1} [AddGroup M] : addCayley Set.univ = ⊤

@[simp]

theorem SimpleGraph.mulCayley_compl_singleton_one {M : Type u_1} [Group M] : mulCayley {1}ᶜ = ⊤

@[simp]

theorem SimpleGraph.addCayley_compl_singleton_zero {M : Type u_1} [AddGroup M] : addCayley {0}ᶜ = ⊤