feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971)

Defines `complete_lattice.independent`
Shows that this notion of independence is finitary in compactly generated lattices



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

Author: awainverse

src/order/compactly_generated.lean

@@ -242,6 +242,67 @@ class is_compactly_generated (α : Type*) [complete_lattice α] : Prop :=
 (exists_Sup_eq :
   ∀ (x : α), ∃ (s : set α), (∀ x ∈ s, complete_lattice.is_compact_element x) ∧ Sup s = x)
 
+section
+variables {α : Type*} [complete_lattice α] [is_compactly_generated α] {a b : α} {s : set α}
+
+@[simp]
+lemma Sup_compact_le_eq (b) : Sup {c : α | complete_lattice.is_compact_element c ∧ c ≤ b} = b :=
+begin
+  rcases is_compactly_generated.exists_Sup_eq b with ⟨s, hs, rfl⟩,
+  exact le_antisymm (Sup_le (λ c hc, hc.2)) (Sup_le_Sup (λ c cs, ⟨hs c cs, le_Sup cs⟩)),
+end
+
+theorem le_iff_compact_le_imp {a b : α} :
+  a ≤ b ↔ ∀ c : α, complete_lattice.is_compact_element c → c ≤ a → c ≤ b :=
+⟨λ ab c hc ca, le_trans ca ab, λ h, begin
+  rw [← Sup_compact_le_eq a, ← Sup_compact_le_eq b],
+  exact Sup_le_Sup (λ c hc, ⟨hc.1, h c hc.1 hc.2⟩),
+end⟩
+
+/-- This property is sometimes referred to as `α` being upper continuous. -/
+theorem inf_Sup_eq_of_directed_on (h : directed_on (≤) s):
+  a ⊓ Sup s = ⨆ b ∈ s, a ⊓ b :=
+le_antisymm (begin
+  rw le_iff_compact_le_imp,
+  by_cases hs : s.nonempty,
+  { intros c hc hcinf,
+    rw le_inf_iff at hcinf,
+    rw complete_lattice.is_compact_element_iff_le_of_directed_Sup_le at hc,
+    rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩,
+    exact (le_inf hcinf.1 cd).trans (le_bsupr d ds) },
+  { rw set.not_nonempty_iff_eq_empty at hs,
+    simp [hs] }
+end) supr_inf_le_inf_Sup
+
+/-- This property is equivalent to `α` being upper continuous. -/
+theorem inf_Sup_eq_supr_inf_sup_finset :
+  a ⊓ Sup s = ⨆ (t : finset α) (H : ↑t ⊆ s), a ⊓ (t.sup id) :=
+le_antisymm (begin
+  rw le_iff_compact_le_imp,
+  intros c hc hcinf,
+  rw le_inf_iff at hcinf,
+  rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩,
+  exact (le_inf hcinf.1 ht2).trans (le_bsupr t ht1),
+end) (supr_le $ λ t, supr_le $ λ h, inf_le_inf_left _ ((finset.sup_eq_Sup t).symm ▸ (Sup_le_Sup h)))
+
+theorem complete_lattice.independent_iff_finite {s : set α} :
+  complete_lattice.independent s ↔
+    ∀ t : finset α, ↑t ⊆ s → complete_lattice.independent (↑t : set α) :=
+⟨λ hs t ht, hs.mono ht, λ h a ha, begin
+  rw [disjoint_iff, inf_Sup_eq_supr_inf_sup_finset, supr_eq_bot],
+  intro t,
+  rw [supr_eq_bot, finset.sup_eq_Sup],
+  intro ht,
+  classical,
+  have h' := (h (insert a t) _ a (t.mem_insert_self a)).eq_bot,
+  { rwa [finset.coe_insert, set.insert_diff_self_of_not_mem] at h',
+    exact λ con, ((set.mem_diff a).1 (ht con)).2 (set.mem_singleton a) },
+  { rw [finset.coe_insert, set.insert_subset],
+    exact ⟨ha, set.subset.trans ht (set.diff_subset _ _)⟩ }
+end⟩
+
+end
+
 namespace complete_lattice
 variables {α : Type*} [complete_lattice α]
 

src/order/complete_boolean_algebra.lean

@@ -24,17 +24,13 @@ section complete_distrib_lattice
 variables [complete_distrib_lattice α] {a b : α} {s t : set α}
 
 theorem sup_Inf_eq : a ⊔ Inf s = (⨅ b ∈ s, a ⊔ b) :=
-le_antisymm
-  (le_infi $ assume i, le_infi $ assume h, sup_le_sup_left (Inf_le h) _)
-  (complete_distrib_lattice.infi_sup_le_sup_Inf _ _)
+sup_Inf_le_infi_sup.antisymm (complete_distrib_lattice.infi_sup_le_sup_Inf _ _)
 
 theorem Inf_sup_eq : Inf s ⊔ b = (⨅ a ∈ s, a ⊔ b) :=
 by simpa [sup_comm] using @sup_Inf_eq α _ b s
 
 theorem inf_Sup_eq : a ⊓ Sup s = (⨆ b ∈ s, a ⊓ b) :=
-le_antisymm
-  (complete_distrib_lattice.inf_Sup_le_supr_inf _ _)
-  (supr_le $ assume i, supr_le $ assume h, inf_le_inf_left _ (le_Sup h))
+(complete_distrib_lattice.inf_Sup_le_supr_inf _ _).antisymm supr_inf_le_inf_Sup
 
 theorem Sup_inf_eq : Sup s ⊓ b = (⨆ a ∈ s, a ⊓ b) :=
 by simpa [inf_comm] using @inf_Sup_eq α _ b s

src/order/complete_lattice.lean

@@ -1006,3 +1006,30 @@ instance [complete_lattice α] [complete_lattice β] : complete_lattice (α × 
   .. prod.has_Inf α β }
 
 end prod
+
+section complete_lattice
+variables [complete_lattice α] {a : α} {s : set α}
+
+lemma sup_Inf_le_infi_sup :
+  a ⊔ Inf s ≤ (⨅ b ∈ s, a ⊔ b) :=
+le_infi $ assume i, le_infi $ assume h, sup_le_sup_left (Inf_le h) _
+
+lemma supr_inf_le_inf_Sup :
+  (⨆ b ∈ s, a ⊓ b) ≤ a ⊓ Sup s :=
+supr_le $ assume i, supr_le $ assume h, inf_le_inf_left _ (le_Sup h)
+
+end complete_lattice
+
+section complete_lattice
+variables [complete_lattice α]
+
+/-- An independent set of elements in a complete lattice is one in which every element is disjoint
+  from the `Sup` of the rest. -/
+def complete_lattice.independent (s : set α) : Prop := ∀ a ∈ s, disjoint a (Sup (s \ {a}))
+
+theorem complete_lattice.independent.mono {s t : set α}
+  (ht : complete_lattice.independent t) (hst : s ⊆ t) :
+  complete_lattice.independent s :=
+λ a ha, (ht a (hst ha)).mono_right (Sup_le_Sup (diff_subset_diff_left hst))
+
+end complete_lattice