Graph automorphisms, vertex orbits, and local action

import Mathlib

set_option autoImplicit false

/-! Automorphisms and their vertex orbits for one literal graph. -/

namespace Conway99Formal.automorphisms

variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

/-- A permutation preserving adjacency in the given graph. -/
def IsAut (σ : Equiv.Perm V) : Prop :=
  ∀ x y, G.Adj x y ↔ G.Adj (σ x) (σ y)

/-- Automorphisms of the given graph, with multiplication inherited from permutations. -/
def autSubgroup : Subgroup (Equiv.Perm V) where
  carrier := {σ | IsAut G σ}
  mul_mem' := by
    intro a b ha hb x y
    simp only [Equiv.Perm.mul_apply]
    exact (hb x y).trans (ha (b x) (b y))
  one_mem' := by intro x y; simp [IsAut]
  inv_mem' := by
    intro a ha x y
    have h := ha (a⁻¹ x) (a⁻¹ y)
    simpa using h.symm



/-- The actual fixed vertices of a permutation of this graph's vertex type. -/
def fixedSet (σ : Equiv.Perm V) : Finset V :=
  Finset.univ.filter fun x => σ x = x









/-- An automorphism fixing a vertex preserves its actual neighbor set. -/
theorem neighbor_mem_iff_apply (σ : Equiv.Perm V) (hσ : IsAut G σ)
    (x : V) (hx : σ x = x) (y : V) :
    y ∈ G.neighborFinset x ↔ σ y ∈ G.neighborFinset x := by
  simpa only [SimpleGraph.mem_neighborFinset, hx] using hσ x y









/-- The permutation induced on the neighbors of a fixed vertex. -/
def neighborPerm (σ : Equiv.Perm V) (hσ : IsAut G σ)
    (x : V) (hx : σ x = x) : Equiv.Perm (G.neighborFinset x) :=
  σ.subtypePerm (fun y => (neighbor_mem_iff_apply G σ hσ x hx y).symm)

















/-- Two vertices are equivalent under the automorphism group of this graph. -/
def SameOrbit (x y : V) : Prop :=
  ∃ σ : Equiv.Perm V, IsAut G σ ∧ σ x = y









/-- Predicate that the full automorphism group acts transitively on vertices. -/
def VertexTransitive : Prop := ∀ x y : V, SameOrbit G x y

/-- Data that the full automorphism group has exactly two vertex orbits. -/
structure TwoOrbitSplit where
  O : Finset V
  nonempty : O.Nonempty
  proper : ∃ x, x ∉ O
  inside : ∀ x ∈ O, ∀ y ∈ O, SameOrbit G x y
  outside : ∀ x, x ∉ O → ∀ y, y ∉ O → SameOrbit G x y
  separated : ∀ x ∈ O, ∀ y, y ∉ O → ¬ SameOrbit G x y















/-- A triangle is an actual three-point clique in the supplied graph. -/
def IsTriangle (T : Finset V) : Prop :=
  T.card = 3 ∧ ∀ x ∈ T, ∀ y ∈ T, x ≠ y → G.Adj x y






end Conway99Formal.automorphisms