CubicPathwidth.FiniteComponents

Source file CubicPathwidth/FiniteComponents.lean of the Lean project (how it is built).

import CubicPathwidth.CorePruning

/-! Finite components expressed by closed induced vertex sets. -/

noncomputable section
namespace CubicPathwidth

variable {n : ℕ} (G : SimpleGraph (Fin n))

def SectionConnected (U : Finset (Fin n)) : Prop :=
  U.Nonempty ∧ ∀ S : Finset (Fin n), S ⊆ U → ClosedIn G U S → S.Nonempty → S = U

theorem closed_sdiff {U S : Finset (Fin n)} (h : ClosedIn G U S) :
    ClosedIn G U (U \ S) := by
  intro v hv w hw hadj
  refine Finset.mem_sdiff.mpr ⟨hw, ?_⟩
  intro hwS
  exact (Finset.mem_sdiff.mp hv).2 (h w hwS v (Finset.mem_sdiff.mp hv).1 hadj.symm)

theorem closed_trans {U S T : Finset (Fin n)} (hS : ClosedIn G U S)
    (hT : ClosedIn G S T) (hTS : T ⊆ S) : ClosedIn G U T := by
  intro v hv w hw hadj
  exact hT v hv w (hS v (hTS hv) w hw hadj) hadj

def component (U : Finset (Fin n)) (v : Fin n) : Finset (Fin n) := by
  classical
  exact U.filter (fun w => v ∈ U ∧
    ∀ S : Finset (Fin n), S ⊆ U → ClosedIn G U S → v ∈ S → w ∈ S)

theorem component_subset (U : Finset (Fin n)) (v : Fin n) : component G U v ⊆ U := by
  classical
  exact Finset.filter_subset _ _

theorem mem_component_self {U : Finset (Fin n)} {v : Fin n} (hv : v ∈ U) :
    v ∈ component G U v := by
  classical
  exact Finset.mem_filter.mpr ⟨hv, hv, fun _ _ _ h => h⟩

theorem component_min {U S : Finset (Fin n)} {v : Fin n}
    (hS : S ⊆ U) (hc : ClosedIn G U S) (hv : v ∈ S) : component G U v ⊆ S := by
  classical
  intro w hw
  exact (Finset.mem_filter.mp hw).2.2 S hS hc hv

theorem component_closed (U : Finset (Fin n)) (v : Fin n) :
    ClosedIn G U (component G U v) := by
  classical
  intro w hw z hz hadj
  obtain ⟨hwU, hvU, hmin⟩ := Finset.mem_filter.mp hw
  exact Finset.mem_filter.mpr ⟨hz, hvU, fun S hS hc hv => hc w (hmin S hS hc hv) z hz hadj⟩

theorem component_eq_of_mem {U : Finset (Fin n)} {v w : Fin n}
    (hw : w ∈ component G U v) : component G U w = component G U v := by
  classical
  have hwU := component_subset G U v hw
  have hvU : v ∈ U := (Finset.mem_filter.mp hw).2.1
  have hsub := component_min G (component_subset G U v) (component_closed G U v) hw
  have hv : v ∈ component G U w := by
    by_contra hnot
    have hcompl := component_min G Finset.sdiff_subset
      (closed_sdiff G (component_closed G U w)) (Finset.mem_sdiff.mpr ⟨hvU, hnot⟩)
    exact (Finset.mem_sdiff.mp (hcompl hw)).2 (mem_component_self G hwU)
  exact Finset.Subset.antisymm hsub
    (component_min G (component_subset G U w) (component_closed G U w) hv)

theorem component_connected {U : Finset (Fin n)} {v : Fin n} (hv : v ∈ U) :
    SectionConnected G (component G U v) := by
  refine ⟨⟨v, mem_component_self G hv⟩, ?_⟩
  intro S hS hc hne
  obtain ⟨w, hw⟩ := hne
  have hclosed := closed_trans G (component_closed G U v) hc hS
  have hmin := component_min G (hS.trans (component_subset G U v)) hclosed hw
  rw [component_eq_of_mem G (hS hw)] at hmin
  exact Finset.Subset.antisymm hS hmin

theorem component_eq_of_connected {U S : Finset (Fin n)} {v : Fin n}
    (hS : S ⊆ U) (hc : ClosedIn G U S) (hconn : SectionConnected G S) (hv : v ∈ S) :
    component G U v = S := by
  have hsub := component_min G hS hc hv
  apply hconn.2 _ hsub
  · intro a ha b hb hab
    exact component_closed G U v a ha b (hS hb) hab
  · exact ⟨v, mem_component_self G (hS hv)⟩

def components (U : Finset (Fin n)) : Finset (Finset (Fin n)) := by
  classical
  exact U.image (component G U)

theorem mem_components {U T : Finset (Fin n)} (hT : T ∈ components G U) :
    T ⊆ U ∧ ClosedIn G U T ∧ SectionConnected G T := by
  classical
  obtain ⟨v, hv, rfl⟩ := Finset.mem_image.mp hT
  exact ⟨component_subset G U v, component_closed G U v, component_connected G hv⟩

theorem components_disjoint {U S T : Finset (Fin n)}
    (hS : S ∈ components G U) (hT : T ∈ components G U) (hne : S ≠ T) : Disjoint S T := by
  classical
  apply Finset.disjoint_left.mpr
  intro v hvS hvT
  obtain ⟨hs, hsc, hsn⟩ := mem_components G hS
  obtain ⟨ht, htc, htn⟩ := mem_components G hT
  exact hne ((component_eq_of_connected G hs hsc hsn hvS).symm.trans
    (component_eq_of_connected G ht htc htn hvT))

theorem components_cover (U : Finset (Fin n)) : (components G U).biUnion id = U := by
  classical
  ext v
  constructor
  · intro hv
    obtain ⟨T, hT, hvT⟩ := Finset.mem_biUnion.mp hv
    exact (mem_components G hT).1 hvT
  · intro hv
    exact Finset.mem_biUnion.mpr ⟨component G U v,
      Finset.mem_image.mpr ⟨v, hv, rfl⟩, mem_component_self G hv⟩

theorem sum_component_cards (U : Finset (Fin n)) :
    ∑ T ∈ components G U, T.card = U.card := by
  classical
  rw [← components_cover G U]
  rw [Finset.card_biUnion]
  · rw [components_cover]
    rfl
  · intro S hS T hT hne
    exact components_disjoint G hS hT hne

/-- A connected section cannot straddle a closed cut. -/
theorem connected_subset_or_disjoint {U S T : Finset (Fin n)}
    (hT : T ⊆ U) (hconn : SectionConnected G T) (hc : ClosedIn G U S) :
    T ⊆ S ∨ Disjoint T S := by
  classical
  by_cases he : (T ∩ S).Nonempty
  · left
    have ht : T ∩ S = T := hconn.2 _ Finset.inter_subset_left (by
      intro v hv w hw hadj
      exact Finset.mem_inter.mpr ⟨hw, hc v (Finset.mem_inter.mp hv).2 w (hT hw) hadj⟩) he
    rw [← ht]
    exact Finset.inter_subset_right
  · right
    exact Finset.disjoint_iff_inter_eq_empty.mpr (Finset.not_nonempty_iff_eq_empty.mp he)

theorem connected_cross_edge {U S : Finset (Fin n)} (h : SectionConnected G U)
    (hS : S ⊆ U) (hne : S.Nonempty) (hproper : S ≠ U) :
    ∃ u ∈ S, ∃ v ∈ U \ S, G.Adj u v := by
  classical
  by_contra hn
  apply hproper
  apply h.2 S hS _ hne
  intro u hu v hv hadj
  by_contra hvS
  exact hn ⟨u, hu, v, Finset.mem_sdiff.mpr ⟨hv, hvS⟩, hadj⟩

end CubicPathwidth
Back to top