feat(Order/Atoms): strong atomicity typeclass (#14004)

A strongly atomic preorder is one in which every nontrivial interval `[a,b]` contains an element covering `a`, or equivalently an order where every closed interval is atomic. We add a new typeclass `IsStronglyAtomic` to capture this.

We provide instances of this typeclass for `SuccOrder`s, orders with `WellFoundedLT`, atomistic upper-modular lattices, complemented atomic modular lattices, and `OrdConnected` subtypes. We also show that such orders are atomic.

We also provide the dual typeclass `IsStronglyCoatomic` and dual versions of all of the above.

Mathlib/Data/Fintype/Order.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Peter Nelson, Yaël Dillies
 -/
 import Mathlib.Data.Finset.Order
-import Mathlib.Order.Atoms.Finite
+import Mathlib.Order.Atoms
+import Mathlib.Data.Set.Finite
 
 #align_import data.fintype.order from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 

Mathlib/GroupTheory/Sylow.lean

@@ -8,7 +8,6 @@ import Mathlib.Data.SetLike.Fintype
 import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.GroupTheory.PGroup
 import Mathlib.GroupTheory.NoncommPiCoprod
-import Mathlib.Order.Atoms.Finite
 import Mathlib.Data.Set.Lattice
 
 #align_import group_theory.sylow from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"

Mathlib/Order/Atoms.lean

@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 import Mathlib.Data.Set.Lattice
 import Mathlib.Order.ModularLattice
+import Mathlib.Order.SuccPred.Basic
 import Mathlib.Order.WellFounded
 import Mathlib.Tactic.Nontriviality
 
@@ -27,6 +28,8 @@ which are lattices with only two elements, and related ideas.
   * `IsCoatomic` indicates that every element other than `⊤` is below a coatom.
   * `IsAtomistic` indicates that every element is the `sSup` of a set of atoms.
   * `IsCoatomistic` indicates that every element is the `sInf` of a set of coatoms.
+  * `IsStronglyAtomic` indicates that for all `a < b`, there is some `x` with `a ⋖ x ≤ b`.
+  * `IsStronglyCoatomic` indicates that for all `a < b`, there is some `x` with `a ≤ x ⋖ b`.
 
 ### Simple Lattices
   * `IsSimpleOrder` indicates that an order has only two unique elements, `⊥` and `⊤`.
@@ -349,14 +352,110 @@ theorem isCoatomic_iff_forall_isCoatomic_Ici [OrderTop α] :
       forall_congr' fun _ => isCoatomic_dual_iff_isAtomic.symm.trans Iff.rfl
 #align is_coatomic_iff_forall_is_coatomic_Ici isCoatomic_iff_forall_isCoatomic_Ici
 
+section StronglyAtomic
+
+variable {α : Type*} {a b : α} [Preorder α]
+
+/-- An order is strongly atomic if every nontrivial interval `[a, b]`
+contains an element covering `a`. -/
+@[mk_iff]
+class IsStronglyAtomic (α : Type*) [Preorder α] : Prop where
+  exists_covBy_le_of_lt : ∀ (a b : α), a < b → ∃ x, a ⋖ x ∧ x ≤ b
+
+theorem exists_covBy_le_of_lt [IsStronglyAtomic α] (h : a < b) : ∃ x, a ⋖ x ∧ x ≤ b :=
+  IsStronglyAtomic.exists_covBy_le_of_lt a b h
+
+alias LT.lt.exists_covby_le := exists_covBy_le_of_lt
+
+/-- An order is strongly coatomic if every nontrivial interval `[a, b]`
+contains an element covered by `b`. -/
+@[mk_iff]
+class IsStronglyCoatomic (α : Type*) [Preorder α] : Prop where
+  (exists_le_covBy_of_lt : ∀ (a b : α), a < b → ∃ x, a ≤ x ∧ x ⋖ b)
+
+theorem exists_le_covBy_of_lt [IsStronglyCoatomic α] (h : a < b) : ∃ x, a ≤ x ∧ x ⋖ b :=
+  IsStronglyCoatomic.exists_le_covBy_of_lt a b h
+
+alias LT.lt.exists_le_covby := exists_le_covBy_of_lt
+
+theorem isStronglyAtomic_dual_iff_is_stronglyCoatomic :
+    IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α := by
+  simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall,
+    OrderDual.toDual_le_toDual, and_comm, isStronglyCoatomic_iff] using forall_comm
+
+@[simp] theorem isStronglyCoatomic_dual_iff_is_stronglyAtomic :
+    IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α := by
+  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; rfl
+
+instance OrderDual.instIsStronglyCoatomic [IsStronglyAtomic α] : IsStronglyCoatomic αᵒᵈ := by
+  rwa [isStronglyCoatomic_dual_iff_is_stronglyAtomic]
+
+instance [IsStronglyCoatomic α] : IsStronglyAtomic αᵒᵈ := by
+  rwa [isStronglyAtomic_dual_iff_is_stronglyCoatomic]
+
+instance IsStronglyAtomic.isAtomic (α : Type*) [PartialOrder α] [OrderBot α] [IsStronglyAtomic α] :
+    IsAtomic α where
+  eq_bot_or_exists_atom_le a := by
+    rw [or_iff_not_imp_left, ← Ne, ← bot_lt_iff_ne_bot]
+    refine fun hlt ↦ ?_
+    obtain ⟨x, hx, hxa⟩ := hlt.exists_covby_le
+    exact ⟨x, bot_covBy_iff.1 hx, hxa⟩
+
+instance IsStronglyCoatomic.toIsCoatomic (α : Type*) [PartialOrder α] [OrderTop α]
+    [IsStronglyCoatomic α] : IsCoatomic α :=
+  isAtomic_dual_iff_isCoatomic.1 <| IsStronglyAtomic.isAtomic (α := αᵒᵈ)
+
+theorem Set.OrdConnected.isStronglyAtomic [IsStronglyAtomic α] {s : Set α}
+    (h : Set.OrdConnected s) : IsStronglyAtomic s where
+  exists_covBy_le_of_lt := by
+    rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
+    obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le
+    exact ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
+      ⟨by simpa using hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using hy) (by simpa using hy')⟩, hxd⟩
+
+theorem Set.OrdConnected.isStronglyCoatomic [IsStronglyCoatomic α] {s : Set α}
+    (h : Set.OrdConnected s) : IsStronglyCoatomic s :=
+  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 h.dual.isStronglyAtomic
+
+instance [IsStronglyAtomic α] {s : Set α} [Set.OrdConnected s] : IsStronglyAtomic s :=
+  Set.OrdConnected.isStronglyAtomic <| by assumption
+
+instance [IsStronglyCoatomic α] {s : Set α} [h : Set.OrdConnected s] : IsStronglyCoatomic s :=
+  Set.OrdConnected.isStronglyCoatomic <| by assumption
+
+instance SuccOrder.toIsStronglyAtomic [SuccOrder α] : IsStronglyAtomic α where
+  exists_covBy_le_of_lt a _ hab :=
+    ⟨SuccOrder.succ a, Order.covBy_succ_of_not_isMax fun ha ↦ ha.not_lt hab,
+      SuccOrder.succ_le_of_lt hab⟩
+
+instance [PredOrder α] : IsStronglyCoatomic α := by
+  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; infer_instance
+
+end StronglyAtomic
+
 section WellFounded
 
+theorem IsStronglyAtomic.of_wellFounded_lt (h : WellFounded ((· < ·) : α → α → Prop)) :
+    IsStronglyAtomic α where
+  exists_covBy_le_of_lt a b hab := by
+    refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩
+    have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)
+    exact ⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
+      (Set.Ioc a b) ⟨b, hab,rfl.le⟩ ⟨hac, hlt.le.trans hmem.2⟩ hlt ⟩, hmem.2⟩
+
+theorem IsStronglyCoatomic.of_wellFounded_gt (h : WellFounded ((· > ·) : α → α → Prop)) :
+    IsStronglyCoatomic α :=
+  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| IsStronglyAtomic.of_wellFounded_lt (α := αᵒᵈ) h
+
+instance [WellFoundedLT α] : IsStronglyAtomic α :=
+  IsStronglyAtomic.of_wellFounded_lt wellFounded_lt
+
+instance [WellFoundedGT α] : IsStronglyCoatomic α :=
+    IsStronglyCoatomic.of_wellFounded_gt wellFounded_gt
+
 theorem isAtomic_of_orderBot_wellFounded_lt [OrderBot α]
     (h : WellFounded ((· < ·) : α → α → Prop)) : IsAtomic α :=
-  ⟨fun a =>
-    or_iff_not_imp_left.2 fun ha =>
-      let ⟨b, hb, hm⟩ := h.has_min { b | b ≠ ⊥ ∧ b ≤ a } ⟨a, ha, le_rfl⟩
-      ⟨b, ⟨hb.1, fun c => not_imp_not.1 fun hc hl => hm c ⟨hc, hl.le.trans hb.2⟩ hl⟩, hb.2⟩⟩
+  (IsStronglyAtomic.of_wellFounded_lt h).isAtomic
 #align is_atomic_of_order_bot_well_founded_lt isAtomic_of_orderBot_wellFounded_lt
 
 theorem isCoatomic_of_orderTop_gt_wellFounded [OrderTop α]
@@ -937,6 +1036,32 @@ protected theorem isCoatomic_iff [OrderTop α] [OrderTop β] (f : α ≃o β) :
 #align order_iso.is_coatomic_iff OrderIso.isCoatomic_iff
 
 end OrderIso
+section CompleteLattice
+
+variable [CompleteLattice α]
+
+/-- A complete upper-modular lattice that is atomistic is strongly atomic.
+Not an instance to prevent loops. -/
+theorem CompleteLattice.isStronglyAtomic [IsUpperModularLattice α] [IsAtomistic α] :
+    IsStronglyAtomic α where
+  exists_covBy_le_of_lt a b hab := by
+    obtain ⟨s, rfl, h⟩ := eq_sSup_atoms b
+    refine by_contra fun hcon ↦ hab.not_le <| sSup_le_iff.2 fun x hx ↦ ?_
+    simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon
+    specialize hcon (x ⊔ a) (sup_le (le_sSup _ _ hx) hab.le)
+    obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)
+    · exact False.elim <| hcon <|
+        (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy
+    rwa [inf_eq_left] at h_inf
+
+/-- A complete lower-modular lattice that is coatomistic is strongly coatomic.
+Not an instance to prevent loops. -/
+theorem CompleteLattice.isStronglyCoatomic [IsLowerModularLattice α] [IsCoatomistic α] :
+    IsStronglyCoatomic α := by
+  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
+  exact CompleteLattice.isStronglyAtomic
+
+end CompleteLattice
 
 section IsModularLattice
 
@@ -983,6 +1108,36 @@ theorem isAtomic_iff_isCoatomic : IsAtomic α ↔ IsCoatomic α :=
     @isAtomic_of_isCoatomic_of_complementedLattice_of_isModular _ _ _ _ _ h⟩
 #align is_atomic_iff_is_coatomic isAtomic_iff_isCoatomic
 
+/-- A complemented modular atomic lattice is strongly atomic.
+Not an instance to prevent loops. -/
+theorem ComplementedLattice.isStronglyAtomic [IsAtomic α] : IsStronglyAtomic α where
+  exists_covBy_le_of_lt a b hab := by
+    obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩
+    obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'
+    · obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint
+      exact False.elim <| hab.ne rfl
+    refine ⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩
+    convert hd.1.bot_covBy
+    rw [← le_bot_iff, ← show a ⊓ a' = ⊥ by simpa using Subtype.coe_inj.2 ha'.inf_eq_bot, inf_comm]
+    exact inf_le_inf_left _ hd.2
+
+/-- A complemented modular coatomic lattice is strongly coatomic.
+Not an instance to prevent loops. -/
+theorem ComplementedLattice.isStronglyCoatomic [IsCoatomic α] : IsStronglyCoatomic α :=
+  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| ComplementedLattice.isStronglyAtomic
+
+/-- A complemented modular atomic lattice is strongly coatomic.
+Not an instance to prevent loops. -/
+theorem ComplementedLattice.isStronglyAtomic' [h : IsAtomic α] : IsStronglyCoatomic α := by
+  rw [isAtomic_iff_isCoatomic] at h
+  exact isStronglyCoatomic
+
+/-- A complemented modular coatomic lattice is strongly atomic.
+Not an instance to prevent loops. -/
+theorem ComplementedLattice.isStronglyCoatomic' [h : IsCoatomic α] : IsStronglyAtomic α := by
+  rw [← isAtomic_iff_isCoatomic] at h
+  exact isStronglyAtomic
+
 end IsModularLattice
 
 namespace «Prop»

Mathlib/Order/Atoms/Finite.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import Mathlib.Data.Set.Finite
+import Mathlib.Order.Interval.Finset.Defs
 import Mathlib.Order.Atoms
 
 #align_import order.atoms.finite from "leanprover-community/mathlib"@"d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce"
@@ -90,3 +90,40 @@ instance (priority := 100) Finite.to_isAtomic [PartialOrder α] [OrderBot α] [F
 #align finite.to_is_atomic Finite.to_isAtomic
 
 end Fintype
+
+section LocallyFinite
+
+variable [Preorder α] [LocallyFiniteOrder α]
+
+instance : IsStronglyAtomic α where
+  exists_covBy_le_of_lt a b hab := by
+    obtain ⟨x, hxmem, hx⟩ := (LocallyFiniteOrder.finsetIoc a b).exists_minimal
+      ⟨b, by simpa [LocallyFiniteOrder.finset_mem_Ioc]⟩
+    simp only [LocallyFiniteOrder.finset_mem_Ioc, and_imp] at hxmem hx
+    exact ⟨x, ⟨hxmem.1, fun c hac hcx ↦ hx _ hac (hcx.le.trans hxmem.2) hcx⟩, hxmem.2⟩
+
+instance : IsStronglyCoatomic α := by
+  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; infer_instance
+
+end LocallyFinite
+
+section IsStronglyAtomic
+
+variable [PartialOrder α] {a : α}
+
+theorem exists_covby_infinite_Ici_of_infinite_Ici [IsStronglyAtomic α]
+    (ha : (Set.Ici a).Infinite) (hfin : {x | a ⋖ x}.Finite) :
+    ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite := by
+  by_contra! h
+  refine ((hfin.biUnion (t := Set.Ici) (by simpa using h)).subset (fun b hb ↦ ?_)).not_infinite
+    (ha.diff (Set.finite_singleton a))
+  obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le
+  exact Set.mem_biUnion hax hxb
+
+theorem exists_covby_infinite_Iic_of_infinite_Iic [IsStronglyCoatomic α]
+    (ha : (Set.Iic a).Infinite) (hfin : {x | x ⋖ a}.Finite) :
+    ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite := by
+  simp_rw [← toDual_covBy_toDual_iff (α := α)] at hfin ⊢
+  exact exists_covby_infinite_Ici_of_infinite_Ici (α := αᵒᵈ) ha hfin
+
+end IsStronglyAtomic