Lattice.lean

/-
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.Order.ConditionallyCompletePartialOrder.Basic
public import Mathlib.Order.CompleteLattice.Basic
public import Mathlib.Combinatorics.Graph.Subgraph

/-!
# Intersection and union of graphs

This file defines the lattice-like structures on graphs.

## Main results

- `CompleteSemilatticeInf (WithTop (Graph α β))`
- `ConditionallyCompletePartialOrderInf (Graph α β)`
- `SemilatticeInf (Graph α β)`

## 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

namespace WithTop

noncomputable instance : CompleteSemilatticeInf (WithTop (Graph α β)) where
  sInf Gs :=
    letI : DecidablePred (Set.Nonempty : Set (Graph α β) → _) := Classical.decPred _
    if hne : (WithTop.some ⁻¹' Gs).Nonempty then ({
    vertexSet := ⋂ G ∈ WithTop.some ⁻¹' Gs, V(G)
    edgeSet := {e | ∃ x y, ∀ G ∈ WithTop.some ⁻¹' Gs, G.IsLink e x y}
    IsLink e x y := ∀ G ∈ WithTop.some ⁻¹' Gs, G.IsLink e x y
    isLink_symm e he x y := by simp [isLink_comm]
    eq_or_eq_of_isLink_of_isLink e _ _ _ _ h h' := by
      obtain ⟨G, hG⟩ := hne
      exact (h G hG).left_eq_or_eq (h' G hG)
    left_mem_of_isLink e x y h := by
      simp only [mem_preimage, mem_iInter]
      exact fun G hG ↦ (h G hG).left_mem} : Graph α β) else ⊤
  isGLB_sInf Gs := by
    refine ⟨fun G hG => ?_, fun H hH => ?_⟩
    · obtain rfl | htop := eq_or_ne G ⊤
      · exact le_top
      lift G to Graph α β using htop
      have hGs : (WithTop.some ⁻¹' Gs).Nonempty := ⟨G, by simpa⟩
      simp only [hGs, ↓reduceDIte, WithTop.coe_le_coe, ge_iff_le]
      refine ⟨fun _ ↦ ?_, fun _ _ _ ↦ ?_⟩ <;> simp only [mem_preimage, mem_iInter]
        <;> exact (· G hG)
    obtain rfl | htop := eq_or_ne H ⊤
    · suffices ¬ (WithTop.some ⁻¹' Gs).Nonempty by simp [this]
      simp only [not_nonempty_iff_eq_empty, preimage_eq_empty_iff, disjoint_right, mem_range,
        forall_exists_index, forall_apply_eq_imp_iff]
      exact fun _ hHs => Option.some_ne_none _ (top_le_iff.mp <| hH hHs)
    lift H to Graph α β using htop
    split_ifs with hne
    · rw [WithTop.coe_le_coe]
      exact { vertexSet_mono := by
                simp only [subset_iInter_iff]
                exact fun G hG ↦ (WithTop.coe_le_coe.mp <| hH hG).vertexSet_mono
              isLink_mono e x y hHxy G hG := (WithTop.coe_le_coe.mp <| hH hG).isLink_mono hHxy}
    exact le_top

lemma sInf_eq_top_iff (Gs : Set (WithTop (Graph α β))) : sInf Gs = ⊤ ↔ Gs ⊆ {⊤} := by
  classical
  refine ⟨fun h G hG => ?_, fun h => ?_⟩
  · exact WithTop.top_le_iff.mp (h ▸ sInf_le hG)
  obtain rfl | rfl := subset_singleton_iff_eq.mp h
  · exact isGLB_empty.sInf_eq
  exact sInf_singleton

lemma sInf_coe_eq_top_iff (Gs : Set (Graph α β)) : sInf (WithTop.some '' Gs) = ⊤ ↔ Gs = ∅ := by
  rw [sInf_eq_top_iff, subset_singleton_iff_eq, image_eq_empty, or_iff_left_iff_imp]
  rintro h
  simpa using (show ⊤ ∈ WithTop.some '' Gs from h ▸ rfl)

end WithTop

noncomputable instance : ConditionallyCompletePartialOrderInf (Graph α β) where
  sInf Gs :=
    letI : DecidablePred (Set.Nonempty : Set (Graph α β) → _) := Classical.decPred _
    sInf (WithTop.some '' Gs) |>.untopD ⊥
  isGLB_csInf_of_directed Gs hGs hGsne hGsBddB := by
    classical
    refine ⟨fun G hG => (WithTop.untopD_le <| sInf_le (by simpa)), fun H hH => ?_⟩
    change H ≤ (WithTop.untopD ⊥ (if hne : Set.Nonempty _ then _ else _))
    simp only [WithTop.coe_injective, preimage_image_eq, hGsne, ↓reduceDIte, WithTop.untopD_coe]
    exact { vertexSet_mono := by
              simp only [subset_iInter_iff]
              exact fun _ hG ↦ (hH hG).vertexSet_mono
            isLink_mono e x y hHxy G hG := (hH hG).isLink_mono hHxy}

lemma isGLB_sInf_of_nonempty {Gs : Set (Graph α β)} (hGsne : Gs.Nonempty) : IsGLB Gs (sInf Gs) := by
  classical
  refine ⟨fun G hG => (WithTop.untopD_le <| sInf_le (by simpa)), fun H hH => ?_⟩
  change H ≤ (WithTop.untopD ⊥ (if hne : Set.Nonempty _ then _ else _))
  simp only [WithTop.coe_injective, preimage_image_eq, hGsne, ↓reduceDIte, WithTop.untopD_coe]
  exact { vertexSet_mono := by
            simp only [subset_iInter_iff]
            exact fun _ hG ↦ (hH hG).vertexSet_mono
          isLink_mono e x y hHxy G hG := (hH hG).isLink_mono hHxy}

@[grind =]
lemma vertexSet_sInf_eq_ite (Gs : Set (Graph α β)) [Decidable Gs.Nonempty] :
    V(sInf Gs) = if Gs.Nonempty then ⋂ G ∈ Gs, V(G) else ∅ := by
  simp only [sInf, WithTop.coe_injective.preimage_image]
  split_ifs with hne <;> rfl

@[simp]
lemma vertexSet_sInf_of_nonempty {Gs : Set (Graph α β)} (hGsne : Gs.Nonempty) :
    V(sInf Gs) = ⋂ G ∈ Gs, V(G) := by
  classical
  grind

@[grind =]
lemma edgeSet_sInf_eq_ite (Gs : Set (Graph α β)) [Decidable Gs.Nonempty] :
    E(sInf Gs) = if Gs.Nonempty then {e | ∃ x y, ∀ G ∈ Gs, G.IsLink e x y} else ∅ := by
  simp only [sInf, WithTop.coe_injective.preimage_image]
  split_ifs with hne <;> rfl

@[simp]
lemma edgeSet_sInf_of_nonempty {Gs : Set (Graph α β)} (hGsne : Gs.Nonempty) :
    E(sInf Gs) = {e | ∃ x y, ∀ G ∈ Gs, G.IsLink e x y} := by
  classical
  grind

@[grind =]
lemma sInf_isLink (Gs : Set (Graph α β)) [Decidable Gs.Nonempty] :
    (sInf Gs).IsLink e x y ↔ if Gs.Nonempty then ∀ G ∈ Gs, G.IsLink e x y else False := by
  simp only [sInf, WithTop.coe_injective.preimage_image]
  split_ifs with hne <;> rfl

@[simp]
lemma sInf_isLink_of_nonempty {Gs : Set (Graph α β)} (hGsne : Gs.Nonempty) :
    (sInf Gs).IsLink e x y ↔ ∀ G ∈ Gs, G.IsLink e x y := by
  classical
  grind

/-- The infimum 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. -/
instance : SemilatticeInf (Graph α β) where
  inf G H := {
    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⟩}
  inf_le_left G H := {
    vertexSet_mono := inter_subset_left
    isLink_mono := by simp +contextual}
  inf_le_right G H := {
    vertexSet_mono := inter_subset_right
    isLink_mono := by simp +contextual}
  le_inf H G₁ G₂ h₁ h₂ := {
    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]}

@[simp] lemma inf_vertexSet (G H : Graph α β) : V(G ⊓ H) = V(G) ∩ V(H) := rfl

lemma inf_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

@[simp] lemma inf_isLink_iff : (G ⊓ H).IsLink e x y ↔ G.IsLink e x y ∧ H.IsLink e x y := Iff.rfl

@[simp] lemma sInf_pair (G H : Graph α β) : sInf {G, H} = G ⊓ H := by ext <;> simp

end Graph