CubicPathwidth.CoreTorso

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

import CubicPathwidth.CorePieces
import CubicPathwidth.Relabelling

/-! A simple subcubic torso on the retained branch vertices. -/

noncomputable section
namespace CubicPathwidth
open SectionDecomposition
variable {n : ℕ} (G : SimpleGraph (Fin n))

def coreTorso (F B : Finset (Fin n)) : SimpleGraph (Fin B.card) where
  Adj i j := i ≠ j ∧ (G.Adj (enumerate B i) (enumerate B j) ∨
    ∃ T ∈ components G (F \ B),
      enumerate B i ∈ attachment G B T ∧ enumerate B j ∈ attachment G B T)
  symm := ⟨by
    intro i j h
    refine ⟨h.1.symm, ?_⟩
    rcases h.2 with h | ⟨T, hT, hi, hj⟩
    · exact Or.inl h.symm
    · exact Or.inr ⟨T, hT, hj, hi⟩⟩
  loopless := ⟨fun i h => h.1 rfl⟩

theorem two_attachment_unique {A : Finset (Fin n)} (hA : A.card ≤ 2)
    {x y z : Fin n} (hx : x ∈ A) (hy : y ∈ A) (hz : z ∈ A)
    (hxy : x ≠ y) (hxz : x ≠ z) : y = z := by
  have hc : (A.erase x).card ≤ 1 := by
    have := Finset.card_erase_add_one hx
    omega
  exact (Finset.card_le_one.mp hc) y
    (Finset.mem_erase.mpr ⟨hxy.symm, hy⟩) z (Finset.mem_erase.mpr ⟨hxz.symm, hz⟩)

/-- A torso edge can be charged to a neighbour in the original graph. -/
theorem torso_edge_witness {F B : Finset (Fin n)} {i j : Fin B.card}
    (h : (coreTorso G F B).Adj i j) :
    ∃ w, G.Adj (enumerate B i) w ∧
      (w = enumerate B j ∨ ∃ T ∈ components G (F \ B),
        w ∈ T ∧ enumerate B i ∈ attachment G B T ∧ enumerate B j ∈ attachment G B T) := by
  rcases h.2 with h | ⟨T, hT, hi, hj⟩
  · exact ⟨enumerate B j, h, Or.inl rfl⟩
  · obtain ⟨_, w, hw, hiw⟩ := (mem_attachment G).mp hi
    exact ⟨w, hiw, Or.inr ⟨T, hT, hw, hi, hj⟩⟩

theorem coreTorso_subcubic (hG : IsSubcubic G) (F B : Finset (Fin n))
    (hattach : ∀ T ∈ components G (F \ B), (attachment G B T).card ≤ 2) :
    IsSubcubic (coreTorso G F B) := by
  classical
  let K := coreTorso G F B
  intro i
  have hw : ∀ j : K.neighborFinset i, ∃ w : G.neighborFinset (enumerate B i),
      ((w : Fin n) = enumerate B j ∨ ∃ T ∈ components G (F \ B),
        (w : Fin n) ∈ T ∧ enumerate B i ∈ attachment G B T ∧
          enumerate B j ∈ attachment G B T) := by
    intro j
    obtain ⟨w, hadj, hr⟩ := torso_edge_witness G ((K.mem_neighborFinset _ _).mp j.property)
    exact ⟨⟨w, (G.mem_neighborFinset _ _).mpr hadj⟩, hr⟩
  choose f hf using hw
  have hinj : Function.Injective f := by
    intro j k he
    have hwval := congrArg Subtype.val he
    have hij : enumerate B i ≠ enumerate B j :=
      fun h => ((K.mem_neighborFinset _ _).mp j.property).1 ((enumerate B).injective h)
    have hik : enumerate B i ≠ enumerate B k :=
      fun h => ((K.mem_neighborFinset _ _).mp k.property).1 ((enumerate B).injective h)
    apply Subtype.ext
    apply (enumerate B).injective
    rcases hf j with hj | ⟨S, hS, hwS, hiS, hjS⟩ <;>
      rcases hf k with hk | ⟨T, hT, hwT, hiT, hkT⟩
    · exact hj.symm.trans (hwval.trans hk)
    · have hwB : (f k : Fin n) ∈ B := by
        rw [← hwval, hj]
        exact (mem_iff_enumerate B _).mpr ⟨j, rfl⟩
      exact False.elim ((Finset.mem_sdiff.mp ((mem_components G hT).1 hwT)).2 hwB)
    · have hwB : (f j : Fin n) ∈ B := by
        rw [hwval, hk]
        exact (mem_iff_enumerate B _).mpr ⟨k, rfl⟩
      exact False.elim ((Finset.mem_sdiff.mp ((mem_components G hS).1 hwS)).2 hwB)
    · have hST : S = T := by
        by_contra hne
        exact Finset.disjoint_left.mp (components_disjoint G hS hT hne) hwS (hwval.symm ▸ hwT)
      subst T
      exact two_attachment_unique (hattach S hS) hiS hjS hkT hij hik
  have hc := Fintype.card_le_of_injective f hinj
  have hc' : (K.neighborFinset i).card ≤ (G.neighborFinset (enumerate B i)).card := by
    simpa only [Fintype.card_coe] using hc
  exact hc'.trans (hG _)

/-- Lift any torso decomposition, retaining exact images of its bags. -/
def liftTorso (F B : Finset (Fin n)) (D : PathDecomposition (coreTorso G F B)) :
    SectionDecomposition G B := by
  classical
  let E : PathDecomposition (inducedOnFin G B) := {
    lastIndex := D.lastIndex
    bag := D.bag
    vertex_covered := D.vertex_covered
    edge_covered := by
      intro i j hij
      exact D.edge_covered i j ⟨by intro he; subst j; exact G.irrefl hij, Or.inl hij⟩
    interval := D.interval }
  exact lift G B E

theorem liftTorso_width (F B : Finset (Fin n)) (D : PathDecomposition (coreTorso G F B))
    {p : ℝ} (hD : D.WidthAtMost p) : (liftTorso G F B D).toBagPath.WidthAtMost p :=
  lift_width G B _ hD

theorem liftTorso_bag (F B : Finset (Fin n)) (D : PathDecomposition (coreTorso G F B))
    (i : Fin (D.lastIndex + 1)) :
    (liftTorso G F B D).bag i.val = (D.bag i).image (enumerate B) := by
  classical
  have hi : i.val ≤ D.lastIndex := by have := i.isLt; omega
  simp [liftTorso, lift, restrict, hi]

/-- Each attachment, including an empty or singleton attachment, fits in one
original torso bag. -/
theorem torso_attachment_bag (F B : Finset (Fin n))
    (D : PathDecomposition (coreTorso G F B)) {T : Finset (Fin n)}
    (hT : T ∈ components G (F \ B)) (hc : (attachment G B T).card ≤ 2) :
    ∃ i, i ≤ (liftTorso G F B D).lastIndex ∧
      attachment G B T ⊆ (liftTorso G F B D).bag i := by
  classical
  let A := attachment G B T
  by_cases hne : A.Nonempty
  · obtain ⟨x, hx⟩ := hne
    obtain ⟨a, ha⟩ := (mem_iff_enumerate B x).mp (attachment_subset G B T hx)
    by_cases he : (A.erase x).Nonempty
    · obtain ⟨y, hy⟩ := he
      obtain ⟨hyx, hyA⟩ := Finset.mem_erase.mp hy
      obtain ⟨b, hb⟩ := (mem_iff_enumerate B y).mp (attachment_subset G B T hyA)
      have hab : (coreTorso G F B).Adj a b :=
        ⟨by intro h; subst b; exact hyx (hb.symm.trans ha), Or.inr ⟨T, hT, ha.symm ▸ hx, hb.symm ▸ hyA⟩⟩
      obtain ⟨i, hai, hbi⟩ := D.edge_covered a b hab
      refine ⟨i.val, by change i.val ≤ D.lastIndex; have := i.isLt; omega, ?_⟩
      rw [liftTorso_bag]
      intro z hz
      by_cases hzx : z = x
      · exact Finset.mem_image.mpr ⟨a, hai, ha.trans hzx.symm⟩
      · have hzy : z = y := two_attachment_unique hc hx hz hyA (Ne.symm hzx) hyx.symm
        exact Finset.mem_image.mpr ⟨b, hbi, hb.trans hzy.symm⟩
    · obtain ⟨i, hai⟩ := D.vertex_covered a
      refine ⟨i.val, by change i.val ≤ D.lastIndex; have := i.isLt; omega, ?_⟩
      rw [liftTorso_bag]
      intro z hz
      have hzx : z = x := by
        by_contra h
        exact he ⟨z, Finset.mem_erase.mpr ⟨h, hz⟩⟩
      exact Finset.mem_image.mpr ⟨a, hai, ha.trans hzx.symm⟩
  · refine ⟨0, Nat.zero_le _, ?_⟩
    have he : attachment G B T = ∅ := Finset.not_nonempty_iff_eq_empty.mp hne
    rw [he]
    exact Finset.empty_subset _

end CubicPathwidth