feat(order/atoms): define (co)atomic, (co)atomistic lattices (#5588)

Define (co)atomic, (co)atomistic lattices
Relate these lattice definitions
Provide basic subtype instances



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

src/order/atoms.lean

@@ -20,6 +20,12 @@ which are lattices with only two elements, and related ideas.
   * `is_atom a` indicates that the only element below `a` is `⊥`.
   * `is_coatom a` indicates that the only element above `a` is `⊤`.
 
+### Atomic and Atomistic Lattices
+  * `is_atomic` indicates that every element other than `⊥` is above an atom.
+  * `is_coatomic` indicates that every element other than `⊤` is below a coatom.
+  * `is_atomistic` indicates that every element is the `Sup` of a set of atoms.
+  * `is_coatomistic` indicates that every element is the `Inf` of a set of coatoms.
+
 ### Simple Lattices
   * `is_simple_lattice` indicates that a bounded lattice has only two elements, `⊥` and `⊤`.
   * `is_simple_lattice.bounded_distrib_lattice`
@@ -30,7 +36,7 @@ which are lattices with only two elements, and related ideas.
     * `is_simple_lattice.complete_boolean_algebra`
 
 ## Main results
-  * `is_atom_iff_is_coatom_dual` and `is_coatom_iff_is_atom_dual` express the (definitional) duality
+  * `is_atom_dual_iff_is_coatom` and `is_coatom_dual_iff_is_atom` express the (definitional) duality
    of `is_atom` and `is_coatom`.
   * `is_simple_lattice_iff_is_atom_top` and `is_simple_lattice_iff_is_coatom_bot` express the
   connection between atoms, coatoms, and simple lattices
@@ -50,7 +56,13 @@ variable [order_bot α]
 def is_atom (a : α) : Prop := a ≠ ⊥ ∧ (∀ b, b < a → b = ⊥)
 
 lemma eq_bot_or_eq_of_le_atom {a b : α} (ha : is_atom a) (hab : b ≤ a) : b = ⊥ ∨ b = a :=
-or.imp_left (ha.2 b) (lt_or_eq_of_le hab)
+hab.lt_or_eq.imp_left (ha.2 b)
+
+lemma is_atom.Iic {x a : α} (ha : is_atom a) (hax : a ≤ x) : is_atom (⟨a, hax⟩ : set.Iic x) :=
+⟨λ con, ha.1 (subtype.mk_eq_mk.1 con), λ ⟨b, hb⟩ hba, subtype.mk_eq_mk.2 (ha.2 b hba)⟩
+
+lemma is_atom.of_is_atom_coe_Iic {x : α} {a : set.Iic x} (ha : is_atom a) : is_atom (a : α) :=
+⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩
 
 end is_atom
 
@@ -63,7 +75,14 @@ variable [order_top α]
 def is_coatom (a : α) : Prop := a ≠ ⊤ ∧ (∀ b, a < b → b = ⊤)
 
 lemma eq_top_or_eq_of_coatom_le {a b : α} (ha : is_coatom a) (hab : a ≤ b) : b = ⊤ ∨ b = a :=
-or.imp (ha.2 b) eq_comm.2 (lt_or_eq_of_le hab)
+hab.lt_or_eq.imp (ha.2 b) eq_comm.2
+
+lemma is_coatom.Ici {x a : α} (ha : is_coatom a) (hax : x ≤ a) : is_coatom (⟨a, hax⟩ : set.Ici x) :=
+⟨λ con, ha.1 (subtype.mk_eq_mk.1 con), λ ⟨b, hb⟩ hba, subtype.mk_eq_mk.2 (ha.2 b hba)⟩
+
+lemma is_coatom.of_is_coatom_coe_Ici {x : α} {a : set.Ici x} (ha : is_coatom a) :
+  is_coatom (a : α) :=
+⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, le_trans a.prop hba.le⟩ hba)⟩
 
 end is_coatom
 
@@ -89,12 +108,131 @@ end pairwise
 
 variables [bounded_lattice α] {a : α}
 
-lemma is_atom_iff_is_coatom_dual : is_atom a ↔ is_coatom (order_dual.to_dual a) := iff.refl _
+@[simp]
+lemma is_coatom_dual_iff_is_atom : is_coatom (order_dual.to_dual a) ↔ is_atom a := iff.refl _
 
-lemma is_coatom_iff_is_atom_dual : is_coatom a ↔ is_atom (order_dual.to_dual a) := iff.refl _
+@[simp]
+lemma is_atom_dual_iff_is_coatom : is_atom (order_dual.to_dual a) ↔ is_coatom a := iff.refl _
 
 end atoms
 
+section atomic
+
+variables (α) [bounded_lattice α]
+
+/-- A lattice is atomic iff every element other than `⊥` has an atom below it. -/
+class is_atomic : Prop :=
+(eq_bot_or_exists_atom_le : ∀ (b : α), b = ⊥ ∨ ∃ (a : α), is_atom a ∧ a ≤ b)
+
+/-- A lattice is coatomic iff every element other than `⊤` has a coatom above it. -/
+class is_coatomic : Prop :=
+(eq_top_or_exists_le_coatom : ∀ (b : α), b = ⊤ ∨ ∃ (a : α), is_coatom a ∧ b ≤ a)
+
+export is_atomic (eq_bot_or_exists_atom_le) is_coatomic (eq_top_or_exists_le_coatom)
+
+variable {α}
+
+@[simp] theorem is_coatomic_dual_iff_is_atomic : is_coatomic (order_dual α) ↔ is_atomic α :=
+⟨λ h, ⟨λ b, by apply h.eq_top_or_exists_le_coatom⟩, λ h, ⟨λ b, by apply h.eq_bot_or_exists_atom_le⟩⟩
+
+@[simp] theorem is_atomic_dual_iff_is_coatomic : is_atomic (order_dual α) ↔ is_coatomic α :=
+⟨λ h, ⟨λ b, by apply h.eq_bot_or_exists_atom_le⟩, λ h, ⟨λ b, by apply h.eq_top_or_exists_le_coatom⟩⟩
+
+namespace is_atomic
+
+instance is_coatomic_dual [h : is_atomic α] : is_coatomic (order_dual α) :=
+is_coatomic_dual_iff_is_atomic.2 h
+
+variables [is_atomic α]
+
+instance {x : α} : is_atomic (set.Iic x) :=
+⟨λ ⟨y, hy⟩, (eq_bot_or_exists_atom_le y).imp subtype.mk_eq_mk.2
+  (λ ⟨a, ha, hay⟩, ⟨⟨a, hay.trans hy⟩, ha.Iic (hay.trans hy), hay⟩)⟩
+
+end is_atomic
+
+namespace is_coatomic
+instance is_coatomic [h : is_coatomic α] : is_atomic (order_dual α) :=
+is_atomic_dual_iff_is_coatomic.2 h
+
+variables [is_coatomic α]
+
+instance {x : α} : is_coatomic (set.Ici x) :=
+⟨λ ⟨y, hy⟩, (eq_top_or_exists_le_coatom y).imp subtype.mk_eq_mk.2
+  (λ ⟨a, ha, hay⟩, ⟨⟨a, le_trans hy hay⟩, ha.Ici (le_trans hy hay), hay⟩)⟩
+
+end is_coatomic
+
+theorem is_atomic_iff_forall_is_atomic_Iic :
+  is_atomic α ↔ ∀ (x : α), is_atomic (set.Iic x) :=
+⟨@is_atomic.set.Iic.is_atomic _ _, λ h, ⟨λ x, ((@eq_bot_or_exists_atom_le _ _ (h x))
+  (⊤ : set.Iic x)).imp subtype.mk_eq_mk.1 (exists_imp_exists' coe
+  (λ ⟨a, ha⟩, and.imp_left (is_atom.of_is_atom_coe_Iic)))⟩⟩
+
+theorem is_coatomic_iff_forall_is_coatomic_Ici :
+  is_coatomic α ↔ ∀ (x : α), is_coatomic (set.Ici x) :=
+is_atomic_dual_iff_is_coatomic.symm.trans $ is_atomic_iff_forall_is_atomic_Iic.trans $ forall_congr
+  (λ x, is_coatomic_dual_iff_is_atomic.symm.trans iff.rfl)
+
+end atomic
+
+section atomistic
+
+variables (α) [complete_lattice α]
+
+/-- A lattice is atomistic iff every element is a `Sup` of a set of atoms. -/
+class is_atomistic : Prop :=
+(eq_Sup_atoms : ∀ (b : α), ∃ (s : set α), b = Sup s ∧ ∀ a, a ∈ s → is_atom a)
+
+/-- A lattice is coatomistic iff every element is an `Inf` of a set of coatoms. -/
+class is_coatomistic: Prop :=
+(eq_Inf_coatoms : ∀ (b : α), ∃ (s : set α), b = Inf s ∧ ∀ a, a ∈ s → is_coatom a)
+
+export is_atomistic (eq_Sup_atoms) is_coatomistic (eq_Inf_coatoms)
+
+variable {α}
+
+@[simp]
+theorem is_coatomistic_dual_iff_is_atomistic : is_coatomistic (order_dual α) ↔ is_atomistic α :=
+⟨λ h, ⟨λ b, by apply h.eq_Inf_coatoms⟩, λ h, ⟨λ b, by apply h.eq_Sup_atoms⟩⟩
+
+@[simp]
+theorem is_atomistic_dual_iff_is_coatomistic : is_atomistic (order_dual α) ↔ is_coatomistic α :=
+⟨λ h, ⟨λ b, by apply h.eq_Sup_atoms⟩, λ h, ⟨λ b, by apply h.eq_Inf_coatoms⟩⟩
+
+namespace is_atomistic
+
+instance is_coatomistic_dual [h : is_atomistic α] : is_coatomistic (order_dual α) :=
+is_coatomistic_dual_iff_is_atomistic.2 h
+
+variable [is_atomistic α]
+
+@[priority 100]
+instance : is_atomic α :=
+⟨λ b, by { rcases eq_Sup_atoms b with ⟨s, rfl, hs⟩,
+  cases s.eq_empty_or_nonempty with h h,
+  { simp [h] },
+  { exact or.intro_right _ ⟨h.some, hs _ h.some_spec, le_Sup h.some_spec⟩ } } ⟩
+
+end is_atomistic
+
+namespace is_coatomistic
+
+instance is_atomistic_dual [h : is_coatomistic α] : is_atomistic (order_dual α) :=
+is_atomistic_dual_iff_is_coatomistic.2 h
+
+variable [is_coatomistic α]
+
+@[priority 100]
+instance : is_coatomic α :=
+⟨λ b, by { rcases eq_Inf_coatoms b with ⟨s, rfl, hs⟩,
+  cases s.eq_empty_or_nonempty with h h,
+  { simp [h] },
+  { exact or.intro_right _ ⟨h.some, hs _ h.some_spec, Inf_le h.some_spec⟩ } } ⟩
+
+end is_coatomistic
+end atomistic
+
 /-- A lattice is simple iff it has only two elements, `⊥` and `⊤`. -/
 class is_simple_lattice (α : Type*) [bounded_lattice α] extends nontrivial α : Prop :=
 (eq_bot_or_eq_top : ∀ (a : α), a = ⊥ ∨ a = ⊤)
@@ -121,7 +259,7 @@ is_simple_lattice_iff_is_simple_lattice_order_dual.1 (by apply_instance)
 @[simp] lemma is_atom_top : is_atom (⊤ : α) :=
 ⟨top_ne_bot, λ a ha, or.resolve_right (eq_bot_or_eq_top a) (ne_of_lt ha)⟩
 
-@[simp] lemma is_coatom_bot : is_coatom (⊥ : α) := is_coatom_iff_is_atom_dual.2 is_atom_top
+@[simp] lemma is_coatom_bot : is_coatom (⊥ : α) := is_atom_dual_iff_is_coatom.1 is_atom_top
 
 end is_simple_lattice
 
@@ -135,6 +273,13 @@ instance : bounded_distrib_lattice α :=
 { le_sup_inf := λ x y z, by { rcases eq_bot_or_eq_top x with rfl | rfl; simp },
   .. (infer_instance : bounded_lattice α) }
 
+@[priority 100]
+instance : is_atomic α :=
+⟨λ b, (eq_bot_or_eq_top b).imp_right (λ h, ⟨⊤, ⟨is_atom_top, ge_of_eq h⟩⟩)⟩
+
+@[priority 100]
+instance : is_coatomic α := is_atomic_dual_iff_is_coatomic.1 is_simple_lattice.is_atomic
+
 section decidable_eq
 variable [decidable_eq α]
 
@@ -203,6 +348,18 @@ protected noncomputable def complete_boolean_algebra : complete_boolean_algebra
 
 end is_simple_lattice
 
+namespace is_simple_lattice
+variables [complete_lattice α] [is_simple_lattice α]
+set_option default_priority 100
+
+instance : is_atomistic α :=
+⟨λ b, (eq_bot_or_eq_top b).elim
+  (λ h, ⟨∅, ⟨h.trans Sup_empty.symm, λ a ha, false.elim (set.not_mem_empty _ ha)⟩⟩)
+  (λ h, ⟨{⊤}, h.trans Sup_singleton.symm, λ a ha, (set.mem_singleton_iff.1 ha).symm ▸ is_atom_top⟩)⟩
+
+instance : is_coatomistic α := is_atomistic_dual_iff_is_coatomistic.1 is_simple_lattice.is_atomistic
+
+end is_simple_lattice
 namespace fintype
 namespace is_simple_lattice
 variables [bounded_lattice α] [is_simple_lattice α] [decidable_eq α]