feat(Combinatorics/SimpleGraph): define completeEquipartiteGraph (leanprover-community#27597)

Define the complete equipartite graph in `r` parts each of *equal* size `t` such that two vertices are adjacent if and only if they are in different parts.

These graphs are typically denoted by $$K_r(t)$$.

Author: mitchell-horner

Mathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -121,6 +121,10 @@ noncomputable instance [Fintype V] [Fintype α] : Fintype (Coloring G α) := by
   change Fintype (RelHom G.Adj (completeGraph α).Adj)
   apply Fintype.ofInjective _ RelHom.coe_fn_injective
 
+instance [DecidableEq α] {c : α} :
+    DecidablePred (· ∈ C.colorClass c) :=
+  inferInstanceAs <| DecidablePred (· ∈ { v | C v = c })
+
 variable (G)
 
 /-- Whether a graph can be colored by at most `n` colors. -/

Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: John Talbot, Lian Bremner Tattersall
 -/
 import Mathlib.Combinatorics.SimpleGraph.Coloring
+import Mathlib.Combinatorics.SimpleGraph.Copy
+import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 import Mathlib.Combinatorics.SimpleGraph.Hasse
+import Mathlib.Combinatorics.SimpleGraph.Turan
 
 /-!
 # Complete Multipartite Graphs
@@ -27,15 +30,37 @@ A graph is complete multipartite iff non-adjacency is transitive.
 * See also: `Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean`
   `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree` a maximally `r + 1`- cliquefree graph
   is `r`-colorable iff it is complete-multipartite.
+
+* `SimpleGraph.completeEquipartiteGraph`: the **complete equipartite graph** in parts of *equal*
+  size such that two vertices are adjacent if and only if they are in different parts.
+
+## Implementation Notes
+
+The definition of `completeEquipartiteGraph` is similar to `completeMultipartiteGraph`
+except that `Sigma.fst` is replaced by `Prod.fst` in the definition. The difference is that the
+former vertices are a product type whereas the latter vertices are a *dependent* product type.
+
+While `completeEquipartiteGraph r t` could have been defined as the specialisation
+`completeMultipartiteGraph (const (Fin r) (Fin t))` (or `turanGraph (r * t) r`), it is convenient
+to instead have a *non-dependent* *product* type for the vertices.
+
+See `completeEquipartiteGraph.completeMultipartiteGraph`, `completeEquipartiteGraph.turanGraph`
+for the isomorphisms between a `completeEquipartiteGraph` and a corresponding
+`completeMultipartiteGraph`, `turanGraph`.
 -/
 
+open Finset Fintype
+
 universe u
 namespace SimpleGraph
 variable {α : Type u}
 
 /-- `G` is `IsCompleteMultipartite` iff non-adjacency is transitive -/
 def IsCompleteMultipartite (G : SimpleGraph α) : Prop := Transitive (¬ G.Adj · ·)
 
+theorem bot_isCompleteMultipartite : (⊥ : SimpleGraph α).IsCompleteMultipartite := by
+  simp [IsCompleteMultipartite, Transitive]
+
 variable {G : SimpleGraph α}
 /-- The setoid given by non-adjacency -/
 def IsCompleteMultipartite.setoid (h : G.IsCompleteMultipartite) : Setoid α :=
@@ -162,4 +187,136 @@ theorem IsCompleteMultipartite.comap {β : Type*} {H : SimpleGraph β} (f : H 
   exact not_isCompleteMultipartite_of_pathGraph3ComplEmbedding
           <| f.comp (pathGraph3ComplEmbeddingOf h)
 
+section CompleteEquipartiteGraph
+
+variable {r t : ℕ}
+
+/-- The **complete equipartite graph** in `r` parts each of *equal* size `t` such that two
+vertices are adjacent if and only if they are in different parts, often denoted $K_r(t)$.
+
+This is isomorphic to a corresponding `completeMultipartiteGraph` and `turanGraph`. The difference
+is that the former vertices are a product type.
+
+See `completeEquipartiteGraph.completeMultipartiteGraph`, `completeEquipartiteGraph.turanGraph`. -/
+abbrev completeEquipartiteGraph (r t : ℕ) : SimpleGraph (Fin r × Fin t) :=
+  SimpleGraph.comap Prod.fst ⊤
+
+lemma completeEquipartiteGraph_adj {v w} :
+  (completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1 := by rfl
+
+/-- A `completeEquipartiteGraph` is isomorphic to a corresponding `completeMultipartiteGraph`.
+
+The difference is that the former vertices are a product type whereas the latter vertices are a
+*dependent* product type. -/
+def completeEquipartiteGraph.completeMultipartiteGraph :
+    completeEquipartiteGraph r t ≃g completeMultipartiteGraph (Function.const (Fin r) (Fin t)) :=
+  { (Equiv.sigmaEquivProd (Fin r) (Fin t)).symm with map_rel_iff' := by simp }
+
+/-- A `completeEquipartiteGraph` is isomorphic to a corresponding `turanGraph`.
+
+The difference is that the former vertices are a product type whereas the latter vertices are
+not. -/
+def completeEquipartiteGraph.turanGraph :
+    completeEquipartiteGraph r t ≃g turanGraph (r * t) r where
+  toFun := by
+    refine fun v ↦ ⟨v.2 * r + v.1, ?_⟩
+    conv_rhs =>
+      rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]
+    exact add_lt_add_of_le_of_lt (Nat.mul_le_mul_right r (Nat.le_pred_of_lt v.2.prop)) v.1.prop
+  invFun := by
+    refine fun v ↦ (⟨v % r, ?_⟩, ⟨v / r, ?_⟩)
+    · have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
+      exact Nat.mod_lt v hr
+    · exact Nat.div_lt_of_lt_mul v.prop
+  left_inv v := by
+    refine Prod.ext (Fin.ext ?_) (Fin.ext ?_)
+    · conv =>
+        enter [1, 1, 1, 1, 1]
+        rw [Nat.mul_add_mod_self_right]
+      exact Nat.mod_eq_of_lt v.1.prop
+    · apply le_antisymm
+      · rw [Nat.div_le_iff_le_mul_add_pred v.1.pos, mul_comm r ↑v.2]
+        exact Nat.add_le_add_left (Nat.le_pred_of_lt v.1.prop) (↑v.2 * r)
+      · rw [Nat.le_div_iff_mul_le v.1.pos]
+        exact Nat.le_add_right (↑v.2 * r) ↑v.1
+  right_inv v := Fin.ext (Nat.div_add_mod' v r)
+  map_rel_iff' {v w} := by
+    rw [turanGraph_adj, Equiv.coe_fn_mk, Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt v.1.prop,
+      Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt w.1.prop, ← Fin.ext_iff.ne,
+      ← completeEquipartiteGraph_adj]
+
+/-- `completeEquipartiteGraph r t` contains no edges when `r ≤ 1` or `t = 0`. -/
+lemma completeEquipartiteGraph_eq_bot_iff :
+    completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0 := by
+  rw [← not_iff_not, not_or, ← ne_eq, ← edgeSet_nonempty, not_le, ← Nat.succ_le_iff,
+    ← Fin.nontrivial_iff_two_le, ← ne_eq, ← Nat.pos_iff_ne_zero, Fin.pos_iff_nonempty]
+  refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩
+  · induction' e with v₁ v₂
+    rw [mem_edgeSet, completeEquipartiteGraph_adj] at he
+    exact ⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩
+  · use s((i₁, x), (i₂, x))
+    rw [mem_edgeSet, completeEquipartiteGraph_adj]
+    exact hv
+
+theorem completeEquipartiteGraph.isCompleteMultipartite :
+    (completeEquipartiteGraph r t).IsCompleteMultipartite := by
+  rcases t.eq_zero_or_pos with ht_eq0 | ht_pos
+  · rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]
+    exact bot_isCompleteMultipartite
+  · rw [isCompleteMultipartite_iff]
+    use (Fin r), Function.const (Fin r) (Fin t)
+    simp_rw [Function.const_apply, exists_prop]
+    exact ⟨Function.const (Fin r) (Fin.pos_iff_nonempty.mp ht_pos),
+      ⟨completeEquipartiteGraph.completeMultipartiteGraph⟩⟩
+
+theorem neighborSet_completeEquipartiteGraph (v) :
+    (completeEquipartiteGraph r t).neighborSet v = {v.1}ᶜ ×ˢ Set.univ := by
+  ext; simp [ne_comm]
+
+theorem neighborFinset_completeEquipartiteGraph (v) :
+    (completeEquipartiteGraph r t).neighborFinset v = {v.1}ᶜ ×ˢ univ := by
+  ext; simp [ne_comm]
+
+theorem degree_completeEquipartiteGraph (v) :
+    (completeEquipartiteGraph r t).degree v = (r - 1) * t := by
+  rw [← card_neighborFinset_eq_degree, neighborFinset_completeEquipartiteGraph v,
+    card_product, card_compl, card_singleton, Fintype.card_fin, card_univ, Fintype.card_fin]
+
+theorem card_edgeFinset_completeEquipartiteGraph :
+    #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * t ^ 2 := by
+  rw [← mul_right_inj' two_ne_zero, ← sum_degrees_eq_twice_card_edges]
+  conv_lhs =>
+    rhs; intro v
+    rw [degree_completeEquipartiteGraph v]
+  rw [sum_const, smul_eq_mul, card_univ, card_prod, Fintype.card_fin, Fintype.card_fin]
+  conv_rhs =>
+    rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]
+  rw [← mul_assoc, mul_comm r _, mul_assoc t _ _, mul_comm t, mul_assoc _ t, ← pow_two]
+
+variable [Fintype α]
+
+/-- Every `n`-colorable graph is contained in a `completeEquipartiteGraph` in `n` parts (as long
+  as the parts are at least as large as the largest color class). -/
+theorem isContained_completeEquipartiteGraph_of_colorable {n : ℕ} (C : G.Coloring (Fin n))
+    (t : ℕ) (h : ∀ c, card (C.colorClass c) ≤ t) : G ⊑ completeEquipartiteGraph n t := by
+  have (c : Fin n) : Nonempty (C.colorClass c ↪ Fin t) := by
+    rw [Function.Embedding.nonempty_iff_card_le, Fintype.card_fin]
+    exact h c
+  have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)
+  have hF {c₁ c₂ v₁ v₂} (hc : c₁ = c₂) (hv : F c₁ v₁ = F c₂ v₂) : v₁.val = v₂.val := by
+    let v₁' : C.colorClass c₂ := ⟨v₁, by simp [← hc]⟩
+    have hv' : F c₁ v₁ = F c₂ v₁' := by
+      apply congr_heq
+      · rw [hc]
+      · rw [Subtype.heq_iff_coe_eq]
+        simp [hc]
+    rw [hv'] at hv
+    simpa [Subtype.ext_iff] using (F c₂).injective hv
+  use ⟨fun v ↦ (C v, F (C v) ⟨v, C.mem_colorClass v⟩), C.valid⟩
+  intro v w h
+  rw [Prod.mk.injEq] at h
+  exact hF h.1 h.2
+
+end CompleteEquipartiteGraph
+
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean

@@ -5,6 +5,7 @@ Authors: Iván Renison
 -/
 import Mathlib.Combinatorics.SimpleGraph.Circulant
 import Mathlib.Combinatorics.SimpleGraph.Coloring
+import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
 import Mathlib.Combinatorics.SimpleGraph.Hasse
 import Mathlib.Data.Fin.Parity
 
@@ -156,6 +157,20 @@ theorem chromaticNumber_cycleGraph_of_odd (n : ℕ) (h : 2 ≤ n) (hOdd : Odd n)
     rw [← hn3]
     exact Walk.three_le_chromaticNumber_of_odd_loop w hOdd'
 
+section CompleteEquipartiteGraph
+
+variable {r t : ℕ}
+
+/-- The injection `(x₁, x₂) ↦ x₁` is always a `r`-coloring of a `completeEquipartiteGraph r ·`. -/
+def Coloring.completeEquipartiteGraph :
+  (completeEquipartiteGraph r t).Coloring (Fin r) := ⟨Prod.fst, id⟩
+
+/-- The `completeEquipartiteGraph r t` is always `r`-colorable. -/
+theorem completeEquipartiteGraph_colorable :
+  (completeEquipartiteGraph r t).Colorable r := ⟨Coloring.completeEquipartiteGraph⟩
+
+end CompleteEquipartiteGraph
+
 open Walk
 lemma two_colorable_iff_forall_loop_even {α : Type*} {G : SimpleGraph α} :
     G.Colorable 2 ↔ ∀ u, ∀ (w : G.Walk u u), Even w.length := by

Mathlib/Combinatorics/SimpleGraph/Turan.lean

@@ -63,6 +63,9 @@ lemma IsTuranMaximal.le_iff_eq (hG : G.IsTuranMaximal r) (hH : H.CliqueFree (r +
 /-- The canonical `r + 1`-cliquefree Turán graph on `n` vertices. -/
 def turanGraph (n r : ℕ) : SimpleGraph (Fin n) where Adj v w := v % r ≠ w % r
 
+lemma turanGraph_adj {v w} :
+  (turanGraph n r).Adj v w ↔ v % r ≠ w % r := by rfl
+
 instance turanGraph.instDecidableRelAdj : DecidableRel (turanGraph n r).Adj := by
   dsimp only [turanGraph]; infer_instance