feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs

Mathlib.lean

@@ -3285,6 +3285,7 @@ public import Mathlib.Combinatorics.Derangements.Basic
 public import Mathlib.Combinatorics.Derangements.Exponential
 public import Mathlib.Combinatorics.Derangements.Finite
 public import Mathlib.Combinatorics.Digraph.Basic
+public import Mathlib.Combinatorics.Digraph.HasAdj
 public import Mathlib.Combinatorics.Digraph.Orientation
 public import Mathlib.Combinatorics.Enumerative.Bell
 public import Mathlib.Combinatorics.Enumerative.Catalan
@@ -3304,6 +3305,7 @@ public import Mathlib.Combinatorics.Graph.Basic
 public import Mathlib.Combinatorics.HalesJewett
 public import Mathlib.Combinatorics.Hall.Basic
 public import Mathlib.Combinatorics.Hall.Finite
+public import Mathlib.Combinatorics.HasAdj.Basic
 public import Mathlib.Combinatorics.Hindman
 public import Mathlib.Combinatorics.KatonaCircle
 public import Mathlib.Combinatorics.Matroid.Basic
@@ -3386,6 +3388,7 @@ public import Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
 public import Mathlib.Combinatorics.SimpleGraph.Girth
 public import Mathlib.Combinatorics.SimpleGraph.Hall
 public import Mathlib.Combinatorics.SimpleGraph.Hamiltonian
+public import Mathlib.Combinatorics.SimpleGraph.HasAdj
 public import Mathlib.Combinatorics.SimpleGraph.Hasse
 public import Mathlib.Combinatorics.SimpleGraph.IncMatrix
 public import Mathlib.Combinatorics.SimpleGraph.Init

Mathlib/Combinatorics/Digraph/HasAdj.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Iván Renison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Iván Renison
+-/
+module
+
+public import Mathlib.Combinatorics.HasAdj.Basic
+public import Mathlib.Combinatorics.Digraph.Basic
+
+/-!
+In this file we make `Digraph` an instance of `HasAdj`.
+-/
+
+@[expose] public section
+
+variable {α : Type*}
+
+instance : HasAdj α (Digraph α) where
+  verts _ := Set.univ
+  Adj G := G.Adj
+  left_mem_verts_of_adj _ := Set.mem_univ _
+  right_mem_verts_of_adj _ := Set.mem_univ _

Mathlib/Combinatorics/HasAdj/Basic.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Iván Renison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Iván Renison
+-/
+module
+
+public import Batteries.Data.List.Basic
+public import Mathlib.Data.Rel
+
+/-!
+# Typeclass for different kinds of (simple) graphs
+
+This module defines the typeclass `HasAdj` for capturing the common structure of different kinds of
+(simple) graphs.
+
+## Main definitions
+
+* `HasAdj`: is the main typeclass in question. The field `verts` gives the set of vertices of a
+  graph, and the field `Adj` gives the adjacency relation between vertices.
+
+## TODO
+* Migrate from `SimpleGraph` all the results that only depend on the adjacency relation.
+
+-/
+
+@[expose] public section
+
+/-- Typeclass for (simple) graphs. -/
+class HasAdj (α : outParam Type*) (Gr : Type*) where
+  /-- The set of vertices of the graph. -/
+  verts (G : Gr) : Set α
+  /-- The adjacency relation of the graph. -/
+  Adj (G : Gr) : α → α → Prop
+  /-- There is no edge of the graph outside of it vertices. -/
+  left_mem_verts_of_adj {G : Gr} {v w : α} (h : Adj G v w) : v ∈ verts G
+  /-- There is no edge of the graph outside of it vertices. -/
+  right_mem_verts_of_adj {G : Gr} {v w : α} (h : Adj G v w) : w ∈ verts G
+
+namespace HasAdj
+
+variable {Gr : Type*} {α : Type*} [HasAdj α Gr]
+
+/-- Dot notation for `left_mem_verts_of_adj`. -/
+lemma Adj.left_mem_verts {G : Gr} {v w : α} (h : Adj G v w) : v ∈ verts G :=
+  left_mem_verts_of_adj h
+
+/-- Dot notation for `right_mem_verts_of_adj`. -/
+lemma Adj.right_mem_verts {G : Gr} {v w : α} (h : Adj G v w) : w ∈ verts G :=
+  right_mem_verts_of_adj h
+
+end HasAdj

Mathlib/Combinatorics/SimpleGraph/HasAdj.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Iván Renison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Iván Renison
+-/
+module
+
+public import Mathlib.Combinatorics.HasAdj.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Basic
+
+/-!
+In this file we make `SimpleGraph` an instance of `HasAdj`.
+-/
+
+@[expose] public section
+
+variable {α : Type*}
+
+instance : HasAdj α (SimpleGraph α) where
+  verts _ := Set.univ
+  Adj G := G.Adj
+  left_mem_verts_of_adj _ := Set.mem_univ _
+  right_mem_verts_of_adj _ := Set.mem_univ _