Lindstrom's theorem for set systems

Stream: Is there code for X?

[Strahinja Gvozdić]

Hello! I would like to check if there is already a proof of Lindström's theorem for set systems: given a system of $m$, $m \ge n+1$, subsets $A_1,\dots,A_m$ of $[n]$, there are disjoint subsets of indices $I,J\subset [m]$ such that $\bigcup_{i\in I} A_i = \bigcup_{j\in J} A_j$ .

[Yaël Dillies]

Not that I know of! @Bhavik Mehta ?

[Bhavik Mehta]

This statement looks too weak to be what you want, since you can pick I,J both empty. For the version where I,J are enforced to me nonempty, you also need to assume the A_i are nonempty (or some similar condition). And this version I think I have code for lying around somewhere, which I can find if it'd be useful?

[Strahinja Gvozdić]

You are right, I forgot to add here the nonemptiness conditions (for I,J and A_i). I thought to contribute it, along with the similar result that for $m \ge n+2$, there are such $I,J$ as before and such that the intersections coincide as well. Do you also have the code for the latter?

[Bhavik Mehta]

I don't, but it should be an easy modification to get that one too. I think these would be welcome in mathlib, I just never had time to contribute them myself

[Strahinja Gvozdić]

Great, could you send me the code? I will add the latter theorem and make the PR.

[Bhavik Mehta]

Here you go:

import Mathlib

open Finset Fintype

-- exists in mathlib, but this one is more general, so should replace it
theorem Finset.exists_pos_of_sum_zero_of_exists_nonzero'
    {ι M : Type*} [AddCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] {s : Finset ι}
    (f : ι → M) (h₁ : ∑ i ∈ s, f i = 0) (h₂ : ∃ i ∈ s, f i ≠ 0) :
    ∃ i ∈ s, 0 < f i := by
  obtain ⟨i, hi, hfi⟩ := h₂
  by_contra! h
  have : ¬ ∃ x ∈ s, f x < 0 := by simp [← sum_neg_iff_of_nonpos h, h₁]
  exact this ⟨i, hi, lt_of_le_of_ne (h i hi) hfi⟩

theorem Finset.exists_neg_of_sum_zero_of_exists_nonzero
    {ι M : Type*} [AddCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] {s : Finset ι}
    (f : ι → M) (h₁ : ∑ i ∈ s, f i = 0) (h₂ : ∃ i ∈ s, f i ≠ 0) :
    ∃ i ∈ s, f i < 0 := by
  obtain ⟨i, hi, hfi⟩ := h₂
  by_contra! h
  have : ¬ ∃ x ∈ s, 0 < f x := by simp [← sum_pos_iff_of_nonneg h, h₁]
  exact this ⟨i, hi, lt_of_le_of_ne' (h i hi) hfi⟩

lemma biUnion_eq_empty {α β : Type*} [DecidableEq β] (s : Finset α) (f : α → Finset β) :
    s.biUnion f = ∅ ↔ ∀ a ∈ s, f a = ∅ := by
  grind

lemma biUnion_nonempty {α β : Type*} [DecidableEq β] (s : Finset α) (f : α → Finset β) :
    (s.biUnion f).Nonempty ↔ ∃ a ∈ s, (f a).Nonempty := by
  grind [not_nonempty_iff_eq_empty]

theorem lindstrom {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] (f : α → Finset β)
    (h : card β + 1 ≤ card α) (hf : ∀ i, (f i).Nonempty) :
    ∃ I J : Finset α, Disjoint I J ∧ I.Nonempty ∧ J.Nonempty ∧ I.biUnion f = J.biUnion f := by
  let v (x : α) (y : β) : ℚ := if y ∈ f x then 1 else 0
  have hv : ¬ LinearIndependent ℚ v := by
    intro h
    have : Fintype.card α ≤ Fintype.card β := by simpa using h.fintype_card_le_finrank
    omega
  obtain ⟨c, hc, hci⟩ : ∃ c : α → ℚ, ∑ i, c i • v i = 0 ∧ ∃ i, c i ≠ 0 := by
    simpa [Fintype.linearIndependent_iff] using hv
  let I : Finset α := { i | 0 < c i }
  let J : Finset α := { i | c i < 0 }
  have hij : I.Nonempty ∨ J.Nonempty := by grind [filter_nonempty_iff]
  have h₁ : ∀ a ∈ I, ∀ x ∈ f a, ∃ b ∈ J, x ∈ f b := by
    intro a ha x hx
    have hzero : ∑ i, c i * v i x = 0 := by simpa using congr($hc x)
    have hpos : 0 < c a * v a x := by simpa [v, hx, I] using ha
    obtain ⟨b, -, hb⟩ := exists_neg_of_sum_zero_of_exists_nonzero _ hzero (by grind)
    simp only [mul_ite, v] at hb
    exact ⟨b, by grind⟩
  have h₂ : ∀ b ∈ J, ∀ x ∈ f b, ∃ a ∈ I, x ∈ f a := by
    intro b hb x hx
    have hzero : ∑ i, c i * v i x = 0 := by simpa using congr($hc x)
    have hpos : c b * v b x < 0 := by simpa [v, hx, J] using hb
    obtain ⟨a, -, ha⟩ := exists_pos_of_sum_zero_of_exists_nonzero' _ hzero (by grind)
    simp only [mul_ite, v] at ha
    exact ⟨a, by grind⟩
  have hIJ : I.biUnion f = J.biUnion f := by grind
  have hi : I.Nonempty := by grind [biUnion_empty, biUnion_eq_empty, not_nonempty_iff_eq_empty]
  have hj : J.Nonempty := by grind [biUnion_empty, biUnion_eq_empty, not_nonempty_iff_eq_empty]
  exact ⟨I, J, by grind [disjoint_left]⟩

I took the liberty of updating it to use grind in a few places :)

[Strahinja Gvozdić]

Here's the PR. https://github.com/leanprover-community/mathlib4/pull/30637