feat(Combinatorics/SimpleGraph): define odd components (#22125)

Adds the definition `oddComponents`: The set of connected components of odd cardinality.
In preparation for Tutte's theorem.



Co-authored-by: Pim Otte <otte.pim@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: pimotte

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

@@ -234,21 +234,26 @@ lemma disjiUnion_supp_toFinset_eq_supp_toFinset {G' : SimpleGraph V} (h : G ≤
 
 end Fintype
 
-lemma ConnectedComponent.odd_card_supp_iff_odd_subcomponents [Finite V] {G'}
+/-- The odd components are the connected components of odd cardinality. This definition excludes
+infinite components. -/
+abbrev oddComponents : Set G.ConnectedComponent := {c : G.ConnectedComponent | Odd c.supp.ncard}
+
+lemma ConnectedComponent.odd_oddComponents_ncard_subset_supp [Finite V] {G'}
     (h : G ≤ G') (c' : ConnectedComponent G') :
-    Odd c'.supp.ncard ↔
-      Odd {c : ConnectedComponent G | c.supp ⊆ c'.supp ∧ Odd c.supp.ncard}.ncard := by
+    Odd {c ∈ G.oddComponents | c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard := by
   simp_rw [← Set.Nat.card_coe_set_eq]
   classical
   cases nonempty_fintype V
-  rw [Nat.card_eq_card_toFinset, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
-  simp only [Finset.card_disjiUnion, Set.toFinset_card]
+  rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
+  simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
   rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
-  simp only [Nat.card_eq_fintype_card, Finset.filter_filter]
+  congr! 2
+  ext c
+  simp only [Set.toFinset_setOf, mem_filter, mem_univ, true_and, ← Set.ncard_coe_Finset, coe_filter,
+    mem_supp_iff, and_comm (a := _ ⊆ _)]
   rfl
 
-lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔
-    Odd {c : ConnectedComponent G | Odd c.supp.ncard}.ncard := by
+lemma odd_ncard_oddComponents [Finite V] : Odd G.oddComponents.ncard ↔ Odd (Nat.card V) := by
   classical
   cases nonempty_fintype V
   rw [Nat.card_eq_fintype_card]
@@ -259,24 +264,22 @@ lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔
     (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]
   simp_rw [Set.toFinset_card, ← Nat.card_eq_fintype_card, ← Finset.coe_filter_univ,
     Set.ncard_coe_Finset, Set.Nat.card_coe_set_eq]
-  exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard))
+  exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm
 
-lemma ncard_odd_components_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') :
-     {c : ConnectedComponent G' | Odd c.supp.ncard}.ncard
-      ≤ {c : ConnectedComponent G | Odd c.supp.ncard}.ncard := by
+lemma ncard_oddComponents_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') :
+     G'.oddComponents.ncard ≤ G.oddComponents.ncard := by
   have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
-      {c' : G.ConnectedComponent | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty := by
+      {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty := by
     refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
     simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h']
-      using (c.odd_card_supp_iff_odd_subcomponents _ h).mp hc
-  let f : {c : ConnectedComponent G' | Odd (Nat.card c.supp)} →
-      {c : ConnectedComponent G | Odd (Nat.card c.supp)} :=
-    fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.2⟩
+      using (c.odd_oddComponents_ncard_subset_supp _ h).2 hc
+  let f : G'.oddComponents → G.oddComponents :=
+    fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.1⟩
   refine Finite.card_le_of_injective f fun c c' fcc' ↦ ?_
   simp only [Subtype.mk.injEq, f] at fcc'
   exact Subtype.val_injective (ConnectedComponent.eq_of_common_vertex
-    ((fcc' ▸ (aux c.1 c.2).choose_spec.1) (ConnectedComponent.nonempty_supp _).some_mem)
-      ((aux c'.1 c'.2).choose_spec.1 (ConnectedComponent.nonempty_supp _).some_mem))
+    ((fcc' ▸ (aux c.1 c.2).choose_spec.2) (ConnectedComponent.nonempty_supp _).some_mem)
+      ((aux c'.1 c'.2).choose_spec.2 (ConnectedComponent.nonempty_supp _).some_mem))
 
 end WalkCounting
 

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -276,11 +276,10 @@ lemma even_card_of_isPerfectMatching [Fintype V] [DecidableEq V] [DecidableRel G
   simpa using (hM.induce_connectedComponent_isMatching c).even_card
 
 lemma odd_matches_node_outside [Finite V] {u : Set V}
-    {c : ConnectedComponent (Subgraph.deleteVerts ⊤ u).coe}
-    (hM : M.IsPerfectMatching) (codd : Odd c.supp.ncard) :
-    ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.supp := by
+    (hM : M.IsPerfectMatching) (c : (Subgraph.deleteVerts ⊤ u).coe.oddComponents) :
+    ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.val.supp := by
   by_contra! h
-  have hMmatch : (M.induce c.supp).IsMatching := by
+  have hMmatch : (M.induce c.val.supp).IsMatching := by
     intro v hv
     obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
     obtain ⟨⟨v', hv'⟩, ⟨hv , rfl⟩⟩ := hv
@@ -292,10 +291,10 @@ lemma odd_matches_node_outside [Finite V] {u : Set V}
       Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
       and_true] at hv' ⊢
     trivial
-  apply Nat.not_even_iff_odd.2 codd
-  haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c)).verts := Fintype.ofFinite _
+  apply Nat.not_even_iff_odd.2 c.prop
+  haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
   classical
-  haveI : Fintype (c.supp) := Fintype.ofFinite _
+  haveI : Fintype (c.val.supp) := Fintype.ofFinite _
   simpa [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_image, Nat.card_eq_fintype_card,
     Set.toFinset_image,Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card,
     ← Set.Nat.card_coe_set_eq] using hMmatch.even_card