[Merged by Bors] - feat(combinatorics/simple_graph/matchings): even_card_vertices_of_perfect_matching

src/combinatorics/simple_graph/matching.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Alena Gusakov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alena Gusakov, Arthur Paulino, Kyle Miller
 -/
+import combinatorics.simple_graph.degree_sum
 import combinatorics.simple_graph.subgraph
 
 /-!
@@ -27,8 +28,9 @@ one edge, and the edges of the subgraph represent the paired vertices.
 
 ## TODO
 
-* Lemma stating that the existence of a perfect matching on `G` implies that
-  the cardinality of `V` is even (assuming it's finite)
+* Define an `other` function and prove useful results about it (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/266205863)
+
+* Provide a bicoloring for matchings (https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/265495120)
 
 * Tutte's Theorem
 
@@ -48,6 +50,33 @@ We say that the vertices in `M.support` are *matched* or *saturated*.
 -/
 def is_matching : Prop := ∀ ⦃v⦄, v ∈ M.verts → ∃! w, M.adj v w
 
+/-- Given a vertex, returns the unique edge of the matching it is incident to. -/
+noncomputable def is_matching.to_edge {M : subgraph G} (h : M.is_matching)
+  (v : M.verts) : M.edge_set :=
+⟨⟦(v, (h v.property).some)⟧, (h v.property).some_spec.1⟩
+
+lemma is_matching.to_edge_eq_of_adj {M : subgraph G} (h : M.is_matching) {v w : V}
+  (hv : v ∈ M.verts) (hvw : M.adj v w) : h.to_edge ⟨v, hv⟩ = ⟨⟦(v, w)⟧, hvw⟩ :=
+begin
+  simp only [is_matching.to_edge, subtype.mk_eq_mk],
+  congr,
+  exact ((h (M.edge_vert hvw)).some_spec.2 w hvw).symm,
+end
+
+lemma is_matching.to_edge.surjective {M : subgraph G} (h : M.is_matching) :
+  function.surjective h.to_edge :=
+begin
+  rintro ⟨e, he⟩,
+  refine sym2.ind (λ x y he, _) e he,
+  exact ⟨⟨x, M.edge_vert he⟩, h.to_edge_eq_of_adj _ he⟩,
+end
+
+lemma is_matching.to_edge_eq_to_edge_of_adj {M : subgraph G} {v w : V}
+  (h : M.is_matching) (hv : v ∈ M.verts) (hw : w ∈ M.verts) (ha : M.adj v w) :
+  h.to_edge ⟨v, hv⟩ = h.to_edge ⟨w, hw⟩ :=
+by rw [h.to_edge_eq_of_adj hv ha, h.to_edge_eq_of_adj hw (M.symm ha),
+       subtype.mk_eq_mk, sym2.eq_swap]
+
 /--
 The subgraph `M` of `G` is a perfect matching on `G` if it's a matching and every vertex `G` is
 matched.
@@ -65,6 +94,16 @@ lemma is_matching_iff_forall_degree {M : subgraph G} [Π (v : V), fintype (M.nei
   M.is_matching ↔ ∀ (v : V), v ∈ M.verts → M.degree v = 1 :=
 by simpa [degree_eq_one_iff_unique_adj]
 
+lemma is_matching.even_card {M : subgraph G} [fintype M.verts] (h : M.is_matching) :
+  even M.verts.to_finset.card :=
+begin
+  classical,
+  rw is_matching_iff_forall_degree at h,
+  use M.coe.edge_finset.card,
+  rw ← M.coe.sum_degrees_eq_twice_card_edges,
+  simp [h, finset.card_univ],
+end
+
 lemma is_perfect_matching_iff : M.is_perfect_matching ↔ ∀ v, ∃! w, M.adj v w :=
 begin
   refine ⟨_, λ hm, ⟨λ v hv, hm v, λ v, _⟩⟩,
@@ -74,6 +113,14 @@ begin
     exact M.edge_vert hw }
 end
 
+lemma is_perfect_matching_iff_forall_degree {M : subgraph G} [Π v, fintype (M.neighbor_set v)] :
+  M.is_perfect_matching ↔ ∀ v, M.degree v = 1 :=
+by simp [degree_eq_one_iff_unique_adj, is_perfect_matching_iff]
+
+lemma is_perfect_matching.even_card {M : subgraph G} [fintype V] (h : M.is_perfect_matching) :
+  even (fintype.card V) :=
+by { classical, simpa [h.2.card_verts] using is_matching.even_card h.1 }
+
 end subgraph
 
 end simple_graph

src/combinatorics/simple_graph/subgraph.lean

@@ -65,6 +65,9 @@ namespace subgraph
 
 variables {V : Type u} {G : simple_graph V}
 
+protected lemma loopless (G' : subgraph G) : irreflexive G'.adj :=
+λ v h, G.loopless v (G'.adj_sub h)
+
 lemma adj_comm (G' : subgraph G) (v w : V) : G'.adj v w ↔ G'.adj w v :=
 ⟨λ x, G'.symm x, λ x, G'.symm x⟩
 
@@ -93,8 +96,8 @@ In general, this adds in all vertices from `V` as isolated vertices. -/
   symm := G'.symm,
   loopless := λ v hv, G.loopless v (G'.adj_sub hv) }
 
-@[simp] lemma spanning_coe_adj_sub (H : subgraph G) (u v : H.verts) (h : H.spanning_coe.adj u v) :
-  G.adj u v := H.adj_sub h
+@[simp] lemma adj.of_spanning_coe {G' : subgraph G} {u v : G'.verts}
+  (h : G'.spanning_coe.adj u v) : G.adj u v := G'.adj_sub h
 
 /-- `spanning_coe` is equivalent to `coe` for a subgraph that `is_spanning`.  -/
 @[simps] def spanning_coe_equiv_coe_of_spanning (G' : subgraph G) (h : G'.is_spanning) :
@@ -123,6 +126,9 @@ def neighbor_set (G' : subgraph G) (v : V) : set V := set_of (G'.adj v)
 lemma neighbor_set_subset (G' : subgraph G) (v : V) : G'.neighbor_set v ⊆ G.neighbor_set v :=
 λ w h, G'.adj_sub h
 
+lemma neighbor_set_subset_verts (G' : subgraph G) (v : V) : G'.neighbor_set v ⊆ G'.verts :=
+λ _ h, G'.edge_vert (adj_symm G' h)
+
 @[simp] lemma mem_neighbor_set (G' : subgraph G) (v w : V) : w ∈ G'.neighbor_set v ↔ G'.adj v w :=
 iff.rfl
 
@@ -374,10 +380,18 @@ def finite_at_of_subgraph {G' G'' : subgraph G} [decidable_rel G'.adj]
    fintype (G'.neighbor_set v) :=
 set.fintype_subset (G''.neighbor_set v) (neighbor_set_subset_of_subgraph h v)
 
+instance (G' : subgraph G) [fintype G'.verts]
+  (v : V) [decidable_pred (∈ G'.neighbor_set v)] : fintype (G'.neighbor_set v) :=
+set.fintype_subset G'.verts (neighbor_set_subset_verts G' v)
+
 instance coe_finite_at {G' : subgraph G} (v : G'.verts) [fintype (G'.neighbor_set v)] :
   fintype (G'.coe.neighbor_set v) :=
 fintype.of_equiv _ (coe_neighbor_set_equiv v).symm
 
+lemma is_spanning.card_verts [fintype V] {G' : subgraph G} [fintype G'.verts]
+  (h : G'.is_spanning) : G'.verts.to_finset.card = fintype.card V :=
+by { rw is_spanning_iff at h, simpa [h] }
+
 /-- The degree of a vertex in a subgraph. It's zero for vertices outside the subgraph. -/
 def degree (G' : subgraph G) (v : V) [fintype (G'.neighbor_set v)] : ℕ :=
 fintype.card (G'.neighbor_set v)
@@ -406,6 +420,11 @@ begin
   exact fintype.card_congr (coe_neighbor_set_equiv v),
 end
 
+@[simp] lemma degree_spanning_coe {G' : G.subgraph} (v : V) [fintype (G'.neighbor_set v)]
+  [fintype (G'.spanning_coe.neighbor_set v)] :
+  G'.spanning_coe.degree v = G'.degree v :=
+by { rw [← card_neighbor_set_eq_degree, subgraph.degree], congr }
+
 lemma degree_eq_one_iff_unique_adj {G' : subgraph G} {v : V} [fintype (G'.neighbor_set v)] :
   G'.degree v = 1 ↔ ∃! (w : V), G'.adj v w :=
 begin