[Merged by Bors] - feat(Combinatorics/Graph): infimum

Mathlib.lean

@@ -3425,6 +3425,7 @@ public import Mathlib.Combinatorics.Enumerative.Schroder
 public import Mathlib.Combinatorics.Enumerative.Stirling
 public import Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
 public import Mathlib.Combinatorics.Graph.Basic
+public import Mathlib.Combinatorics.Graph.InterUnion
 public import Mathlib.Combinatorics.Graph.Subgraph
 public import Mathlib.Combinatorics.HalesJewett
 public import Mathlib.Combinatorics.Hall.Basic

Mathlib/Combinatorics/Graph/InterUnion.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Jun Kwon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Nelson, Jun Kwon
+-/
+module
+
+public import Mathlib.Data.Set.Lattice
+public import Mathlib.Combinatorics.Graph.Subgraph
+
+/-!
+# Intersection and union of graphs
+
+This file defines the intersection and union of graphs.
+
+## Main definitions
+
+- `Graph.iInter` : the intersection of a nonempty family of graphs
+- `Graph.sInter` : the intersection of a nonempty set of graphs
+- `Graph.inter` : the intersection of two graphs
+
+## Implementation notes
+
+Intersections are defined here as the maximal mutual subgraph of the given graphs.
+This has the effect of, when taking the intersection of non-compatible graphs,
+**any non-compatible edges are removed**.
+
+-/
+
+@[expose] public section
+
+variable {α β ι : Type*} {x y : α} {e : β} {G G₁ G₂ H : Graph α β} {F F₀ : Set β} {X : Set α}
+
+open Set Function
+
+namespace Graph
+
+section iInter
+
+/-- The intersection of a nonempty family of pairwise compatible graphs.
+Remove any non-compatible edges. -/
+@[simps (attr := grind =)]
+protected def iInter [Nonempty ι] (G : ι → Graph α β) : Graph α β where
+  vertexSet := ⋂ i, V(G i)
+  edgeSet := {e | ∃ x y, ∀ i, (G i).IsLink e x y}
+  IsLink e x y := ∀ i, (G i).IsLink e x y
+  isLink_symm e he x y := by simp [isLink_comm]
+  eq_or_eq_of_isLink_of_isLink e _ _ _ _ h h' :=
+    (h (Classical.arbitrary ι)).left_eq_or_eq (h' (Classical.arbitrary ι))
+  edge_mem_iff_exists_isLink e := by simp
+  left_mem_of_isLink e x y h := mem_iInter.2 fun i ↦ (h i).left_mem
+
+protected lemma iInter_le {G : ι → Graph α β} [Nonempty ι] (i : ι) : Graph.iInter G ≤ G i where
+  vertexSet_mono := iInter_subset (fun i ↦ V(G i)) i
+  isLink_mono _ _ _ h := h i
+
+@[simp]
+lemma le_iInter_iff [Nonempty ι] {G : ι → Graph α β} : H ≤ Graph.iInter G ↔ ∀ i, H ≤ G i := by
+  let j := Classical.arbitrary ι
+  refine ⟨fun h i ↦ h.trans <| Graph.iInter_le .., fun h ↦ ?_⟩
+  rw [Compatible.of_le_le (h j) (Graph.iInter_le ..) |>.le_iff]
+  refine ⟨?_, fun e he ↦ ?_⟩
+  · simp [fun i ↦ (h i).vertexSet_mono]
+  simp only [iInter_edgeSet, mem_setOf_eq]
+  obtain ⟨x, y, hbtw⟩ := exists_isLink_of_mem_edgeSet he
+  use x, y, fun i ↦ (h i).isLink_mono hbtw
+
+end iInter
+
+section sInter
+
+/-- The intersection of a nonempty set of pairwise compatible graphs.
+Remove any non-compatible edges. -/
+@[simps! (attr := grind =)]
+protected def sInter (s : Set (Graph α β)) (hne : s.Nonempty) : Graph α β :=
+  @Graph.iInter _ _ _ hne.to_subtype (fun G : s ↦ G.1)
+
+protected lemma sInter_le {Gs : Set (Graph α β)} (hG : G ∈ Gs) : Graph.sInter Gs ⟨G, hG⟩ ≤ G := by
+  rw [Graph.sInter]
+  generalize_proofs h
+  exact Graph.iInter_le (⟨G, hG⟩ : Gs)
+
+@[simp]
+protected lemma le_sInter_iff {Gs : Set (Graph α β)} (hne : Gs.Nonempty) :
+    H ≤ Graph.sInter Gs hne ↔ ∀ G ∈ Gs, H ≤ G := by
+  simp [Graph.sInter]
+
+end sInter
+
+section inter
+
+/-- The intersection of two graphs `G` and `H`. The edges are precisely those on which `G`
+and `H` agree, and the edge set is a subset of `E(G) ∩ E(H)`, with equality if `G` and `H` are
+compatible. -/
+protected def inter (G H : Graph α β) : Graph α β where
+  vertexSet := V(G) ∩ V(H)
+  edgeSet := {e ∈ E(G) ∩ E(H) | ∀ x y, G.IsLink e x y ↔ H.IsLink e x y}
+  IsLink e x y := G.IsLink e x y ∧ H.IsLink e x y
+  isLink_symm _ _ _ _ h := ⟨h.1.symm, h.2.symm⟩
+  eq_or_eq_of_isLink_of_isLink _ _ _ _ _ h h' := h.1.left_eq_or_eq h'.1
+  edge_mem_iff_exists_isLink e := by
+    simp only [edgeSet_eq_setOf_exists_isLink, mem_inter_iff, mem_setOf_eq]
+    exact ⟨fun ⟨⟨⟨x, y, hexy⟩, ⟨z, w, hezw⟩⟩, h⟩ ↦ ⟨x, y, hexy, by rwa [← h]⟩,
+      fun ⟨x, y, hfG, hfH⟩ ↦ ⟨⟨⟨_, _, hfG⟩, ⟨_, _, hfH⟩⟩,
+      fun z w ↦ by rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]⟩⟩
+  left_mem_of_isLink e x y h := ⟨h.1.left_mem, h.2.left_mem⟩
+
+instance : Inter (Graph α β) where inter := Graph.inter
+
+@[simp] lemma inter_vertexSet (G H : Graph α β) : V(G ∩ H) = V(G) ∩ V(H) := rfl
+
+@[simp] lemma inter_isLink_iff : (G ∩ H).IsLink e x y ↔ G.IsLink e x y ∧ H.IsLink e x y := Iff.rfl
+
+lemma inter_edgeSet (G H : Graph α β) :
+    E(G ∩ H) = {e ∈ E(G) ∩ E(H) | ∀ x y, G.IsLink e x y ↔ H.IsLink e x y} := rfl
+
+protected lemma inter_comm (G H : Graph α β) : G ∩ H = H ∩ G :=
+  Graph.ext (Set.inter_comm ..) <| by simp [and_comm]
+
+instance : Std.Commutative (α := Graph α β) (· ∩ ·) where
+  comm G H := Graph.ext (Set.inter_comm ..) <| by simp [and_comm]
+
+protected lemma inter_assoc (G H I : Graph α β) : (G ∩ H) ∩ I = G ∩ (H ∩ I) :=
+  Graph.ext (Set.inter_assoc ..) <| by simp [and_assoc]
+
+instance : Std.Associative (α := Graph α β) (· ∩ ·) where
+  assoc _ _ _ := Graph.ext (Set.inter_assoc ..) <| by simp [and_assoc]
+
+@[simp]
+protected lemma inter_le_left : G ∩ H ≤ G where
+  vertexSet_mono := inter_subset_left
+  isLink_mono := by simp +contextual
+
+@[simp] protected lemma inter_le_right : G ∩ H ≤ H := Graph.inter_comm _ _ ▸ Graph.inter_le_left
+
+protected lemma le_inter (h₁ : H ≤ G₁) (h₂ : H ≤ G₂) : H ≤ G₁ ∩ G₂ where
+  vertexSet_mono := subset_inter h₁.vertexSet_mono h₂.vertexSet_mono
+  isLink_mono e x y h := by simp [h₁.isLink_mono h, h₂.isLink_mono h]
+
+instance : SemilatticeInf (Graph α β) where
+  inf := Graph.inter
+  inf_le_left _ _ := Graph.inter_le_left
+  inf_le_right _ _ := Graph.inter_le_right
+  le_inf _ _ _ := Graph.le_inter
+
+end inter
+
+end Graph