[Merged by Bors] - feat(combinatorics/simple_graph/{basic,subgraph,clique,coloring}): add induced graphs, characterization of cliques, and bounds for colorings

src/combinatorics/simple_graph/basic.lean

@@ -640,6 +640,75 @@ lemma delete_edges_eq_inter_edge_set (s : set (sym2 V)) :
   G.delete_edges s = G.delete_edges (s ∩ G.edge_set) :=
 by { ext, simp [imp_false] { contextual := tt } }
 
+/-! ## Map and comap -/
+
+/-- Given an injective function, there is an covariant induced map on graphs by pushing forward
+the adjacency relation.
+
+This is injective (see `simple_graph.map_injective`). -/
+protected def map (f : V ↪ W) (G : simple_graph V) : simple_graph W :=
+{ adj := relation.map G.adj f f }
+
+@[simp] lemma map_adj (f : V ↪ W) (G : simple_graph V) (u v : W) :
+  (G.map f).adj u v ↔ ∃ (u' v' : V), G.adj u' v' ∧ f u' = u ∧ f v' = v := iff.rfl
+
+lemma map_monotone (f : V ↪ W) : monotone (simple_graph.map f) :=
+by { rintros G G' h _ _ ⟨u, v, ha, rfl, rfl⟩, exact ⟨_, _, h ha, rfl, rfl⟩ }
+
+/-- Given a function, there is a contravariant induced map on graphs by pulling back the
+adjacency relation.
+This is one of the ways of creating induced graphs. See `simple_graph.induce` for a wrapper.
+
+This is surjective when `f` is injective (see `simple_graph.comap_surjective`).-/
+@[simps] protected def comap (f : V → W) (G : simple_graph W) : simple_graph V :=
+{ adj := λ u v, G.adj (f u) (f v) }
+
+lemma comap_monotone (f : V ↪ W) : monotone (simple_graph.comap f) :=
+by { intros G G' h _ _ ha, exact h ha }
+
+@[simp] lemma comap_map_eq (f : V ↪ W) (G : simple_graph V) : (G.map f).comap f = G :=
+by { ext, simp }
+
+lemma left_inverse_comap_map (f : V ↪ W) :
+  function.left_inverse (simple_graph.comap f) (simple_graph.map f) := comap_map_eq f
+
+lemma map_injective (f : V ↪ W) : function.injective (simple_graph.map f) :=
+(left_inverse_comap_map f).injective
+
+lemma comap_surjective (f : V ↪ W) : function.surjective (simple_graph.comap f) :=
+(left_inverse_comap_map f).surjective
+
+lemma map_le_iff_le_comap (f : V ↪ W) (G : simple_graph V) (G' : simple_graph W) :
+  G.map f ≤ G' ↔ G ≤ G'.comap f :=
+⟨λ h u v ha, h ⟨_, _, ha, rfl, rfl⟩, by { rintros h _ _ ⟨u, v, ha, rfl, rfl⟩, exact h ha, }⟩
+
+lemma map_comap_le (f : V ↪ W) (G : simple_graph W) : (G.comap f).map f ≤ G :=
+by { rw map_le_iff_le_comap, exact le_refl _ }
+
+/-! ## Induced graphs -/
+
+/- Given a set `s` of vertices, we can restrict a graph to those vertices by restricting its
+adjacency relation. This gives a map between `simple_graph V` and `simple_graph s`.
+
+There is also a notion of induced subgraphs (see `simple_graph.subgraph.induce`). -/
+
+/-- Restrict a graph to the vertices in the set `s`, deleting all edges incident to vertices
+outside the set. This is a wrapper around `simple_graph.comap`. -/
+@[reducible] def induce (s : set V) (G : simple_graph V) : simple_graph s :=
+G.comap (function.embedding.subtype _)
+
+/-- Given a graph on a set of vertices, we can make it be a `simple_graph V` by
+adding in the remaining vertices without adding in any additional edges.
+This is a wrapper around `simple_graph.map`. -/
+@[reducible] def spanning_coe {s : set V} (G : simple_graph s) : simple_graph V :=
+G.map (function.embedding.subtype _)
+
+lemma induce_spanning_coe {s : set V} {G : simple_graph s} : G.spanning_coe.induce s = G :=
+comap_map_eq _ _
+
+lemma spanning_coe_induce_le (s : set V) : (G.induce s).spanning_coe ≤ G :=
+map_comap_le _ _
+
 section finite_at
 
 /-!
@@ -999,6 +1068,20 @@ begin
   apply sym2.map.injective hinj,
 end
 
+/-- Every graph homomomorphism from a complete graph is injective. -/
+lemma injective_of_top_hom (f : (⊤ : simple_graph V) →g G') : function.injective f :=
+begin
+  intros v w h,
+  contrapose! h,
+  exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h)),
+end
+
+/-- There is a homomorphism to a graph from a comapped graph.
+When the function is injective, this is an embedding (see `simple_graph.embedding.comap`). -/
+@[simps] protected def comap (f : V → W) (G : simple_graph W) : G.comap f →g G :=
+{ to_fun := f,
+  map_rel' := by simp }
+
 variable {G'' : simple_graph X}
 
 /-- Composition of graph homomorphisms. -/
@@ -1039,12 +1122,32 @@ map_adj_iff f
     exact f.inj' h,
   end }
 
+/-- Given an injective function, there is an embedding from the comapped graph into the original
+graph. -/
+@[simps]
+protected def comap (f : V ↪ W) (G : simple_graph W) : G.comap f ↪g G :=
+{ map_rel_iff' := by simp, ..f }
+
+/-- Given an injective function, there is an embedding from a graph into the mapped graph. -/
+@[simps]
+protected def map (f : V ↪ W) (G : simple_graph V) : G ↪g G.map f :=
+{ map_rel_iff' := by simp, ..f }
+
+/-- Induced graphs embed in the original graph.
+
+Note that if `G.induce s = ⊤` (i.e., if `s` is a clique) then this gives the embedding of a
+complete graph. -/
+@[reducible] protected def induce (s : set V) : G.induce s ↪g G :=
+simple_graph.embedding.comap (function.embedding.subtype _) G
+
+/-- Graphs on a set of vertices embed in their `spanning_coe`. -/
+@[reducible] protected def spanning_coe {s : set V} (G : simple_graph s) : G ↪g G.spanning_coe :=
+simple_graph.embedding.map (function.embedding.subtype _) G
+
 /-- Embeddings of types induce embeddings of complete graphs on those types. -/
 protected def complete_graph {α β : Type*} (f : α ↪ β) :
   (⊤ : simple_graph α) ↪g (⊤ : simple_graph β) :=
-{ to_fun := f,
-  inj' := f.inj',
-  map_rel_iff' := by simp }
+{ map_rel_iff' := by simp, ..f }
 
 variables {G'' : simple_graph X}
 
@@ -1112,6 +1215,23 @@ map_adj_iff f
 lemma card_eq_of_iso [fintype V] [fintype W] (f : G ≃g G') : fintype.card V = fintype.card W :=
 by convert (fintype.of_equiv_card f.to_equiv).symm
 
+/-- Given a bijection, there is an embedding from the comapped graph into the original
+graph. -/
+@[simps] protected def comap (f : V ≃ W) (G : simple_graph W) : G.comap f.to_embedding ≃g G :=
+{ map_rel_iff' := by simp, ..f }
+
+/-- Given an injective function, there is an embedding from a graph into the mapped graph. -/
+@[simps] protected def map (f : V ≃ W) (G : simple_graph V) : G ≃g G.map f.to_embedding :=
+{ map_rel_iff' := by simp, ..f }
+
+/-- Equivalences of types induce isomorphisms of complete graphs on those types. -/
+protected def complete_graph {α β : Type*} (f : α ≃ β) :
+  (⊤ : simple_graph α) ≃g (⊤ : simple_graph β) :=
+{ map_rel_iff' := by simp, ..f }
+
+lemma to_embedding_complete_graph {α β : Type*} (f : α ≃ β) :
+  (iso.complete_graph f).to_embedding = embedding.complete_graph f.to_embedding := rfl
+
 variables {G'' : simple_graph X}
 
 /-- Composition of graph isomorphisms. -/

src/combinatorics/simple_graph/clique.lean

@@ -22,7 +22,6 @@ adjacent.
 ## TODO
 
 * Clique numbers
-* Going back and forth between cliques and complete subgraphs or embeddings of complete graphs.
 * Do we need `clique_set`, a version of `clique_finset` for infinite graphs?
 -/
 
@@ -41,6 +40,21 @@ abbreviation is_clique (s : set α) : Prop := s.pairwise G.adj
 
 lemma is_clique_iff : G.is_clique s ↔ s.pairwise G.adj := iff.rfl
 
+/-- A clique is a set of vertices whose induced graph is complete. -/
+lemma is_clique_iff_induce_eq : G.is_clique s ↔ G.induce s = ⊤ :=
+begin
+  rw is_clique_iff,
+  split,
+  { intro h,
+    ext ⟨v, hv⟩ ⟨w, hw⟩,
+    simp only [comap_adj, subtype.coe_mk, top_adj, ne.def, subtype.mk_eq_mk],
+    exact ⟨adj.ne, h hv hw⟩, },
+  { intros h v hv w hw hne,
+    have : (G.induce s).adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl,
+    conv_lhs at this { rw h },
+    simpa [hne], }
+end
+
 instance [decidable_eq α] [decidable_rel G.adj] {s : finset α} : decidable (G.is_clique s) :=
 decidable_of_iff' _ G.is_clique_iff
 
@@ -123,6 +137,57 @@ def clique_free (n : ℕ) : Prop := ∀ t, ¬ G.is_n_clique n t
 
 variables {G H}
 
+lemma not_clique_free_of_top_embedding {n : ℕ}
+  (f : (⊤ : simple_graph (fin n)) ↪g G) : ¬ G.clique_free n :=
+begin
+  simp only [clique_free, is_n_clique_iff, is_clique_iff_induce_eq, not_forall, not_not],
+  use finset.univ.map f.to_embedding,
+  simp only [card_map, finset.card_fin, eq_self_iff_true, and_true],
+  ext ⟨v, hv⟩ ⟨w, hw⟩,
+  simp only [coe_map, rel_embedding.coe_fn_to_embedding, set.mem_image,
+    coe_univ, set.mem_univ, true_and] at hv hw,
+  obtain ⟨v', rfl⟩ := hv,
+  obtain ⟨w', rfl⟩ := hw,
+  simp only [f.map_adj_iff, comap_adj, function.embedding.coe_subtype, subtype.coe_mk, top_adj,
+    ne.def, subtype.mk_eq_mk],
+  exact (function.embedding.apply_eq_iff_eq _ _ _).symm.not,
+end
+
+/-- An embedding of a complete graph that witnesses the fact that the graph is not clique-free. -/
+noncomputable
+def top_embedding_of_not_clique_free {n : ℕ} (h : ¬ G.clique_free n) :
+  (⊤ : simple_graph (fin n)) ↪g G :=
+begin
+  simp only [clique_free, is_n_clique_iff, is_clique_iff_induce_eq, not_forall, not_not] at h,
+  obtain ⟨ha, hb⟩ := h.some_spec,
+  have : (⊤ : simple_graph (fin h.some.card)) ≃g (⊤ : simple_graph h.some),
+  { apply iso.complete_graph,
+    simpa using (fintype.equiv_fin h.some).symm },
+  rw ← ha at this,
+  convert (embedding.induce ↑h.some).comp this.to_embedding;
+  exact hb.symm,
+end
+
+lemma not_clique_free_iff (n : ℕ) :
+  ¬ G.clique_free n ↔ nonempty ((⊤ : simple_graph (fin n)) ↪g G) :=
+begin
+  split,
+  { exact λ h, ⟨top_embedding_of_not_clique_free h⟩ },
+  { rintro ⟨f⟩,
+    exact not_clique_free_of_top_embedding f },
+end
+
+lemma clique_free_iff {n : ℕ} :
+  G.clique_free n ↔ is_empty ((⊤ : simple_graph (fin n)) ↪g G) :=
+by rw [← not_iff_not, not_clique_free_iff, not_is_empty_iff]
+
+lemma not_clique_free_card_of_top_embedding [fintype α] (f : (⊤ : simple_graph α) ↪g G) :
+  ¬ G.clique_free (card α) :=
+begin
+  rw [not_clique_free_iff],
+  use (iso.complete_graph (fintype.equiv_fin α)).symm.to_embedding.trans f,
+end
+
 lemma clique_free_bot (h : 2 ≤ n) : (⊥ : simple_graph α).clique_free n :=
 begin
   rintro t ht,
@@ -140,6 +205,15 @@ end
 lemma clique_free.anti (h : G ≤ H) : H.clique_free n → G.clique_free n :=
 forall_imp $ λ s, mt $ is_n_clique.mono h
 
+/-- See `simple_graph.clique_free_chromatic_number_succ` for a tighter bound. -/
+lemma clique_free_of_card_lt [fintype α] (hc : card α < n) : G.clique_free n :=
+begin
+  by_contra h,
+  refine nat.lt_le_antisymm hc _,
+  rw [clique_free_iff, not_is_empty_iff] at h,
+  simpa using fintype.card_le_of_embedding h.some.to_embedding,
+end
+
 end clique_free
 
 /-! ### Set of cliques -/

src/combinatorics/simple_graph/coloring.lean

@@ -5,6 +5,7 @@ Authors: Arthur Paulino, Kyle Miller
 -/
 
 import combinatorics.simple_graph.subgraph
+import combinatorics.simple_graph.clique
 import data.nat.lattice
 import data.setoid.partition
 import order.antichain
@@ -43,8 +44,6 @@ a complete graph, whose vertices represent the colors.
     * https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/coloring.lean
     * https://github.com/kmill/lean-graphcoloring/blob/master/src/graph.lean
 
-  * Lowerbound for cliques
-
   * Trees
 
   * Planar graphs
@@ -416,4 +415,46 @@ begin
       contradiction }, },
 end
 
+/-! ### Cliques -/
+
+lemma is_clique.card_le_of_coloring {s : finset V} (h : G.is_clique s)
+  [fintype α] (C : G.coloring α) :
+  s.card ≤ fintype.card α :=
+begin
+  rw is_clique_iff_induce_eq at h,
+  have f : G.induce ↑s ↪g G := embedding.induce ↑s,
+  rw h at f,
+  convert fintype.card_le_of_injective _ (C.comp f.to_hom).injective_of_top_hom using 1,
+  simp,
+end
+
+lemma is_clique.card_le_of_colorable {s : finset V} (h : G.is_clique s)
+  {n : ℕ} (hc : G.colorable n) :
+  s.card ≤ n :=
+begin
+  convert h.card_le_of_coloring hc.some,
+  simp,
+end
+
+-- TODO eliminate `fintype V` constraint once chromatic numbers are refactored.
+-- This is just to ensure the chromatic number exists.
+lemma is_clique.card_le_chromatic_number [fintype V] {s : finset V} (h : G.is_clique s) :
+  s.card ≤ G.chromatic_number :=
+h.card_le_of_colorable G.colorable_chromatic_number_of_fintype
+
+protected
+lemma colorable.clique_free {n m : ℕ} (hc : G.colorable n) (hm : n < m) : G.clique_free m :=
+begin
+  by_contra h,
+  simp only [clique_free, is_n_clique_iff, not_forall, not_not] at h,
+  obtain ⟨s, h, rfl⟩ := h,
+  exact nat.lt_le_antisymm hm (h.card_le_of_colorable hc),
+end
+
+-- TODO eliminate `fintype V` constraint once chromatic numbers are refactored.
+-- This is just to ensure the chromatic number exists.
+lemma clique_free_of_chromatic_number_lt [fintype V] {n : ℕ} (hc : G.chromatic_number < n) :
+  G.clique_free n :=
+G.colorable_chromatic_number_of_fintype.clique_free hc
+
 end simple_graph