[Merged by Bors] - feat(order/complete_lattice): independence of an indexed family

src/order/compactly_generated.lean

@@ -300,9 +300,9 @@ le_antisymm (begin
   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 α) :=
+theorem complete_lattice.set_independent_iff_finite {s : set α} :
+  complete_lattice.set_independent s ↔
+    ∀ t : finset α, ↑t ⊆ s → complete_lattice.set_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,
@@ -316,14 +316,14 @@ theorem complete_lattice.independent_iff_finite {s : set α} :
     exact ⟨ha, set.subset.trans ht (set.diff_subset _ _)⟩ }
 end⟩
 
-lemma complete_lattice.independent_Union_of_directed {η : Type*}
+lemma complete_lattice.set_independent_Union_of_directed {η : Type*}
   {s : η → set α} (hs : directed (⊆) s)
-  (h : ∀ i, complete_lattice.independent (s i)) :
-  complete_lattice.independent (⋃ i, s i) :=
+  (h : ∀ i, complete_lattice.set_independent (s i)) :
+  complete_lattice.set_independent (⋃ i, s i) :=
 begin
   by_cases hη : nonempty η,
   { resetI,
-    rw complete_lattice.independent_iff_finite,
+    rw complete_lattice.set_independent_iff_finite,
     intros t ht,
     obtain ⟨I, fi, hI⟩ := set.finite_subset_Union t.finite_to_set ht,
     obtain ⟨i, hi⟩ := hs.finset_le fi.to_finset,
@@ -335,10 +335,10 @@ end
 
 lemma complete_lattice.independent_sUnion_of_directed {s : set (set α)}
   (hs : directed_on (⊆) s)
-  (h : ∀ a ∈ s, complete_lattice.independent a) :
-  complete_lattice.independent (⋃₀ s) :=
+  (h : ∀ a ∈ s, complete_lattice.set_independent a) :
+  complete_lattice.set_independent (⋃₀ s) :=
 by rw set.sUnion_eq_Union; exact
-  complete_lattice.independent_Union_of_directed hs.directed_coe (by simpa using h)
+  complete_lattice.set_independent_Union_of_directed hs.directed_coe (by simpa using h)
 
 
 end
@@ -422,7 +422,7 @@ end, λ _, and.left⟩⟩
 theorem is_complemented_of_Sup_atoms_eq_top (h : Sup {a : α | is_atom a} = ⊤) : is_complemented α :=
 ⟨λ b, begin
   obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn.zorn_subset
-    {s : set α | complete_lattice.independent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _,
+    {s : set α | complete_lattice.set_independent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _,
   { refine ⟨Sup s, le_of_eq b_inf_Sup_s, _⟩,
     rw [← h, Sup_le_iff],
     intros a ha,

src/order/complete_lattice.lean

@@ -435,6 +435,10 @@ bsupr_le $ λ i hi, le_trans (h i hi) (le_bsupr i hi)
 theorem supr_le_supr_const (h : ι → ι₂) : (⨆ i:ι, a) ≤ (⨆ j:ι₂, a) :=
 supr_le $ le_supr _ ∘ h
 
+theorem bsupr_le_bsupr' {p q : ι → Prop} (hpq : ∀ i, p i → q i) {f : ι → α} :
+  (⨆ i (hpi : p i), f i) ≤ ⨆ i (hqi : q i), f i :=
+supr_le_supr $ λ i, supr_le_supr_const (hpq i)
+
 @[simp] theorem supr_le_iff : supr s ≤ a ↔ (∀i, s i ≤ a) :=
 (is_lub_le_iff is_lub_supr).trans forall_range_iff
 
@@ -1144,32 +1148,101 @@ 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 independent (s : set α) : Prop := ∀ ⦃a⦄, a ∈ s → disjoint a (Sup (s \ {a}))
+def set_independent (s : set α) : Prop := ∀ ⦃a⦄, a ∈ s → disjoint a (Sup (s \ {a}))
 
-variables {s : set α} (hs : independent s)
+variables {s : set α} (hs : set_independent s)
 
 @[simp]
-lemma independent_empty : independent (∅ : set α) :=
+lemma set_independent_empty : set_independent (∅ : set α) :=
 λ x hx, (set.not_mem_empty x hx).elim
 
-theorem independent.mono {t : set α} (hst : t ⊆ s) :
-  independent t :=
+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 independent.disjoint {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : disjoint x y :=
+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]⟩)
 
 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 independent.disjoint_Sup {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
+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],
+  apply forall_congr, intro a, apply forall_congr, intro 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 indepedent 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
+
+/-- 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