From bf2750e52ef716079c5ecd0f1fbe0d525b0f86cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 14 May 2021 04:49:57 +0000 Subject: [PATCH] chore(order/atoms): ask for the correct instances (#7582) replace bounded_lattice by order_bot/order_top where it can --- src/order/atoms.lean | 64 +++++++++++++++++++++++++------------------- 1 file changed, 37 insertions(+), 27 deletions(-) diff --git a/src/order/atoms.lean b/src/order/atoms.lean index 0cb3134c286a0..5b0884c84a67a 100644 --- a/src/order/atoms.lean +++ b/src/order/atoms.lean @@ -109,44 +109,48 @@ or.elim (eq_top_or_eq_of_coatom_le ha le_sup_left) id end pairwise -variables [bounded_lattice α] {a : α} +variable {a : α} @[simp] -lemma is_coatom_dual_iff_is_atom : is_coatom (order_dual.to_dual a) ↔ is_atom a := iff.refl _ +lemma is_coatom_dual_iff_is_atom [order_bot α] : is_coatom (order_dual.to_dual a) ↔ is_atom a := +iff.rfl @[simp] -lemma is_atom_dual_iff_is_coatom : is_atom (order_dual.to_dual a) ↔ is_coatom a := iff.refl _ +lemma is_atom_dual_iff_is_coatom [order_top α] : is_atom (order_dual.to_dual a) ↔ is_coatom a := +iff.rfl end atoms section atomic -variables (α) [bounded_lattice α] +variable (α) /-- A lattice is atomic iff every element other than `⊥` has an atom below it. -/ -class is_atomic : Prop := +class is_atomic [order_bot α] : 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 := +class is_coatomic [order_top α] : 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 α := +@[simp] theorem is_coatomic_dual_iff_is_atomic [order_bot α] : + 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 α := +@[simp] theorem is_atomic_dual_iff_is_coatomic [order_top α] : + 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 [order_bot α] [is_atomic α] -variables [is_atomic α] +instance is_coatomic_dual : is_coatomic (order_dual α) := +is_coatomic_dual_iff_is_atomic.2 ‹is_atomic α› instance {x : α} : is_atomic (set.Iic x) := ⟨λ ⟨y, hy⟩, (eq_bot_or_exists_atom_le y).imp subtype.mk_eq_mk.2 @@ -155,10 +159,11 @@ instance {x : α} : is_atomic (set.Iic x) := 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 α] +variables [order_top α] [is_coatomic α] + +instance is_coatomic : is_atomic (order_dual α) := +is_atomic_dual_iff_is_coatomic.2 ‹is_coatomic α› instance {x : α} : is_coatomic (set.Ici x) := ⟨λ ⟨y, hy⟩, (eq_top_or_exists_le_coatom y).imp subtype.mk_eq_mk.2 @@ -166,13 +171,13 @@ instance {x : α} : is_coatomic (set.Ici x) := end is_coatomic -theorem is_atomic_iff_forall_is_atomic_Iic : +theorem is_atomic_iff_forall_is_atomic_Iic [order_bot α] : 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 : +theorem is_coatomic_iff_forall_is_coatomic_Ici [order_top α] : 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) @@ -188,7 +193,7 @@ 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 := +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) @@ -451,10 +456,8 @@ 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 := +@[simp] lemma is_atom_iff [order_bot α] {β : Type*} [order_bot β] (f : α ≃o β) (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 @@ -464,16 +467,22 @@ and_congr (not_congr ⟨λ h, f.injective (f.map_bot.symm ▸ h), λ h, f.map_bo 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 +@[simp] lemma is_coatom_iff [order_top α] {β : Type*} [order_top β] (f : α ≃o β) (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 β := +lemma is_simple_lattice_iff [bounded_lattice α] {β : Type*} [bounded_lattice β] (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 α := +lemma is_simple_lattice [bounded_lattice α] {β : Type*} [bounded_lattice β] + [h : is_simple_lattice β] (f : α ≃o β) : + is_simple_lattice α := f.is_simple_lattice_iff.mpr h -lemma is_atomic_iff : is_atomic α ↔ is_atomic β := +lemma is_atomic_iff [order_bot α] {β : Type*} [order_bot β] (f : α ≃o β) : + is_atomic α ↔ is_atomic β := begin suffices : (∀ b : α, b = ⊥ ∨ ∃ (a : α), is_atom a ∧ a ≤ b) ↔ (∀ b : β, b = ⊥ ∨ ∃ (a : β), is_atom a ∧ a ≤ b), @@ -489,9 +498,10 @@ begin rwa [←f.le_iff_le, f.apply_symm_apply], }, }, end -lemma is_coatomic_iff : is_coatomic α ↔ is_coatomic β := +lemma is_coatomic_iff [order_top α] {β : Type*} [order_top β] (f : α ≃o β) : + is_coatomic α ↔ is_coatomic β := by { rw [←is_atomic_dual_iff_is_coatomic, ←is_atomic_dual_iff_is_coatomic], - exact f.dual.is_atomic_iff, } + exact f.dual.is_atomic_iff } end order_iso