Impl bipartiteDoubleCover

Author: mitchell-horner

Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -445,4 +445,88 @@ theorem degree_le_between_add_compl (hw : w ∈ sᶜ) :
 
 end Between
 
+section BipartiteDoubleCover
+
+/-- `bipartiteDoubleCover G` has two vertices `inl v` and `inr v` for each vertex `v` in `G`
+such that `inl v` (`inr v`) is adjacent to `inr w` (`inl w`) iff `v` is adjacent to `w` in `G`. -/
+@[simp] def bipartiteDoubleCover (G : SimpleGraph V) : SimpleGraph (V ⊕ V) where
+  Adj v w := match v, w with
+    | .inl v', .inr w' | .inr v', .inl w' => G.Adj v' w'
+    | _, _ => False
+  symm v w :=  match v, w with
+    | .inl _, .inr _ | .inr _, .inl _ => G.adj_symm
+    | .inl _, .inl _ | .inr _, .inr _ => id
+
+instance [h : DecidableRel G.Adj] : DecidableRel G.bipartiteDoubleCover.Adj :=
+  fun v w ↦ match v, w with
+    | .inl _, .inr _ | .inr _, .inl _ => h _ _
+    | .inl _, .inl _ | .inr _, .inr _ => inferInstanceAs (Decidable False)
+
+/-- The bipartite double cover of `G` is contained in the corresponding complete bipartite graph,
+that is, the bipartite double cover of `G` is bipartite. -/
+theorem bipartiteDoubleCover_le : G.bipartiteDoubleCover ≤ completeBipartiteGraph V V :=
+  fun v w hadj ↦ match v, w with
+  | .inl _, .inr _ | .inr _, .inl _ => by simp
+  | .inl _, .inl _ | .inr _, .inr _ => by simp at hadj
+
+/-- The bipartite double cover of `G` has twice the number of edges as `G`. -/
+theorem bipartiteDoubleCover_card_edgeFinset [Fintype V] [DecidableRel G.Adj] :
+    #G.bipartiteDoubleCover.edgeFinset = 2 * #G.edgeFinset := by
+  rw [two_mul_card_edgeFinset, eq_comm]
+  apply card_bij (fun (v, w) _ ↦ s(.inl v, .inr w)) (fun _ h ↦ by simpa using h)
+    (fun (_, _) _ (_, _) _ ↦ by simp) (fun e he ↦ ?_)
+  induction e with | _ v w
+  rw [Set.mem_toFinset, mem_edgeSet] at he
+  match v, w with
+  | .inl _, .inr _ => simpa using he
+  | .inr _, .inl _ => simpa using he.symm
+  | .inl _, .inl _ | .inr _, .inr _ => simp at he
+
+/-- If the double cover of `G` contains `completeBipartiteGraph α β`, then `G` also
+contains `completeBipartiteGraph α β`. -/
+theorem bipartiteDoubleCover_completeBipartiteGraph_isContained
+    {α β : Type*} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β]
+    (h : completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover) :
+    completeBipartiteGraph α β ⊑ G := by
+  rw [completeBipartiteGraph_isContained_iff] at h ⊢
+  obtain ⟨left, right, card_left, card_right, h⟩ := h
+  simp_rw [← card_left, ← card_right]
+  obtain ⟨l, hl⟩ : left.Nonempty := card_pos.mp <| card_pos.trans_le card_left.ge
+  obtain ⟨r, hr⟩ : right.Nonempty := card_pos.mp <| card_pos.trans_le card_right.ge
+  have hmem_left {l'} (hl' : l' ∈ left) : (l.isLeft → l'.isLeft) ∧ (l.isRight → l'.isRight) := by
+    rcases l with l | l <;> rcases r with r | r <;> rcases l' with l' | l'
+    all_goals solve | simp | simpa using h hl hr | simpa using h hl' hr
+  have hmem_right {r'} (hr' : r' ∈ right) : (r.isLeft → r'.isLeft) ∧ (r.isRight → r'.isRight) := by
+    rcases l with l | l <;> rcases r with r | r <;> rcases r' with r' | r'
+    all_goals solve | simp | simpa using h hl hr | simpa using h hl hr'
+  rcases l with l | l <;> rcases r with r | r
+  · simpa using h hl hr
+  · refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩
+    · exact card_bij (fun i _ ↦ .inl i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
+        (fun i hi ↦ ⟨i.getLeft <| (hmem_left hi).left Sum.isLeft_inl, by simp [hi]⟩)
+    · exact card_bij (fun j hj ↦ .inr j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
+        (fun j hj ↦ ⟨j.getRight <| (hmem_right hj).right Sum.isRight_inr, by simp [hj]⟩)
+    · rw [mem_coe, mem_toLeft] at hi
+      rw [mem_coe, mem_toRight] at hj
+      simpa using h hi hj
+  · refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
+    · exact card_bij (fun i _ ↦ .inr i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
+        (fun i hi ↦ ⟨i.getRight <| (hmem_left hi).right Sum.isRight_inr, by simp [hi]⟩)
+    · exact card_bij (fun j hj ↦ .inl j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
+        (fun j hj ↦ ⟨j.getLeft <| (hmem_right hj).left Sum.isLeft_inl, by simp [hj]⟩)
+    · rw [mem_coe, mem_toRight] at hi
+      rw [mem_coe, mem_toLeft] at hj
+      simpa using h hi hj
+  · simpa using h hl hr
+
+theorem bipartiteDoubleCover_isBipartiteWith :
+    G.bipartiteDoubleCover.IsBipartiteWith {v | v.isLeft} {w | w.isRight} where
+  disjoint := by simp [Set.disjoint_iff_forall_ne]
+  mem_of_adj := by simp
+
+theorem bipartiteDoubleCover_isBipartite : G.bipartiteDoubleCover.IsBipartite :=
+  bipartiteDoubleCover_isBipartiteWith.isBipartite
+
+end BipartiteDoubleCover
+
 end SimpleGraph