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

src/combinatorics/simple_graph/matching.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alena Gusakov, Arthur Paulino, Kyle Miller
 -/
 import combinatorics.simple_graph.subgraph
+import combinatorics.simple_graph.degree_sum
 
 /-!
 # Matchings
@@ -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,32 @@ 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.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,
+  use ⟨x, M.edge_vert he⟩,
+  simp only [is_matching.to_edge, subtype.mk_eq_mk, subtype.coe_mk, sym2.congr_right],
+  exact ((h (M.edge_vert he)).some_spec.2 y he).symm,
+end
+
+lemma is_matching.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⟩ :=
+begin
+  simp only [is_matching.to_edge, subtype.mk_eq_mk],
+  rw sym2.eq_swap,
+  congr,
+  { exact ((h (M.edge_vert ha)).some_spec.2 w ha).symm, },
+  { exact ((h (M.edge_vert (M.symm ha))).some_spec.2 v (M.symm ha)), },
+end
+
 /--
 The subgraph `M` of `G` is a perfect matching on `G` if it's a matching and every vertex `G` is
 matched.
@@ -65,6 +93,19 @@ 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} [hM : fintype M.support] [decidable_eq V]
+  [decidable_rel G.adj] (h : M.is_matching) :
+  even (M.support.to_finset.card) :=
+begin
+  classical,
+  unfreezingI { rw h.support_eq_verts at hM },
+  rw is_matching_iff_forall_degree at h,
+  have := M.coe.sum_degrees_eq_twice_card_edges,
+  simp [h] at this,
+  sorry,
+  -- exact ⟨_, this⟩,
+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 +115,21 @@ 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] [decidable_eq V] [decidable_rel G.adj]
+    (h : M.is_perfect_matching) : even (fintype.card V) :=
+begin
+  classical,
+  rw is_perfect_matching_iff_forall_degree at h,
+  have := M.spanning_coe.sum_degrees_eq_twice_card_edges,
+  simp [h] at this,
+  exact ⟨_, this⟩,
+end
+
 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}
 
+lemma adj_irrefl {v : V} (G' : subgraph G) : ¬G'.adj v v :=
+by { by_contra h, exact 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⟩
 
@@ -348,6 +351,11 @@ 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)
 
+noncomputable instance (G' : subgraph G) [fintype G'.support] (a : V) :
+  fintype (G'.neighbor_set a) :=
+fintype.of_injective (λ b, ⟨b.1, a, G'.adj_symm b.2⟩ : G'.neighbor_set a → G'.support)
+  (λ b c h, by { ext, convert congr_arg subtype.val h })
+
 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
@@ -380,6 +388,11 @@ begin
   exact fintype.card_congr (coe_neighbor_set_equiv v),
 end
 
+@[simp] lemma spanning_coe_degree {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