feat: characterise independence in compactly-generated lattices (#8154)

Also some loosely-related short lemmas

Author: ocfnash

Mathlib/Order/CompactlyGenerated.lean

@@ -53,6 +53,8 @@ This is demonstrated by means of the following four lemmas:
 complete lattice, well-founded, compact
 -/
 
+open Set
+
 variable {ι : Sort*} {α : Type*} [CompleteLattice α] {f : ι → α}
 
 namespace CompleteLattice
@@ -438,6 +440,28 @@ theorem CompleteLattice.setIndependent_iff_finite {s : Set α} :
         exact ⟨ha, Set.Subset.trans ht (Set.diff_subset _ _)⟩⟩
 #align complete_lattice.set_independent_iff_finite CompleteLattice.setIndependent_iff_finite
 
+lemma CompleteLattice.independent_iff_supIndep_of_injOn {ι : Type*} {f : ι → α}
+    (hf : InjOn f {i | f i ≠ ⊥}) :
+    CompleteLattice.Independent f ↔ ∀ (s : Finset ι), s.SupIndep f := by
+  refine ⟨fun h ↦ h.supIndep', fun h ↦ CompleteLattice.independent_def'.mpr fun i ↦ ?_⟩
+  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
+  intro s hs
+  classical
+  rw [← Finset.sup_erase_bot]
+  set t := s.erase ⊥
+  replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by refine hf ?_ ?_ hij <;> aesop
+  have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t := by
+    ext a
+    simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq, Finset.mem_insert, true_or, not_true,
+      Finset.erase_insert_eq_erase, not_and, Finset.mem_image]
+    refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
+    obtain ⟨j, hj, rfl⟩ := hs has
+    exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
+  rw [← this, Finset.sup_image]
+  specialize h (insert i (t.preimage _ hf))
+  rw [Finset.supIndep_iff_disjoint_erase] at h
+  exact h i (Finset.mem_insert_self i _)
+
 theorem CompleteLattice.setIndependent_iUnion_of_directed {η : Type*} {s : η → Set α}
     (hs : Directed (· ⊆ ·) s) (h : ∀ i, CompleteLattice.SetIndependent (s i)) :
     CompleteLattice.SetIndependent (⋃ i, s i) := by

Mathlib/Order/CompleteLattice.lean

@@ -693,6 +693,10 @@ theorem iSup_congr (h : ∀ i, f i = g i) : ⨆ i, f i = ⨆ i, g i :=
   congr_arg _ <| funext h
 #align supr_congr iSup_congr
 
+theorem biSup_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) :
+    ⨆ (i) (_ : p i), f i = ⨆ (i) (_ : p i), g i :=
+  iSup_congr <| fun i ↦ iSup_congr (h i)
+
 theorem Function.Surjective.iSup_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
     ⨆ x, g (f x) = ⨆ y, g y := by
   simp only [iSup._eq_1]
@@ -758,6 +762,10 @@ theorem iInf_congr (h : ∀ i, f i = g i) : ⨅ i, f i = ⨅ i, g i :=
   congr_arg _ <| funext h
 #align infi_congr iInf_congr
 
+theorem biInf_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) :
+    ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), g i :=
+  biSup_congr (α := αᵒᵈ) h
+
 theorem Function.Surjective.iInf_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
     ⨅ x, g (f x) = ⨅ y, g y :=
   @Function.Surjective.iSup_comp αᵒᵈ _ _ _ f hf g

Mathlib/Order/Disjoint.lean

@@ -42,6 +42,10 @@ def Disjoint (a b : α) : Prop :=
   ∀ ⦃x⦄, x ≤ a → x ≤ b → x ≤ ⊥
 #align disjoint Disjoint
 
+@[simp]
+theorem disjoint_of_subsingleton [Subsingleton α] : Disjoint a b :=
+  fun x _ _ ↦ le_of_eq (Subsingleton.elim x ⊥)
+
 theorem disjoint_comm : Disjoint a b ↔ Disjoint b a :=
   forall_congr' fun _ ↦ forall_swap
 #align disjoint.comm disjoint_comm

Mathlib/Order/SupIndep.lean

@@ -72,6 +72,7 @@ theorem SupIndep.subset (ht : t.SupIndep f) (h : s ⊆ t) : s.SupIndep f := fun
   ht (hu.trans h) (h hi)
 #align finset.sup_indep.subset Finset.SupIndep.subset
 
+@[simp]
 theorem supIndep_empty (f : ι → α) : (∅ : Finset ι).SupIndep f := fun _ _ a ha =>
   (not_mem_empty a ha).elim
 #align finset.sup_indep_empty Finset.supIndep_empty
@@ -406,17 +407,21 @@ theorem Independent.setIndependent_range (ht : Independent t) : SetIndependent <
   exact ht.comp' surjective_onto_range
 #align complete_lattice.independent.set_independent_range CompleteLattice.Independent.setIndependent_range
 
-theorem Independent.injective (ht : Independent t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Injective t := by
-  intro i j h
+theorem Independent.injOn (ht : Independent t) : InjOn t {i | t i ≠ ⊥} := by
+  rintro i _ j (hj : t j ≠ ⊥) h
   by_contra' contra
-  apply h_ne_bot j
+  apply hj
   suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
     replace ht := (ht i).mono_right this
     rwa [h, disjoint_self] at ht
   replace contra : j ≠ i
   · exact Ne.symm contra
   -- Porting note: needs explicit `f`
   exact @le_iSup₂ _ _ _ _ (fun x _ => t x) j contra
+
+theorem Independent.injective (ht : Independent t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Injective t := by
+  suffices univ = {i | t i ≠ ⊥} by rw [injective_iff_injOn_univ, this]; exact ht.injOn
+  aesop
 #align complete_lattice.independent.injective CompleteLattice.Independent.injective
 
 theorem independent_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j) :
@@ -473,6 +478,10 @@ alias ⟨CompleteLattice.Independent.supIndep, Finset.SupIndep.independent⟩ :=
 #align complete_lattice.independent.sup_indep CompleteLattice.Independent.supIndep
 #align finset.sup_indep.independent Finset.SupIndep.independent
 
+theorem CompleteLattice.Independent.supIndep' [CompleteLattice α] {f : ι → α} (s : Finset ι)
+    (h : CompleteLattice.Independent f) : s.SupIndep f :=
+  CompleteLattice.Independent.supIndep (h.comp Subtype.coe_injective)
+
 /-- A variant of `CompleteLattice.independent_iff_supIndep` for `Fintype`s. -/
 theorem CompleteLattice.independent_iff_supIndep_univ [CompleteLattice α] [Fintype ι] {f : ι → α} :
     CompleteLattice.Independent f ↔ Finset.univ.SupIndep f := by