Definition of Graph Action

In this file we define group actions on simple graphs.

Let G be a group and X be a simple graph. Then an action of G on X is defined as an action on the vertices of X that preserves the adjacency relation.

We show that a graph action induces an action on the edges.

class GraphAction {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] (X : SimpleGraph V) : Prop

A group G acts as a graph action on X, if the adjacency relation is preserved.

• smul_adj_smul (g : G) (x y : V) (h : X.Adj x y) : X.Adj (g • x) (g • y)

@[simp]

theorem GraphAction.adj_iff {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] (X : SimpleGraph V) [GraphAction G X] (g : G) (x y : V) : X.Adj (g • x) (g • y) ↔ X.Adj x y

@[implicit_reducible]

instance GraphAction.instSMulSym2 {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] : SMul G (Sym2 V)

Equations

• GraphAction.instSMulSym2 G = { smul := fun (g : G) => Sym2.map fun (x : V) => g • x }

@[simp]

theorem GraphAction.smul_sym2 {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] (g : G) (x y : V) : g • s(x, y) = s(g • x, g • y)

@[implicit_reducible]

instance GraphAction.instMulActionSym2 {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] : MulAction G (Sym2 V)

Equations

• GraphAction.instMulActionSym2 G = { toSMul := GraphAction.instSMulSym2 G, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance GraphAction.instSMulElemSym2EdgeSet {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] (X : SimpleGraph V) [GraphAction G X] : SMul G ↑X.edgeSet

Equations

• GraphAction.instSMulElemSym2EdgeSet G X = { smul := fun (g : G) (e : ↑X.edgeSet) => ⟨g • ↑e, ⋯⟩ }

@[simp]

theorem GraphAction.smul_edgeSet_coe {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] (X : SimpleGraph V) [GraphAction G X] (g : G) (e : ↑X.edgeSet) : ↑(g • e) = g • ↑e

@[implicit_reducible]

instance GraphAction.instMulActionElemSym2EdgeSet {V : Type u_1} (G : Type u_2) [Group G] [MulAction G V] (X : SimpleGraph V) [GraphAction G X] : MulAction G ↑X.edgeSet

The action on edges induced by a graph action.

Equations

• GraphAction.instMulActionElemSym2EdgeSet G X = { toSMul := GraphAction.instSMulElemSym2EdgeSet G X, mul_smul := ⋯, one_smul := ⋯ }

theorem GraphAction.smul_mem_smul_of {V : Type u_1} {G : Type u_2} [Group G] [MulAction G V] (g : G) (e : Sym2 V) (x : V) (h : x ∈ e) : g • x ∈ g • e

@[simp]

theorem GraphAction.smul_mem_smul_iff {V : Type u_1} {G : Type u_2} [Group G] [MulAction G V] (g : G) (e : Sym2 V) (x : V) : g • x ∈ g • e ↔ x ∈ e

instance GraphAction.instIsPretransitiveElemSym2EdgeSet {V : Type u_1} {G : Type u_2} [Group G] [MulAction G V] {X : SimpleGraph V} [GraphAction G X] [MulAction.IsPretransitive G (Sym2 V)] : MulAction.IsPretransitive G ↑X.edgeSet