feat(order/sup_indep): More lemmas (#11932)

YaelDillies · YaelDillies · commit c4c2ed622f43 · 2023-06-16T08:34:16.000Z
A few more lemmas about `finset.sup_indep` and `set.pairwise_disjoint`.
diff --git a/src/data/finset/pairwise.lean b/src/data/finset/pairwise.lean
@@ -39,15 +39,23 @@ lemma pairwise_disjoint.elim_finset {s : set ι} {f : ι → finset α}
   i = j :=
 hs.elim hi hj (finset.not_disjoint_iff.2 ⟨a, hai, haj⟩)
 
-lemma pairwise_disjoint.image_finset_of_le [decidable_eq ι] [semilattice_inf α] [order_bot α]
-  {s : finset ι} {f : ι → α} (hs : (s : set ι).pairwise_disjoint f) {g : ι → ι}
-  (hf : ∀ a, f (g a) ≤ f a) :
+section semilattice_inf
+variables [semilattice_inf α] [order_bot α] {s : finset ι} {f : ι → α}
+
+lemma pairwise_disjoint.image_finset_of_le [decidable_eq ι] {s : finset ι} {f : ι → α}
+  (hs : (s : set ι).pairwise_disjoint f) {g : ι → ι} (hf : ∀ a, f (g a) ≤ f a) :
   (s.image g : set ι).pairwise_disjoint f :=
 begin
   rw coe_image,
   exact hs.image_of_le hf,
 end
 
+lemma pairwise_disjoint.attach (hs : (s : set ι).pairwise_disjoint f) :
+  (s.attach : set {x // x ∈ s}).pairwise_disjoint (f ∘ subtype.val) :=
+λ i _ j _ hij, hs i.2 j.2 $ mt subtype.ext_val hij
+
+end semilattice_inf
+
 variables [lattice α] [order_bot α]
 
 /-- Bind operation for `set.pairwise_disjoint`. In a complete lattice, you can use
diff --git a/src/data/set/pairwise/basic.lean b/src/data/set/pairwise/basic.lean
@@ -30,7 +30,7 @@ The spelling `s.pairwise_disjoint id` is preferred over `s.pairwise disjoint` to
 on `set.pairwise_disjoint`, even though the latter unfolds to something nicer.
 -/
 
-open set function
+open function order set
 
 variables {α β γ ι ι' : Type*} {r p q : α → α → Prop}
 
@@ -296,6 +296,8 @@ end semilattice_inf_bot
 
 /-! ### Pairwise disjoint set of sets -/
 
+variables {s : set ι} {t : set ι'}
+
 lemma pairwise_disjoint_range_singleton :
   (set.range (singleton : ι → set ι)).pairwise_disjoint id :=
 begin
@@ -311,6 +313,18 @@ lemma pairwise_disjoint.elim_set {s : set ι} {f : ι → set α} (hs : s.pairwi
   (hi : i ∈ s) (hj : j ∈ s) (a : α) (hai : a ∈ f i) (haj : a ∈ f j) : i = j :=
 hs.elim hi hj $ not_disjoint_iff.2 ⟨a, hai, haj⟩
 
+lemma pairwise_disjoint.prod {f : ι → set α} {g : ι' → set β} (hs : s.pairwise_disjoint f)
+  (ht : t.pairwise_disjoint g) :
+  (s ×ˢ t : set (ι × ι')).pairwise_disjoint (λ i, f i.1 ×ˢ g i.2) :=
+λ ⟨i, i'⟩ ⟨hi, hi'⟩ ⟨j, j'⟩ ⟨hj, hj'⟩ hij, disjoint_left.2 $ λ ⟨a, b⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩,
+  hij $ prod.ext (hs.elim_set hi hj _ hai haj) $ ht.elim_set hi' hj' _ hbi hbj
+
+lemma pairwise_disjoint_pi {ι' α : ι → Type*} {s : Π i, set (ι' i)} {f : Π i, ι' i → set (α i)}
+  (hs : ∀ i, (s i).pairwise_disjoint (f i)) :
+  ((univ : set ι).pi s).pairwise_disjoint (λ I, (univ : set ι).pi (λ i, f _ (I i))) :=
+λ I hI J hJ hIJ, disjoint_left.2 $ λ a haI haJ, hIJ $ funext $ λ i,
+  (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial)
+
 /-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
 disjoint iff `f` is injective . -/
 lemma pairwise_disjoint_image_right_iff {f : α → β → γ} {s : set α} {t : set β}
diff --git a/src/data/set/pairwise/lattice.lean b/src/data/set/pairwise/lattice.lean
@@ -15,16 +15,16 @@ import data.set.pairwise.basic
 In this file we prove many facts about `pairwise` and the set lattice.
 -/
 
-open set function
+open function set order
 
-variables {α β γ ι ι' : Type*} {r p q : α → α → Prop}
+variables {α β γ ι ι' : Type*} {κ : Sort*} {r p q : α → α → Prop}
 
 section pairwise
 variables {f g : ι → α} {s t u : set α} {a b : α}
 
 namespace set
 
-lemma pairwise_Union {f : ι → set α} (h : directed (⊆) f) :
+lemma pairwise_Union {f : κ → set α} (h : directed (⊆) f) :
   (⋃ n, f n).pairwise r ↔ ∀ n, (f n).pairwise r :=
 begin
   split,
@@ -60,7 +60,7 @@ pairwise_sUnion h
 end partial_order_bot
 
 section complete_lattice
-variables [complete_lattice α]
+variables [complete_lattice α] {s : set ι} {t : set ι'}
 
 /-- Bind operation for `set.pairwise_disjoint`. If you want to only consider finsets of indices, you
 can use `set.pairwise_disjoint.bUnion_finset`. -/
@@ -78,8 +78,41 @@ begin
   { exact (hs hc hd $ ne_of_apply_ne _ hcd).mono (le_supr₂ a ha) (le_supr₂ b hb) }
 end
 
+/-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
+pairwise disjoint. Not to be confused with `set.pairwise_disjoint.prod`. -/
+lemma pairwise_disjoint.prod_left {f : ι × ι' → α}
+  (hs : s.pairwise_disjoint $ λ i, ⨆ i' ∈ t, f (i, i'))
+  (ht : t.pairwise_disjoint $ λ i', ⨆ i ∈ s, f (i, i')) :
+  (s ×ˢ t : set (ι × ι')).pairwise_disjoint f :=
+begin
+  rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h,
+  rw mem_prod at hi hj,
+  obtain rfl | hij := eq_or_ne i j,
+  { refine (ht hi.2 hj.2 $ (prod.mk.inj_left _).ne_iff.1 h).mono _ _,
+    { convert le_supr₂ i hi.1, refl },
+    { convert le_supr₂ i hj.1, refl } },
+  { refine (hs hi.1 hj.1 hij).mono _ _,
+    { convert le_supr₂ i' hi.2, refl },
+    { convert le_supr₂ j' hj.2, refl } }
+end
+
 end complete_lattice
 
+section frame
+variables [frame α]
+
+lemma pairwise_disjoint_prod_left {s : set ι} {t : set ι'} {f : ι × ι' → α} :
+  (s ×ˢ t : set (ι × ι')).pairwise_disjoint f ↔ s.pairwise_disjoint (λ i, ⨆ i' ∈ t, f (i, i')) ∧
+    t.pairwise_disjoint (λ i', ⨆ i ∈ s, f (i, i')) :=
+begin
+  refine (⟨λ h, ⟨λ i hi j hj hij, _, λ i hi j hj hij, _⟩, λ h, h.1.prod_left h.2⟩);
+    simp_rw [function.on_fun, supr_disjoint_iff, disjoint_supr_iff]; intros i' hi' j' hj',
+  { exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne prod.fst hij) },
+  { exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne prod.snd hij) }
+end
+
+end frame
+
 lemma bUnion_diff_bUnion_eq {s t : set ι} {f : ι → set α} (h : (s ∪ t).pairwise_disjoint f) :
   (⋃ i ∈ s, f i) \ (⋃ i ∈ t, f i) = (⋃ i ∈ s \ t, f i) :=
 begin
diff --git a/src/data/set/prod.lean b/src/data/set/prod.lean
@@ -106,13 +106,21 @@ by { ext ⟨x, y⟩, simp only [←and_and_distrib_left, mem_inter_iff, mem_prod
 lemma prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) :=
 by { ext ⟨x, y⟩, simp [and_assoc, and.left_comm] }
 
-lemma disjoint_prod : disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ disjoint s₁ s₂ ∨ disjoint t₁ t₂ :=
+@[simp] lemma disjoint_prod : disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ disjoint s₁ s₂ ∨ disjoint t₁ t₂ :=
 begin
   simp_rw [disjoint_left, mem_prod, not_and_distrib, prod.forall, and_imp,
     ←@forall_or_distrib_right α, ←@forall_or_distrib_left β,
     ←@forall_or_distrib_right (_ ∈ s₁), ←@forall_or_distrib_left (_ ∈ t₁)],
 end
 
+lemma _root_.disjoint.set_prod_left (hs : disjoint s₁ s₂) (t₁ t₂ : set β) :
+  disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
+disjoint_left.2 $ λ ⟨a, b⟩ ⟨ha₁, hb₁⟩ ⟨ha₂, hb₂⟩, disjoint_left.1 hs ha₁ ha₂
+
+lemma _root_.disjoint.set_prod_right (ht : disjoint t₁ t₂) (s₁ s₂ : set α) :
+  disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
+disjoint_left.2 $ λ ⟨a, b⟩ ⟨ha₁, hb₁⟩ ⟨ha₂, hb₂⟩, disjoint_left.1 ht hb₁ hb₂
+
 lemma insert_prod : insert a s ×ˢ t = (prod.mk a '' t) ∪ s ×ˢ t :=
 by { ext ⟨x, y⟩, simp [image, iff_def, or_imp_distrib, imp.swap] {contextual := tt} }
 
@@ -479,6 +487,20 @@ univ_pi_eq_empty_iff.2 $ h.elim $ λ x, ⟨x, rfl⟩
 @[simp] lemma disjoint_univ_pi : disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, disjoint (t₁ i) (t₂ i) :=
 by simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]
 
+lemma _root_.disjoint.set_pi (hi : i ∈ s) (ht : disjoint (t₁ i) (t₂ i)) :
+  disjoint (s.pi t₁) (s.pi t₂) :=
+disjoint_left.2 $ λ h h₁ h₂, disjoint_left.1 ht (h₁ _ hi) (h₂ _ hi)
+
+section nonempty
+variables [Π i, nonempty (α i)]
+
+lemma pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [pi_eq_empty_iff]
+
+@[simp] lemma disjoint_pi : disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, disjoint (t₁ i) (t₂ i) :=
+by simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']
+
+end nonempty
+
 @[simp] lemma range_dcomp (f : Π i, α i → β i) :
   range (λ (g : Π i, α i), (λ i, f i (g i))) = pi univ (λ i, range (f i)) :=
 begin
diff --git a/src/order/sup_indep.lean b/src/order/sup_indep.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Aaron Anderson, Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Kevin Buzzard, Yaël Dillies, Eric Wieser
 -/
+import data.finset.sigma
 import data.finset.pairwise
 import data.finset.powerset
 import data.fintype.basic
@@ -77,12 +78,45 @@ end
 lemma sup_indep.pairwise_disjoint (hs : s.sup_indep f) : (s : set ι).pairwise_disjoint f :=
 λ a ha b hb hab, sup_singleton.subst $ hs (singleton_subset_iff.2 hb) ha $ not_mem_singleton.2 hab
 
+lemma sup_indep.le_sup_iff (hs : s.sup_indep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) :
+  f i ≤ t.sup f ↔ i ∈ t :=
+begin
+  refine ⟨λ h, _, le_sup⟩,
+  by_contra hit,
+  exact hf i (disjoint_self.1 $ (hs hts hi hit).mono_right h),
+end
+
 /-- The RHS looks like the definition of `complete_lattice.independent`. -/
 lemma sup_indep_iff_disjoint_erase [decidable_eq ι] :
   s.sup_indep f ↔ ∀ i ∈ s, disjoint (f i) ((s.erase i).sup f) :=
 ⟨λ hs i hi, hs (erase_subset _ _) hi (not_mem_erase _ _), λ hs t ht i hi hit,
   (hs i hi).mono_right (sup_mono $ λ j hj, mem_erase.2 ⟨ne_of_mem_of_not_mem hj hit, ht hj⟩)⟩
 
+lemma sup_indep.image [decidable_eq ι] {s : finset ι'} {g : ι' → ι} (hs : s.sup_indep (f ∘ g)) :
+  (s.image g).sup_indep f :=
+begin
+  intros t ht i hi hit,
+  rw mem_image at hi,
+  obtain ⟨i, hi, rfl⟩ := hi,
+  haveI : decidable_eq ι' := classical.dec_eq _,
+  suffices hts : t ⊆ (s.erase i).image g,
+  { refine (sup_indep_iff_disjoint_erase.1 hs i hi).mono_right ((sup_mono hts).trans _),
+    rw sup_image },
+  rintro j hjt,
+  obtain ⟨j, hj, rfl⟩ := mem_image.1 (ht hjt),
+  exact mem_image_of_mem _ (mem_erase.2 ⟨ne_of_apply_ne g (ne_of_mem_of_not_mem hjt hit), hj⟩),
+end
+
+lemma sup_indep_map {s : finset ι'} {g : ι' ↪ ι} : (s.map g).sup_indep f ↔ s.sup_indep (f ∘ g) :=
+begin
+  refine ⟨λ hs t ht i hi hit, _, λ hs, _⟩,
+  { rw ←sup_map,
+    exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa mem_map') },
+  { classical,
+    rw map_eq_image,
+    exact hs.image }
+end
+
 @[simp] lemma sup_indep_pair [decidable_eq ι] {i j : ι} (hij : i ≠ j) :
   ({i, j} : finset ι).sup_indep f ↔ disjoint (f i) (f j) :=
 ⟨λ h, h.pairwise_disjoint (by simp) (by simp) hij, λ h, begin
@@ -117,7 +151,7 @@ begin
   exact sup_indep_pair this,
 end
 
-lemma sup_indep.attach (hs : s.sup_indep f) : s.attach.sup_indep (f ∘ subtype.val) :=
+lemma sup_indep.attach (hs : s.sup_indep f) : s.attach.sup_indep (λ a, f a) :=
 begin
   intros t ht i _ hi,
   classical,
@@ -128,6 +162,18 @@ begin
   rwa subtype.ext hji at hj,
 end
 
+@[simp] lemma sup_indep_attach : s.attach.sup_indep (λ a, f a) ↔ s.sup_indep f :=
+begin
+  refine ⟨λ h t ht i his hit, _, sup_indep.attach⟩,
+  classical,
+  convert h (filter_subset (λ i, (i : ι) ∈ t) _) (mem_attach _ ⟨i, ‹_›⟩)
+    (λ hi, hit $ by simpa using hi) using 1,
+  refine eq_of_forall_ge_iff _,
+  simp only [finset.sup_le_iff, mem_filter, mem_attach, true_and, function.comp_app, subtype.forall,
+    subtype.coe_mk],
+  exact λ a, forall_congr (λ j, ⟨λ h _, h, λ h hj, h (ht hj) hj⟩),
+end
+
 end lattice
 
 section distrib_lattice
@@ -156,6 +202,58 @@ lemma sup_indep.bUnion [decidable_eq ι] {s : finset ι'} {g : ι' → finset ι
   (s.bUnion g).sup_indep f :=
 by { rw ←sup_eq_bUnion, exact hs.sup hg }
 
+/-- Bind operation for `sup_indep`. -/
+lemma sup_indep.sigma {β : ι → Type*} {s : finset ι} {g : Π i, finset (β i)} {f : sigma β → α}
+  (hs : s.sup_indep $ λ i, (g i).sup $ λ b, f ⟨i, b⟩)
+  (hg : ∀ i ∈ s, (g i).sup_indep $ λ b, f ⟨i, b⟩) :
+  (s.sigma g).sup_indep f :=
+begin
+  rintro t ht ⟨i, b⟩ hi hit,
+  rw finset.disjoint_sup_right,
+  rintro ⟨j, c⟩ hj,
+  have hbc := (ne_of_mem_of_not_mem hj hit).symm,
+  replace hj := ht hj,
+  rw mem_sigma at hi hj,
+  obtain rfl | hij := eq_or_ne i j,
+  { exact (hg _ hj.1).pairwise_disjoint hi.2 hj.2 (sigma_mk_injective.ne_iff.1 hbc) },
+  { refine (hs.pairwise_disjoint hi.1 hj.1 hij).mono _ _,
+    { convert le_sup hi.2 },
+    { convert le_sup hj.2 } }
+end
+
+lemma sup_indep.product {s : finset ι} {t : finset ι'} {f : ι × ι' → α}
+  (hs : s.sup_indep $ λ i, t.sup $ λ i', f (i, i'))
+  (ht : t.sup_indep $ λ i', s.sup $ λ i, f (i, i')) :
+  (s.product t).sup_indep f :=
+begin
+  rintro u hu ⟨i, i'⟩ hi hiu,
+  rw finset.disjoint_sup_right,
+  rintro ⟨j, j'⟩ hj,
+  have hij := (ne_of_mem_of_not_mem hj hiu).symm,
+  replace hj := hu hj,
+  rw mem_product at hi hj,
+  obtain rfl | hij := eq_or_ne i j,
+  { refine (ht.pairwise_disjoint hi.2 hj.2 $ (prod.mk.inj_left _).ne_iff.1 hij).mono _ _,
+    { convert le_sup hi.1 },
+    { convert le_sup hj.1 } },
+  { refine (hs.pairwise_disjoint hi.1 hj.1 hij).mono _ _,
+    { convert le_sup hi.2 },
+    { convert le_sup hj.2 } }
+end
+
+lemma sup_indep_product_iff {s : finset ι} {t : finset ι'} {f : ι × ι' → α} :
+  (s.product t).sup_indep f ↔
+    s.sup_indep (λ i, t.sup $ λ i', f (i, i')) ∧ t.sup_indep (λ i', s.sup $ λ i, f (i, i')) :=
+begin
+  refine ⟨_, λ h, h.1.product h.2⟩,
+  simp_rw sup_indep_iff_pairwise_disjoint,
+  refine (λ h, ⟨λ i hi j hj hij, _, λ i hi j hj hij, _⟩);
+    simp_rw [function.on_fun, finset.disjoint_sup_left, finset.disjoint_sup_right];
+      intros i' hi' j' hj',
+  { exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne prod.fst hij) },
+  { exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne prod.snd hij) }
+end
+
 end distrib_lattice
 end finset
 
