chore(order/{complete_lattice,sup_indep}): move complete_lattice.independent (#12588)

Putting this here means that in future we can talk about `pairwise_disjoint` at the same time, which was previously defined downstream of `complete_lattice.independent`.
This commit only moves existing declarations and adjusts module docstrings.

The new authorship comes from #5971 and #7199, which predate this file.

Author: eric-wieser

src/group_theory/subgroup/basic.lean

@@ -9,6 +9,7 @@ import group_theory.submonoid.centralizer
 import algebra.group.conj
 import algebra.module.basic
 import order.atoms
+import order.sup_indep
 
 /-!
 # Subgroups

src/order/compactly_generated.lean

@@ -6,6 +6,7 @@ Authors: Oliver Nash
 import tactic.tfae
 import order.atoms
 import order.order_iso_nat
+import order.sup_indep
 import order.zorn
 import data.finset.order
 

src/order/complete_lattice.lean

@@ -1325,149 +1325,3 @@ protected def function.injective.complete_lattice [has_sup α] [has_inf α] [has
   bot_le := λ a, map_bot.le.trans bot_le,
   ..hf.lattice f map_sup map_inf }
 
-/-! ### Supremum independence-/
-
-namespace 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 set_independent (s : set α) : Prop := ∀ ⦃a⦄, a ∈ s → disjoint a (Sup (s \ {a}))
-
-variables {s : set α} (hs : set_independent s)
-
-@[simp]
-lemma set_independent_empty : set_independent (∅ : set α) :=
-λ x hx, (set.not_mem_empty x hx).elim
-
-theorem set_independent.mono {t : set α} (hst : t ⊆ s) :
-  set_independent t :=
-λ a ha, (hs (hst ha)).mono_right (Sup_le_Sup (diff_subset_diff_left hst))
-
-/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
-lemma set_independent.disjoint {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : disjoint x y :=
-disjoint_Sup_right (hs hx) ((mem_diff y).mpr ⟨hy, by simp [h.symm]⟩)
-
-lemma set_independent_pair {a b : α} (hab : a ≠ b) :
-  set_independent ({a, b} : set α) ↔ disjoint a b :=
-begin
-  split,
-  { intro h,
-    exact h.disjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab, },
-  { rintros h c ((rfl : c = a) | (rfl : c = b)),
-    { convert h using 1,
-      simp [hab, Sup_singleton] },
-    { convert h.symm using 1,
-      simp [hab, Sup_singleton] }, },
-end
-
-include hs
-
-/-- If the elements of a set are independent, then any element is disjoint from the `Sup` of some
-subset of the rest. -/
-lemma set_independent.disjoint_Sup {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
-  disjoint x (Sup y) :=
-begin
-  have := (hs.mono $ insert_subset.mpr ⟨hx, hy⟩) (mem_insert x _),
-  rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this,
-  exact this,
-end
-
-omit hs
-
-/-- An independent indexed family of elements in a complete lattice is one in which every element
-  is disjoint from the `supr` of the rest.
-
-  Example: an indexed family of non-zero elements in a
-  vector space is linearly independent iff the indexed family of subspaces they generate is
-  independent in this sense.
-
-  Example: an indexed family of submodules of a module is independent in this sense if
-  and only the natural map from the direct sum of the submodules to the module is injective. -/
-def independent {ι : Sort*} {α : Type*} [complete_lattice α] (t : ι → α) : Prop :=
-∀ i : ι, disjoint (t i) (⨆ (j ≠ i), t j)
-
-lemma set_independent_iff {α : Type*} [complete_lattice α] (s : set α) :
-  set_independent s ↔ independent (coe : s → α) :=
-begin
-  simp_rw [independent, set_independent, set_coe.forall, Sup_eq_supr],
-  refine forall₂_congr (λ a ha, _),
-  congr' 2,
-  convert supr_subtype.symm,
-  simp [supr_and],
-end
-
-variables {t : ι → α} (ht : independent t)
-
-theorem independent_def : independent t ↔ ∀ i : ι, disjoint (t i) (⨆ (j ≠ i), t j) :=
-iff.rfl
-
-theorem independent_def' {ι : Type*} {t : ι → α} :
-  independent t ↔ ∀ i, disjoint (t i) (Sup (t '' {j | j ≠ i})) :=
-by {simp_rw Sup_image, refl}
-
-theorem independent_def'' {ι : Type*} {t : ι → α} :
-  independent t ↔ ∀ i, disjoint (t i) (Sup {a | ∃ j ≠ i, t j = a}) :=
-by {rw independent_def', tidy}
-
-@[simp]
-lemma independent_empty (t : empty → α) : independent t.
-
-@[simp]
-lemma independent_pempty (t : pempty → α) : independent t.
-
-/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
-lemma independent.disjoint {x y : ι} (h : x ≠ y) : disjoint (t x) (t y) :=
-disjoint_Sup_right (ht x) ⟨y, by simp [h.symm]⟩
-
-lemma independent.mono {ι : Type*} {α : Type*} [complete_lattice α]
-  {s t : ι → α} (hs : independent s) (hst : t ≤ s) :
-  independent t :=
-λ i, (hs i).mono (hst i) (supr_le_supr $ λ j, supr_le_supr $ λ _, hst j)
-
-/-- Composing an independent indexed family with an injective function on the index results in
-another indepedendent indexed family. -/
-lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
-  {s : ι → α} (hs : independent s) (f : ι' → ι) (hf : function.injective f) :
-  independent (s ∘ f) :=
-λ i, (hs (f i)).mono_right begin
-  refine (supr_le_supr $ λ i, _).trans (supr_comp_le _ f),
-  exact supr_le_supr_const hf.ne,
-end
-
-lemma independent_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j):
-  independent t ↔ disjoint (t i) (t j) :=
-begin
-  split,
-  { intro h,
-    exact h.disjoint hij, },
-  { rintros h k,
-    obtain rfl | rfl := huniv k,
-    { refine h.mono_right (supr_le $ λ i, supr_le $ λ hi, eq.le _),
-      rw (huniv i).resolve_left hi },
-    { refine h.symm.mono_right (supr_le $ λ j, supr_le $ λ hj, eq.le _),
-      rw (huniv j).resolve_right hj } },
-end
-
-/-- Composing an indepedent indexed family with an order isomorphism on the elements results in
-another indepedendent indexed family. -/
-lemma independent.map_order_iso {ι : Sort*} {α β : Type*}
-  [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} (ha : independent a) :
-  independent (f ∘ a) :=
-λ i, ((ha i).map_order_iso f).mono_right (f.monotone.le_map_supr2 _)
-
-@[simp] lemma independent_map_order_iso_iff {ι : Sort*} {α β : Type*}
-  [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} :
-  independent (f ∘ a) ↔ independent a :=
-⟨ λ h, have hf : f.symm ∘ f ∘ a = a := congr_arg (∘ a) f.left_inv.comp_eq_id,
-      hf ▸ h.map_order_iso f.symm,
-  λ h, h.map_order_iso f⟩
-
-/-- If the elements of a set are independent, then any element is disjoint from the `supr` of some
-subset of the rest. -/
-lemma independent.disjoint_bsupr {ι : Type*} {α : Type*} [complete_lattice α]
-  {t : ι → α} (ht : independent t) {x : ι} {y : set ι} (hx : x ∉ y) :
-  disjoint (t x) (⨆ i ∈ y, t i) :=
-disjoint.mono_right (bsupr_le_bsupr' $ λ i hi, (ne_of_mem_of_not_mem hi hx : _)) (ht x)
-
-end complete_lattice

src/order/sup_indep.lean

@@ -1,31 +1,36 @@
 /-
-Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Copyright (c) 2021 Aaron Anderson, Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yaël Dillies
+Authors: Aaron Anderson, Kevin Buzzard, Yaël Dillies, Eric Wieser
 -/
 import data.finset.pairwise
 import data.set.finite
 
 /-!
-# Finite supremum independence
+# Supremum independence
 
 In this file, we define supremum independence of indexed sets. An indexed family `f : ι → α` is
 sup-independent if, for all `a`, `f a` and the supremum of the rest are disjoint.
 
 In distributive lattices, this is equivalent to being pairwise disjoint.
 
-## Implementation notes
+## Main definitions
 
-We avoid the "obvious" definition `∀ i ∈ s, disjoint (f i) ((s.erase i).sup f)` because `erase`
-would require decidable equality on `ι`.
+* `finset.sup_indep s f`: a family of elements `f` are supremum independent on the finite set `s`.
+* `complete_lattice.set_independent s`: a set of elements are supremum independent.
+* `complete_lattice.independent f`: a family of elements are supremum independent.
 
-## TODO
+## Implementation notes
 
-`complete_lattice.independent` and `complete_lattice.set_independent` should live in this file.
+For the finite version, we avoid the "obvious" definition
+`∀ i ∈ s, disjoint (f i) ((s.erase i).sup f)` because `erase` would require decidable equality on
+`ι`.
 -/
 
 variables {α β ι ι' : Type*}
 
+/-! ### On lattices with a bottom element, via `finset.sup` -/
+
 namespace finset
 section lattice
 variables [lattice α] [order_bot α]
@@ -141,6 +146,156 @@ by { rw ←sup_eq_bUnion, exact hs.sup hg }
 end distrib_lattice
 end finset
 
+
+/-! ### On complete lattices via `has_Sup.Sup` -/
+
+namespace complete_lattice
+variables [complete_lattice α]
+
+open set
+
+/-- An independent set of elements in a complete lattice is one in which every element is disjoint
+  from the `Sup` of the rest. -/
+def set_independent (s : set α) : Prop := ∀ ⦃a⦄, a ∈ s → disjoint a (Sup (s \ {a}))
+
+variables {s : set α} (hs : set_independent s)
+
+@[simp]
+lemma set_independent_empty : set_independent (∅ : set α) :=
+λ x hx, (set.not_mem_empty x hx).elim
+
+theorem set_independent.mono {t : set α} (hst : t ⊆ s) :
+  set_independent t :=
+λ a ha, (hs (hst ha)).mono_right (Sup_le_Sup (diff_subset_diff_left hst))
+
+/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
+lemma set_independent.disjoint {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : disjoint x y :=
+disjoint_Sup_right (hs hx) ((mem_diff y).mpr ⟨hy, by simp [h.symm]⟩)
+
+lemma set_independent_pair {a b : α} (hab : a ≠ b) :
+  set_independent ({a, b} : set α) ↔ disjoint a b :=
+begin
+  split,
+  { intro h,
+    exact h.disjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab, },
+  { rintros h c ((rfl : c = a) | (rfl : c = b)),
+    { convert h using 1,
+      simp [hab, Sup_singleton] },
+    { convert h.symm using 1,
+      simp [hab, Sup_singleton] }, },
+end
+
+include hs
+
+/-- If the elements of a set are independent, then any element is disjoint from the `Sup` of some
+subset of the rest. -/
+lemma set_independent.disjoint_Sup {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
+  disjoint x (Sup y) :=
+begin
+  have := (hs.mono $ insert_subset.mpr ⟨hx, hy⟩) (mem_insert x _),
+  rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this,
+  exact this,
+end
+
+omit hs
+
+/-- An independent indexed family of elements in a complete lattice is one in which every element
+  is disjoint from the `supr` of the rest.
+
+  Example: an indexed family of non-zero elements in a
+  vector space is linearly independent iff the indexed family of subspaces they generate is
+  independent in this sense.
+
+  Example: an indexed family of submodules of a module is independent in this sense if
+  and only the natural map from the direct sum of the submodules to the module is injective. -/
+def independent {ι : Sort*} {α : Type*} [complete_lattice α] (t : ι → α) : Prop :=
+∀ i : ι, disjoint (t i) (⨆ (j ≠ i), t j)
+
+lemma set_independent_iff {α : Type*} [complete_lattice α] (s : set α) :
+  set_independent s ↔ independent (coe : s → α) :=
+begin
+  simp_rw [independent, set_independent, set_coe.forall, Sup_eq_supr],
+  refine forall₂_congr (λ a ha, _),
+  congr' 2,
+  convert supr_subtype.symm,
+  simp [supr_and],
+end
+
+variables {t : ι → α} (ht : independent t)
+
+theorem independent_def : independent t ↔ ∀ i : ι, disjoint (t i) (⨆ (j ≠ i), t j) :=
+iff.rfl
+
+theorem independent_def' {ι : Type*} {t : ι → α} :
+  independent t ↔ ∀ i, disjoint (t i) (Sup (t '' {j | j ≠ i})) :=
+by {simp_rw Sup_image, refl}
+
+theorem independent_def'' {ι : Type*} {t : ι → α} :
+  independent t ↔ ∀ i, disjoint (t i) (Sup {a | ∃ j ≠ i, t j = a}) :=
+by {rw independent_def', tidy}
+
+@[simp]
+lemma independent_empty (t : empty → α) : independent t.
+
+@[simp]
+lemma independent_pempty (t : pempty → α) : independent t.
+
+/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
+lemma independent.disjoint {x y : ι} (h : x ≠ y) : disjoint (t x) (t y) :=
+disjoint_Sup_right (ht x) ⟨y, by simp [h.symm]⟩
+
+lemma independent.mono {ι : Type*} {α : Type*} [complete_lattice α]
+  {s t : ι → α} (hs : independent s) (hst : t ≤ s) :
+  independent t :=
+λ i, (hs i).mono (hst i) (supr_le_supr $ λ j, supr_le_supr $ λ _, hst j)
+
+/-- Composing an independent indexed family with an injective function on the index results in
+another indepedendent indexed family. -/
+lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
+  {s : ι → α} (hs : independent s) (f : ι' → ι) (hf : function.injective f) :
+  independent (s ∘ f) :=
+λ i, (hs (f i)).mono_right begin
+  refine (supr_le_supr $ λ i, _).trans (supr_comp_le _ f),
+  exact supr_le_supr_const hf.ne,
+end
+
+lemma independent_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j):
+  independent t ↔ disjoint (t i) (t j) :=
+begin
+  split,
+  { intro h,
+    exact h.disjoint hij, },
+  { rintros h k,
+    obtain rfl | rfl := huniv k,
+    { refine h.mono_right (supr_le $ λ i, supr_le $ λ hi, eq.le _),
+      rw (huniv i).resolve_left hi },
+    { refine h.symm.mono_right (supr_le $ λ j, supr_le $ λ hj, eq.le _),
+      rw (huniv j).resolve_right hj } },
+end
+
+/-- Composing an indepedent indexed family with an order isomorphism on the elements results in
+another indepedendent indexed family. -/
+lemma independent.map_order_iso {ι : Sort*} {α β : Type*}
+  [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} (ha : independent a) :
+  independent (f ∘ a) :=
+λ i, ((ha i).map_order_iso f).mono_right (f.monotone.le_map_supr2 _)
+
+@[simp] lemma independent_map_order_iso_iff {ι : Sort*} {α β : Type*}
+  [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} :
+  independent (f ∘ a) ↔ independent a :=
+⟨ λ h, have hf : f.symm ∘ f ∘ a = a := congr_arg (∘ a) f.left_inv.comp_eq_id,
+      hf ▸ h.map_order_iso f.symm,
+  λ h, h.map_order_iso f⟩
+
+/-- If the elements of a set are independent, then any element is disjoint from the `supr` of some
+subset of the rest. -/
+lemma independent.disjoint_bsupr {ι : Type*} {α : Type*} [complete_lattice α]
+  {t : ι → α} (ht : independent t) {x : ι} {y : set ι} (hx : x ∉ y) :
+  disjoint (t x) (⨆ i ∈ y, t i) :=
+disjoint.mono_right (bsupr_le_bsupr' $ λ i hi, (ne_of_mem_of_not_mem hi hx : _)) (ht x)
+
+end complete_lattice
+
 lemma complete_lattice.independent_iff_sup_indep [complete_lattice α] {s : finset ι} {f : ι → α} :
   complete_lattice.independent (f ∘ (coe : s → ι)) ↔ s.sup_indep f :=
 begin