feat(order/compactly_generated): A compactly-generated modular lattic…

…e is complemented iff atomistic (#6071)

Shows that a compactly-generated modular lattice is complemented iff it is atomistic
Proves extra lemmas about atomistic or compactly-generated lattices
Proves extra lemmas about `complete_lattice.independent`
Fix the name of `is_modular_lattice.sup_inf_sup_assoc`



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

docs/references.bib

@@ -593,3 +593,12 @@ @article {MR317916
        DOI = {10.2307/2318447},
        URL = {https://doi.org/10.2307/2318447},
 }
+
+@book{calugareanu,
+      author = {C\v{a}lug\v{a}reanu, Grigore},
+      year = {2000},
+      month = {01},
+      pages = {},
+      title = {Lattice Concepts of Module Theory},
+      doi = {10.1007/978-94-015-9588-9}
+}

src/order/atoms.lean

@@ -219,6 +219,32 @@ instance : is_atomic α :=
 
 end is_atomistic
 
+section is_atomistic
+variables [is_atomistic α]
+
+@[simp]
+theorem Sup_atoms_le_eq (b : α) : Sup {a : α | is_atom a ∧ a ≤ b} = b :=
+begin
+  rcases eq_Sup_atoms b with ⟨s, rfl, hs⟩,
+  exact le_antisymm (Sup_le (λ _, and.right)) (Sup_le_Sup (λ a ha, ⟨hs a ha, le_Sup ha⟩)),
+end
+
+@[simp]
+theorem Sup_atoms_eq_top : Sup {a : α | is_atom a} = ⊤ :=
+begin
+  refine eq.trans (congr rfl (set.ext (λ x, _))) (Sup_atoms_le_eq ⊤),
+  exact (and_iff_left le_top).symm,
+end
+
+theorem le_iff_atom_le_imp {a b : α} :
+  a ≤ b ↔ ∀ c : α, is_atom c → c ≤ a → c ≤ b :=
+⟨λ ab c hc ca, le_trans ca ab, λ h, begin
+  rw [← Sup_atoms_le_eq a, ← Sup_atoms_le_eq b],
+  exact Sup_le_Sup (λ c hc, ⟨hc.1, h c hc.1 hc.2⟩),
+end⟩
+
+end is_atomistic
+
 namespace is_coatomistic
 
 instance is_atomistic_dual [h : is_coatomistic α] : is_atomistic (order_dual α) :=

src/order/compactly_generated.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import data.set.finite
+import data.finset.order
 import order.well_founded
 import order.order_iso_nat
 import order.atoms
@@ -38,14 +40,19 @@ This is demonstrated by means of the following four lemmas:
  We also show well-founded lattices are compactly generated
  (`complete_lattice.compactly_generated_of_well_founded`).
 
+## References
+- [G. Călugăreanu, *Lattice Concepts of Module Theory*][calugareanu]
+
 ## Tags
 
 complete lattice, well-founded, compact
 -/
 
+variables {α : Type*} [complete_lattice α]
+
 namespace complete_lattice
 
-variables (α : Type*) [complete_lattice α]
+variables (α)
 
 /-- A compactness property for a complete lattice is that any `sup`-closed non-empty subset
 contains its `Sup`. -/
@@ -243,7 +250,7 @@ class is_compactly_generated (α : Type*) [complete_lattice α] : Prop :=
   ∀ (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 α}
+variables {α} [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 :=
@@ -252,6 +259,14 @@ begin
   exact le_antisymm (Sup_le (λ c hc, hc.2)) (Sup_le_Sup (λ c cs, ⟨hs c cs, le_Sup cs⟩)),
 end
 
+@[simp]
+theorem Sup_compact_eq_top :
+  Sup {a : α | complete_lattice.is_compact_element a} = ⊤ :=
+begin
+  refine eq.trans (congr rfl (set.ext (λ x, _))) (Sup_compact_le_eq ⊤),
+  exact (and_iff_left le_top).symm,
+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
@@ -301,10 +316,34 @@ 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*}
+  {s : η → set α} (hs : directed (⊆) s)
+  (h : ∀ i, complete_lattice.independent (s i)) :
+  complete_lattice.independent (⋃ i, s i) :=
+begin
+  by_cases hη : nonempty η,
+  { resetI,
+    rw complete_lattice.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,
+    exact (h i).mono (set.subset.trans hI $ set.bUnion_subset $
+      λ j hj, hi j (set.finite.mem_to_finset.2 hj)) },
+  { rintros a ⟨_, ⟨i, _⟩, _⟩,
+    exfalso, exact hη ⟨i⟩, },
+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) :=
+by rw set.sUnion_eq_Union; exact
+  complete_lattice.independent_Union_of_directed hs.directed_coe (by simpa using h)
+
+
 end
 
 namespace complete_lattice
-variables {α : Type*} [complete_lattice α]
 
 lemma compactly_generated_of_well_founded (h : well_founded ((>) : α → α → Prop)) :
   is_compactly_generated α :=
@@ -334,3 +373,104 @@ theorem Iic_coatomic_of_compact_element {k : α} (h : is_compact_element k) :
 end⟩
 
 end complete_lattice
+
+section
+variables [is_modular_lattice α] [is_compactly_generated α]
+
+@[priority 100]
+instance is_atomic_of_is_complemented [is_complemented α] : is_atomic α :=
+⟨λ b, begin
+  by_cases h : {c : α | complete_lattice.is_compact_element c ∧ c ≤ b} ⊆ {⊥},
+  { left,
+    rw [← Sup_compact_le_eq b, Sup_eq_bot],
+    exact h },
+  { rcases set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩,
+    right,
+    have hc' := complete_lattice.Iic_coatomic_of_compact_element hc,
+    rw ← is_atomic_iff_is_coatomic at hc',
+    haveI := hc',
+    obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : set.Iic c),
+    { exfalso,
+      apply hcbot,
+      simp only [subtype.ext_iff, set.Iic.coe_bot, subtype.coe_mk] at con,
+      exact con },
+    rw [← subtype.coe_le_coe, subtype.coe_mk] at hac,
+    exact ⟨a, ha.of_is_atom_coe_Iic, hac.trans hcb⟩ },
+end⟩
+
+/-- See Lemma 5.1, Călugăreanu -/
+@[priority 100]
+instance is_atomistic_of_is_complemented [is_complemented α] : is_atomistic α :=
+⟨λ b, ⟨{a | is_atom a ∧ a ≤ b}, begin
+  symmetry,
+  have hle : Sup {a : α | is_atom a ∧ a ≤ b} ≤ b := (Sup_le $ λ _, and.right),
+  apply (lt_or_eq_of_le hle).resolve_left (λ con, _),
+  obtain ⟨c, hc⟩ := exists_is_compl (⟨Sup {a : α | is_atom a ∧ a ≤ b}, hle⟩ : set.Iic b),
+  obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c,
+  { exact ne_of_lt con (subtype.ext_iff.1 (eq_top_of_is_compl_bot hc)) },
+  { apply ha.1,
+    rw eq_bot_iff,
+    apply le_trans (le_inf _ hac) hc.1,
+    rw [← subtype.coe_le_coe, subtype.coe_mk],
+    exact le_Sup ⟨ha.of_is_atom_coe_Iic, a.2⟩ }
+end, λ _, and.left⟩⟩
+
+/-- See Theorem 6.6, Călugăreanu -/
+theorem is_complemented_of_is_atomistic [is_atomistic α] : is_complemented α :=
+⟨λ b, begin
+  rcases zorn.zorn_subset
+    {s : set α | complete_lattice.independent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _ with
+      ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩,
+  { refine ⟨Sup s, le_of_eq b_inf_Sup_s, le_iff_atom_le_imp.2 (λ a ha _, _)⟩,
+    rw ← inf_eq_left,
+    refine (eq_bot_or_eq_of_le_atom ha inf_le_left).resolve_left (λ con, ha.1 _),
+    rw [eq_bot_iff, ← con],
+    refine le_inf (le_refl a) ((le_Sup _).trans le_sup_right),
+    rw ← disjoint_iff at *,
+    have a_dis_Sup_s : disjoint a (Sup s) := con.mono_right le_sup_right,
+    rw ← s_max (s ∪ {a}) ⟨λ x hx, _, ⟨_, λ x hx, _⟩⟩ (set.subset_union_left _ _),
+    { exact set.mem_union_right _ (set.mem_singleton _) },
+    { rw [set.mem_union, set.mem_singleton_iff] at hx,
+      by_cases xa : x = a,
+      { simp only [xa, set.mem_singleton, set.insert_diff_of_mem, set.union_singleton],
+        exact con.mono_right (le_trans (Sup_le_Sup (set.diff_subset s {a})) le_sup_right) },
+      { have h : (s ∪ {a}) \ {x} = (s \ {x}) ∪ {a},
+        { simp only [set.union_singleton],
+          rw set.insert_diff_of_not_mem,
+          rw set.mem_singleton_iff,
+          exact ne.symm xa },
+        rw [h, Sup_union, Sup_singleton],
+        apply (s_ind x (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
+          (a_dis_Sup_s.mono_right _).symm,
+        rw [← Sup_insert, set.insert_diff_singleton,
+          set.insert_eq_of_mem (hx.resolve_right xa)] } },
+    { rw [Sup_union, Sup_singleton, ← disjoint_iff],
+      exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm },
+    { rw [set.mem_union, set.mem_singleton_iff] at hx,
+      cases hx,
+      { exact s_atoms x hx },
+      { rw hx,
+        exact ha } } },
+  { intros c hc1 hc2,
+    refine ⟨⋃₀ c, ⟨complete_lattice.independent_sUnion_of_directed hc2.directed_on
+      (λ s hs, (hc1 hs).1), _, λ a ha, _⟩, λ _, set.subset_sUnion_of_mem⟩,
+    { rw [Sup_sUnion, ← Sup_image, inf_Sup_eq_of_directed_on, supr_eq_bot],
+      { intro i,
+        rw supr_eq_bot,
+        intro hi,
+        obtain ⟨x, xc, rfl⟩ := (set.mem_image _ _ _).1 hi,
+        exact (hc1 xc).2.1 },
+      { rw directed_on_image,
+        refine hc2.directed_on.mono (λ s t, Sup_le_Sup) } },
+    { rcases set.mem_sUnion.1 ha with ⟨s, sc, as⟩,
+      exact (hc1 sc).2.2 a as } }
+end⟩
+
+theorem is_complemented_iff_is_atomistic : is_complemented α ↔ is_atomistic α :=
+begin
+  split; introsI,
+  { exact is_atomistic_of_is_complemented },
+  { exact is_complemented_of_is_atomistic }
+end
+
+end

src/order/complete_lattice.lean

@@ -380,6 +380,18 @@ le_antisymm
   (Sup_le $ assume b h, le_supr_of_le b $ le_supr _ h)
   (supr_le $ assume b, supr_le $ assume h, le_Sup h)
 
+lemma Sup_sUnion {s : set (set α)} :
+  Sup (⋃₀ s) = ⨆ (t ∈ s), Sup t :=
+begin
+  apply le_antisymm,
+  { apply Sup_le (λ b hb, _),
+    rcases hb with ⟨t, ts, bt⟩,
+    apply le_trans _ (le_supr _ t),
+    exact le_trans (le_Sup bt) (le_supr _ ts), },
+  { apply supr_le (λ t, _),
+    exact supr_le (λ ts, Sup_le_Sup (λ x xt, ⟨t, ts, xt⟩)) }
+end
+
 lemma le_supr_iff : (a ≤ supr s) ↔ (∀ b, (∀ i, s i ≤ b) → a ≤ b) :=
 ⟨λ h b hb, le_trans h (supr_le hb), λ h, h _ $ λ i, le_supr s i⟩
 
@@ -1027,6 +1039,10 @@ variables [complete_lattice α]
   from the `Sup` of the rest. -/
 def complete_lattice.independent (s : set α) : Prop := ∀ a ∈ s, disjoint a (Sup (s \ {a}))
 
+@[simp]
+lemma complete_lattice.independent_empty : complete_lattice.independent (∅ : set α) :=
+λ x hx, (set.not_mem_empty x hx).elim
+
 theorem complete_lattice.independent.mono {s t : set α}
   (ht : complete_lattice.independent t) (hst : s ⊆ t) :
   complete_lattice.independent s :=

src/order/modular_lattice.lean

@@ -21,8 +21,8 @@ any distributive lattice.
   This corresponds to the diamond (or second) isomorphism theorems of algebra.
 
 ## Main Results
-- `is_modular_lattice_iff_sup_inf_sup_assoc`:
-  Modularity is equivalent to the `sup_inf_sup_assoc`: `(x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z`
+- `is_modular_lattice_iff_inf_sup_inf_assoc`:
+  Modularity is equivalent to the `inf_sup_inf_assoc`: `(x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z`
 - `distrib_lattice.is_modular_lattice`: Distributive lattices are modular.
 
 ## To do
@@ -44,7 +44,7 @@ theorem sup_inf_assoc_of_le {x : α} (y : α) {z : α} (h : x ≤ z) :
 le_antisymm (is_modular_lattice.sup_inf_le_assoc_of_le y h)
   (le_inf (sup_le_sup_left inf_le_left _) (sup_le h inf_le_right))
 
-theorem is_modular_lattice.sup_inf_sup_assoc {x y z : α} :
+theorem is_modular_lattice.inf_sup_inf_assoc {x y z : α} :
   (x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z :=
 (sup_inf_assoc_of_le y inf_le_right).symm
 
@@ -56,6 +56,10 @@ instance : is_modular_lattice (order_dual α) :=
 ⟨λ x y z xz, le_of_eq (by { rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm],
   convert sup_inf_assoc_of_le (order_dual.of_dual y) (order_dual.dual_le.2 xz) })⟩
 
+theorem is_modular_lattice.sup_inf_sup_assoc {x y z : α} :
+  (x ⊔ z) ⊓ (y ⊔ z) = ((x ⊔ z) ⊓ y) ⊔ z :=
+@is_modular_lattice.inf_sup_inf_assoc (order_dual α) _ _ _ _ _
+
 /-- The diamond isomorphism between the intervals `[a ⊓ b, a]` and `[b, a ⊔ b]` -/
 def inf_Icc_order_iso_Icc_sup (a b : α) : set.Icc (a ⊓ b) a ≃o set.Icc b (a ⊔ b) :=
 { to_fun := λ x, ⟨x ⊔ b, ⟨le_sup_right, sup_le_sup_right x.prop.2 b⟩⟩,
@@ -85,9 +89,9 @@ def Iic_order_iso_Ici {a b : α} (h : is_compl a b) : set.Iic a ≃o set.Ici b :
 
 end is_compl
 
-theorem is_modular_lattice_iff_sup_inf_sup_assoc [lattice α] :
+theorem is_modular_lattice_iff_inf_sup_inf_assoc [lattice α] :
   is_modular_lattice α ↔ ∀ (x y z : α), (x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z :=
-⟨λ h, @is_modular_lattice.sup_inf_sup_assoc _ _ h, λ h, ⟨λ x y z xz, by rw [← inf_eq_left.2 xz, h]⟩⟩
+⟨λ h, @is_modular_lattice.inf_sup_inf_assoc _ _ h, λ h, ⟨λ x y z xz, by rw [← inf_eq_left.2 xz, h]⟩⟩
 
 namespace distrib_lattice
 
@@ -97,6 +101,17 @@ instance [distrib_lattice α] : is_modular_lattice α :=
 
 end distrib_lattice
 
+theorem disjoint.disjoint_sup_right_of_disjoint_sup_left
+  [bounded_lattice α] [is_modular_lattice α] {a b c : α}
+  (h : disjoint a b) (hsup : disjoint (a ⊔ b) c) :
+  disjoint a (b ⊔ c) :=
+begin
+  rw [disjoint, ← h.eq_bot, sup_comm],
+  apply le_inf inf_le_left,
+  apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans,
+  rw [sup_comm, is_modular_lattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]
+end
+
 namespace is_modular_lattice
 
 variables [bounded_lattice α] [is_modular_lattice α] {a : α}