feat(order/atoms): further facts about atoms, coatoms, and simple lattices (#5493)

Provides possible instances of `bounded_distrib_lattice`, `boolean_algebra`, `complete_lattice`, and `complete_boolean_algebra` on a simple lattice
Relates the `is_atom` and `is_coatom` conditions to `is_simple_lattice` structures on intervals
Shows that all three conditions are preserved by `order_iso`s
Adds more instances on `bool`, including `is_simple_lattice`



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

Author: awainverse

src/data/bool.lean

@@ -160,6 +160,12 @@ instance : linear_order bool :=
 
 namespace bool
 
+@[simp] lemma ff_le {x : bool} : ff ≤ x := or.intro_left _ rfl
+
+@[simp] lemma le_tt {x : bool} : x ≤ tt := or.intro_right _ rfl
+
+@[simp] lemma ff_lt_tt : ff < tt := lt_of_le_of_ne ff_le ff_ne_tt
+
 /-- convert a `bool` to a `ℕ`, `false -> 0`, `true -> 1` -/
 def to_nat (b : bool) : ℕ :=
 cond b 1 0

src/logic/nontrivial.lean

@@ -261,3 +261,9 @@ add_tactic_doc
   tags                     := ["logic", "type class"] }
 
 end tactic.interactive
+
+namespace bool
+
+instance : nontrivial bool := ⟨⟨tt,ff, tt_eq_ff_eq_false⟩⟩
+
+end bool

src/order/atoms.lean

@@ -4,8 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author:  Aaron Anderson.
 -/
 
-import order.bounded_lattice
+import order.complete_boolean_algebra
 import order.order_dual
+import order.lattice_intervals
+import order.rel_iso
+import data.fintype.basic
 
 /-!
 # Atoms, Coatoms, and Simple Lattices
@@ -14,9 +17,25 @@ This module defines atoms, which are minimal non-`⊥` elements in bounded latti
 which are lattices with only two elements, and related ideas.
 
 ## Main definitions
+
+### Atoms and Coatoms
   * `is_atom a` indicates that the only element below `a` is `⊥`.
   * `is_coatom a` indicates that the only element above `a` is `⊤`.
+
+### Simple Lattices
   * `is_simple_lattice` indicates that a bounded lattice has only two elements, `⊥` and `⊤`.
+  * `is_simple_lattice.bounded_distrib_lattice`
+  * Given an instance of `is_simple_lattice`, we provide the following definitions. These are not
+    made global instances as they contain data :
+    * `is_simple_lattice.boolean_algebra`
+    * `is_simple_lattice.complete_lattice`
+    * `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
+   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
 
 -/
 
@@ -108,6 +127,113 @@ is_simple_lattice_iff_is_simple_lattice_order_dual.1 (by apply_instance)
 
 end is_simple_lattice
 
+namespace is_simple_lattice
+
+variables [bounded_lattice α] [is_simple_lattice α]
+
+/-- A simple `bounded_lattice` is also distributive. -/
+@[priority 100]
+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 α) }
+
+section decidable_eq
+variable [decidable_eq α]
+
+/-- Every simple lattice is order-isomorphic to `bool`. -/
+def order_iso_bool : α ≃o bool :=
+{ to_fun := λ x, x = ⊤,
+  inv_fun := λ x, cond x ⊤ ⊥,
+  left_inv := λ x, by { rcases (eq_bot_or_eq_top x) with rfl | rfl; simp [bot_ne_top] },
+  right_inv := λ x, by { cases x; simp [bot_ne_top] },
+  map_rel_iff' := λ a b, begin
+    rcases (eq_bot_or_eq_top a) with rfl | rfl,
+    { simp [bot_ne_top] },
+    { rcases (eq_bot_or_eq_top b) with rfl | rfl,
+      { simp [bot_ne_top.symm, bot_ne_top, bool.ff_lt_tt] },
+      { simp [bot_ne_top] } }
+  end }
+
+@[priority 200]
+instance : fintype α := fintype.of_equiv bool (order_iso_bool.to_equiv).symm
+
+/-- A simple `bounded_lattice` is also a `boolean_algebra`. -/
+protected def boolean_algebra : boolean_algebra α :=
+{ compl := λ x, if x = ⊥ then ⊤ else ⊥,
+  sdiff := λ x y, if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥,
+  sdiff_eq := λ x y, by { rcases eq_bot_or_eq_top x with rfl | rfl; simp [bot_ne_top] },
+  inf_compl_le_bot := λ x, by { rcases eq_bot_or_eq_top x with rfl | rfl; simp },
+  top_le_sup_compl := λ x, by { rcases eq_bot_or_eq_top x with rfl | rfl; simp },
+  .. is_simple_lattice.bounded_distrib_lattice }
+
+end decidable_eq
+
+open_locale classical
+
+/-- A simple `bounded_lattice` is also complete. -/
+protected noncomputable def complete_lattice : complete_lattice α :=
+{ Sup := λ s, if ⊤ ∈ s then ⊤ else ⊥,
+  Inf := λ s, if ⊥ ∈ s then ⊥ else ⊤,
+  le_Sup := λ s x h, by { rcases eq_bot_or_eq_top x with rfl | rfl,
+    { exact bot_le },
+    { rw if_pos h } },
+  Sup_le := λ s x h, by { rcases eq_bot_or_eq_top x with rfl | rfl,
+    { rw if_neg,
+      intro con,
+      exact bot_ne_top (eq_top_iff.2 (h ⊤ con)) },
+    { exact le_top } },
+  Inf_le := λ s x h, by { rcases eq_bot_or_eq_top x with rfl | rfl,
+    { rw if_pos h },
+    { exact le_top } },
+  le_Inf := λ s x h, by { rcases eq_bot_or_eq_top x with rfl | rfl,
+    { exact bot_le },
+    { rw if_neg,
+      intro con,
+      exact top_ne_bot (eq_bot_iff.2 (h ⊥ con)) } },
+  .. (infer_instance : bounded_lattice α) }
+
+/-- A simple `bounded_lattice` is also a `complete_boolean_algebra`. -/
+protected noncomputable def complete_boolean_algebra : complete_boolean_algebra α :=
+{ infi_sup_le_sup_Inf := λ x s, by { rcases eq_bot_or_eq_top x with rfl | rfl,
+    { simp only [bot_sup_eq, ← Inf_eq_infi], apply le_refl },
+    { simp only [top_sup_eq, le_top] }, },
+  inf_Sup_le_supr_inf := λ x s, by { rcases eq_bot_or_eq_top x with rfl | rfl,
+    { simp only [bot_inf_eq, bot_le] },
+    { simp only [top_inf_eq, ← Sup_eq_supr], apply le_refl } },
+  .. is_simple_lattice.complete_lattice,
+  .. is_simple_lattice.boolean_algebra }
+
+end is_simple_lattice
+
+namespace fintype
+namespace is_simple_lattice
+variables [bounded_lattice α] [is_simple_lattice α] [decidable_eq α]
+
+lemma univ : (finset.univ : finset α) = {⊤, ⊥} :=
+begin
+  change finset.map _ (finset.univ : finset bool) = _,
+  rw fintype.univ_bool,
+  simp only [finset.map_insert, function.embedding.coe_fn_mk, finset.map_singleton],
+  refl,
+end
+
+lemma card : fintype.card α = 2 :=
+(fintype.of_equiv_card _).trans fintype.card_bool
+
+end is_simple_lattice
+end fintype
+
+namespace bool
+
+instance : is_simple_lattice bool :=
+⟨λ a, begin
+  rw [← finset.mem_singleton, or.comm, ← finset.mem_insert,
+      top_eq_tt, bot_eq_ff, ← fintype.univ_bool],
+  apply finset.mem_univ,
+end⟩
+
+end bool
+
 theorem is_simple_lattice_iff_is_atom_top [bounded_lattice α] :
   is_simple_lattice α ↔ is_atom (⊤ : α) :=
 ⟨λ h, @is_atom_top _ _ h, λ h, {
@@ -116,4 +242,46 @@ theorem is_simple_lattice_iff_is_atom_top [bounded_lattice α] :
 
 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
+is_simple_lattice_iff_is_simple_lattice_order_dual.trans is_simple_lattice_iff_is_atom_top
+
+namespace set
+
+theorem is_simple_lattice_Iic_iff_is_atom [bounded_lattice α] {a : α} :
+  is_simple_lattice (Iic a) ↔ is_atom a :=
+is_simple_lattice_iff_is_atom_top.trans $ and_congr (not_congr subtype.mk_eq_mk)
+  ⟨λ h b ab, subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab),
+    λ h ⟨b, hab⟩ hbotb, subtype.mk_eq_mk.2 (h b (subtype.mk_lt_mk.1 hbotb))⟩
+
+theorem is_simple_lattice_Ici_iff_is_coatom [bounded_lattice α] {a : α} :
+  is_simple_lattice (Ici a) ↔ is_coatom a :=
+is_simple_lattice_iff_is_coatom_bot.trans $ and_congr (not_congr subtype.mk_eq_mk)
+  ⟨λ h b ab, subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab),
+    λ h ⟨b, hab⟩ hbotb, subtype.mk_eq_mk.2 (h b (subtype.mk_lt_mk.1 hbotb))⟩
+
+end set
+
+namespace order_iso
+
+variables [bounded_lattice α] {β : Type*} [bounded_lattice β] (f : α ≃o β)
+include f
+
+@[simp] lemma is_atom_iff (a : α) : is_atom (f a) ↔ is_atom a :=
+and_congr (not_congr ⟨λ h, f.injective (f.map_bot.symm ▸ h), λ h, f.map_bot ▸ (congr rfl h)⟩)
+  ⟨λ h b hb, f.injective ((h (f b) ((f : α ↪o β).lt_iff_lt.2 hb)).trans f.map_bot.symm),
+  λ h b hb, f.symm.injective begin
+    rw f.symm.map_bot,
+    apply h,
+    rw [← f.symm_apply_apply a],
+    exact (f.symm : β ↪o α).lt_iff_lt.2 hb,
+  end⟩
+
+@[simp] lemma is_coatom_iff (a : α) : is_coatom (f a) ↔ is_coatom a := f.dual.is_atom_iff a
+
+lemma is_simple_lattice_iff (f : α ≃o β) : is_simple_lattice α ↔ is_simple_lattice β :=
+by rw [is_simple_lattice_iff_is_atom_top, is_simple_lattice_iff_is_atom_top,
+  ← f.is_atom_iff ⊤, f.map_top]
+
+lemma is_simple_lattice [h : is_simple_lattice β] (f : α ≃o β) : is_simple_lattice α :=
+f.is_simple_lattice_iff.mpr h
+
+end order_iso

src/order/bounded_lattice.lean

@@ -826,24 +826,6 @@ end with_top
 
 namespace subtype
 
-/-- A subtype forms a `⊔`-semilattice if `⊔` preserves the property. -/
-protected def semilattice_sup [semilattice_sup α] {P : α → Prop}
-  (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) : semilattice_sup {x : α // P x} :=
-{ sup := λ x y, ⟨x.1 ⊔ y.1, Psup x.2 y.2⟩,
-  le_sup_left := λ x y, @le_sup_left _ _ (x : α) y,
-  le_sup_right := λ x y, @le_sup_right _ _ (x : α) y,
-  sup_le := λ x y z h1 h2, @sup_le α _ _ _ _ h1 h2,
-  ..subtype.partial_order P }
-
-/-- A subtype forms a `⊓`-semilattice if `⊓` preserves the property. -/
-protected def semilattice_inf [semilattice_inf α] {P : α → Prop}
-  (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y)) : semilattice_inf {x : α // P x} :=
-{ inf := λ x y, ⟨x.1 ⊓ y.1, Pinf x.2 y.2⟩,
-  inf_le_left := λ x y, @inf_le_left _ _ (x : α) y,
-  inf_le_right := λ x y, @inf_le_right _ _ (x : α) y,
-  le_inf := λ x y z h1 h2, @le_inf α _ _ _ _ h1 h2,
-  ..subtype.partial_order P }
-
 /-- A subtype forms a `⊔`-`⊥`-semilattice if `⊥` and `⊔` preserve the property. -/
 protected def semilattice_sup_bot [semilattice_sup_bot α] {P : α → Prop}
   (Pbot : P ⊥) (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) : semilattice_sup_bot {x : α // P x} :=
@@ -865,12 +847,6 @@ protected def semilattice_inf_top [semilattice_inf_top α] {P : α → Prop}
   le_top := λ x, @le_top α _ x,
   ..subtype.semilattice_inf Pinf }
 
-/-- A subtype forms a lattice if `⊔` and `⊓` preserve the property. -/
-protected def lattice [lattice α] {P : α → Prop}
-  (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y)) :
-  lattice {x : α // P x} :=
-{ ..subtype.semilattice_inf Pinf, ..subtype.semilattice_sup Psup }
-
 end subtype
 
 namespace order_dual
@@ -1125,3 +1101,22 @@ lemma bot_ne_top : (⊥ : α) ≠ ⊤ :=
 lemma top_ne_bot : (⊤ : α) ≠ ⊥ := ne.symm bot_ne_top
 
 end nontrivial
+
+namespace bool
+
+instance : bounded_lattice bool :=
+{ top := tt,
+  le_top := λ x, le_tt,
+  bot := ff,
+  bot_le := λ x, ff_le,
+  .. (infer_instance : lattice bool)}
+
+end bool
+
+section bool
+
+@[simp] lemma top_eq_tt : ⊤ = tt := rfl
+
+@[simp] lemma bot_eq_ff : ⊥ = ff := rfl
+
+end bool

src/order/lattice.lean

@@ -480,3 +480,31 @@ instance [distrib_lattice α] [distrib_lattice β] : distrib_lattice (α × β)
   .. prod.lattice α β }
 
 end prod
+
+namespace subtype
+
+/-- A subtype forms a `⊔`-semilattice if `⊔` preserves the property. -/
+protected def semilattice_sup [semilattice_sup α] {P : α → Prop}
+  (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) : semilattice_sup {x : α // P x} :=
+{ sup := λ x y, ⟨x.1 ⊔ y.1, Psup x.2 y.2⟩,
+  le_sup_left := λ x y, @le_sup_left _ _ (x : α) y,
+  le_sup_right := λ x y, @le_sup_right _ _ (x : α) y,
+  sup_le := λ x y z h1 h2, @sup_le α _ _ _ _ h1 h2,
+  ..subtype.partial_order P }
+
+/-- A subtype forms a `⊓`-semilattice if `⊓` preserves the property. -/
+protected def semilattice_inf [semilattice_inf α] {P : α → Prop}
+  (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y)) : semilattice_inf {x : α // P x} :=
+{ inf := λ x y, ⟨x.1 ⊓ y.1, Pinf x.2 y.2⟩,
+  inf_le_left := λ x y, @inf_le_left _ _ (x : α) y,
+  inf_le_right := λ x y, @inf_le_right _ _ (x : α) y,
+  le_inf := λ x y z h1 h2, @le_inf α _ _ _ _ h1 h2,
+  ..subtype.partial_order P }
+
+/-- A subtype forms a lattice if `⊔` and `⊓` preserve the property. -/
+protected def lattice [lattice α] {P : α → Prop}
+  (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y)) :
+  lattice {x : α // P x} :=
+{ ..subtype.semilattice_inf Pinf, ..subtype.semilattice_sup Psup }
+
+end subtype