feat(order/bounded_lattice): define atoms, coatoms, and simple lattices (#5471)

Defines `is_atom`, `is_coatom`, and `is_simple_lattice`
Refactors `ideal.is_maximal` to use `is_coatom`, the new definition is definitionally equal to the old one



Co-authored-by: Johan Commelin <johan@commelin.net>

Author: awainverse

src/order/atoms.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2020 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author:  Aaron Anderson.
+-/
+
+import order.bounded_lattice
+import order.order_dual
+
+/-!
+# Atoms, Coatoms, and Simple Lattices
+
+This module defines atoms, which are minimal non-`⊥` elements in bounded lattices, simple lattices,
+which are lattices with only two elements, and related ideas.
+
+## Main definitions
+  * `is_atom a` indicates that the only element below `a` is `⊥`.
+  * `is_coatom a` indicates that the only element above `a` is `⊤`.
+  * `is_simple_lattice` indicates that a bounded lattice has only two elements, `⊥` and `⊤`.
+
+-/
+
+variable {α : Type*}
+
+section atoms
+
+section is_atom
+
+variable [order_bot α]
+
+/-- An atom of an `order_bot` is an element with no other element between it and `⊥`,
+  which is not `⊥`. -/
+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)
+
+end is_atom
+
+section is_coatom
+
+variable [order_top α]
+
+/-- A coatom of an `order_top` is an element with no other element between it and `⊤`,
+  which is not `⊤`. -/
+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)
+
+end is_coatom
+
+variables [bounded_lattice α] {a : α}
+
+lemma is_atom_iff_is_coatom_dual : is_atom a ↔ is_coatom (order_dual.to_dual a) := iff.refl _
+
+lemma is_coatom_iff_is_atom_dual : is_coatom a ↔ is_atom (order_dual.to_dual a) := iff.refl _
+
+end atoms
+
+/-- 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 = ⊤)
+
+export is_simple_lattice (eq_bot_or_eq_top)
+
+theorem is_simple_lattice_iff_is_simple_lattice_order_dual [bounded_lattice α] :
+  is_simple_lattice α ↔ is_simple_lattice (order_dual α) :=
+begin
+  split; intro i; haveI := i,
+  { exact { exists_pair_ne := @exists_pair_ne α _,
+      eq_bot_or_eq_top := λ a, or.symm (eq_bot_or_eq_top ((order_dual.of_dual a)) : _ ∨ _) } },
+  { exact { exists_pair_ne := @exists_pair_ne (order_dual α) _,
+      eq_bot_or_eq_top := λ a, or.symm (eq_bot_or_eq_top (order_dual.to_dual a)) } }
+end
+
+section is_simple_lattice
+
+variables [bounded_lattice α] [is_simple_lattice α]
+
+instance : is_simple_lattice (order_dual α) :=
+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
+
+end is_simple_lattice
+
+theorem is_simple_lattice_iff_is_atom_top [bounded_lattice α] :
+  is_simple_lattice α ↔ is_atom (⊤ : α) :=
+⟨λ h, @is_atom_top _ _ h, λ h, {
+  exists_pair_ne := ⟨⊤, ⊥, h.1⟩,
+  eq_bot_or_eq_top := λ a, ((eq_or_lt_of_le (@le_top _ _ a)).imp_right (h.2 a)).symm }⟩
+
+theorem is_simple_lattice_iff_is_coatom_bot [bounded_lattice α] :
+  is_simple_lattice α ↔ is_coatom (⊥ : α) :=
+iff.trans is_simple_lattice_iff_is_simple_lattice_order_dual is_simple_lattice_iff_is_atom_top

src/order/bounded_lattice.lean

@@ -10,6 +10,7 @@ Includes the Prop and fun instances.
 import order.lattice
 import data.option.basic
 import tactic.pi_instances
+import logic.nontrivial
 
 set_option old_structure_cmd true
 
@@ -1010,6 +1011,8 @@ end bounded_distrib_lattice
 
 end disjoint
 
+section is_compl
+
 /-!
 ### `is_compl` predicate
 -/
@@ -1100,3 +1103,16 @@ is_compl.of_eq bot_inf_eq sup_top_eq
 
 lemma is_compl_top_bot [bounded_lattice α] : is_compl (⊤ : α) ⊥ :=
 is_compl.of_eq inf_bot_eq top_sup_eq
+
+end is_compl
+
+section nontrivial
+
+variables [bounded_lattice α] [nontrivial α]
+
+lemma bot_ne_top : (⊥ : α) ≠ ⊤ :=
+λ H, not_nontrivial_iff_subsingleton.mpr (subsingleton_of_bot_eq_top H) ‹_›
+
+lemma top_ne_bot : (⊤ : α) ≠ ⊥ := ne.symm bot_ne_top
+
+end nontrivial

src/order/order_dual.lean

@@ -24,6 +24,8 @@ variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
 namespace order_dual
 
+instance [nontrivial α] : nontrivial (order_dual α) := by delta order_dual; assumption
+
 /-- `to_dual` is the identity function to the `order_dual` of a linear order.  -/
 def to_dual : α ≃ order_dual α := ⟨id, id, λ h, rfl, λ h, rfl⟩
 

src/ring_theory/ideal/basic.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau, Chris Hughes, Mario Carneiro
 import algebra.associated
 import linear_algebra.basic
 import order.zorn
+import order.atoms
 /-!
 
 # Ideals over a ring
@@ -197,8 +198,7 @@ lemma bot_prime {R : Type*} [integral_domain R] : (⊥ : ideal R).is_prime :=
  λ x y h, mul_eq_zero.mp (by simpa only [submodule.mem_bot] using h)⟩
 
 /-- An ideal is maximal if it is maximal in the collection of proper ideals. -/
-@[class] def is_maximal (I : ideal α) : Prop :=
-I ≠ ⊤ ∧ ∀ J, I < J → J = ⊤
+@[class] def is_maximal (I : ideal α) : Prop := is_coatom I
 
 theorem is_maximal_iff {I : ideal α} : I.is_maximal ↔
   (1:α) ∉ I ∧ ∀ (J : ideal α) x, I ≤ J → x ∉ I → x ∈ J → (1:α) ∈ J :=