feat(order/bounded_order): Codisjointness (#14195)

Define `codisjoint`, the dual notion of `disjoint`. This is already used without a name in `is_compl`, and will soon be used for Heyting algebras.

src/linear_algebra/bilinear_form.lean

@@ -945,8 +945,8 @@ end
   is complement to its orthogonal complement. -/
 lemma is_compl_span_singleton_orthogonal {B : bilin_form K V}
   {x : V} (hx : ¬ B.is_ortho x x) : is_compl (K ∙ x) (B.orthogonal $ K ∙ x) :=
-{ inf_le_bot := eq_bot_iff.1 $ span_singleton_inf_orthogonal_eq_bot hx,
-  top_le_sup := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }
+{ disjoint := eq_bot_iff.1 $ span_singleton_inf_orthogonal_eq_bot hx,
+  codisjoint := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }
 
 end orthogonal
 
@@ -1137,14 +1137,11 @@ begin
     rintro ⟨n, hn⟩,
     rw [restrict_apply, submodule.coe_mk, submodule.coe_mk, b₁],
     exact hx₂ n hn },
-  refine ⟨this ▸ le_rfl, _⟩,
-  { rw top_le_iff,
-    refine eq_top_of_finrank_eq _,
-    refine le_antisymm (submodule.finrank_le _) _,
-    conv_rhs { rw ← add_zero (finrank K _) },
-    rw [← finrank_bot K V, ← this, submodule.dim_sup_add_dim_inf_eq,
-        finrank_add_finrank_orthogonal b₁],
-    exact nat.le.intro rfl }
+  refine is_compl.of_eq this (eq_top_of_finrank_eq $ (submodule.finrank_le _).antisymm _),
+  conv_rhs { rw ← add_zero (finrank K _) },
+  rw [← finrank_bot K V, ← this, submodule.dim_sup_add_dim_inf_eq,
+      finrank_add_finrank_orthogonal b₁],
+  exact le_self_add,
 end
 
 /-- A subspace is complement to its orthogonal complement with respect to some reflexive bilinear

src/linear_algebra/sesquilinear_form.lean

@@ -372,9 +372,8 @@ end
   is complement to its orthogonal complement. -/
 lemma is_compl_span_singleton_orthogonal {B : V →ₗ[K] V →ₗ[K] K}
   {x : V} (hx : ¬ B.is_ortho x x) : is_compl (K ∙ x) (submodule.orthogonal_bilin (K ∙ x) B) :=
-{ inf_le_bot := eq_bot_iff.1 $
-    (span_singleton_inf_orthogonal_eq_bot B x hx),
-  top_le_sup := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }
+{ disjoint := eq_bot_iff.1 $ span_singleton_inf_orthogonal_eq_bot B x hx,
+  codisjoint := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }
 
 end orthogonal
 

src/order/bounded_order.lean

@@ -33,11 +33,6 @@ instances for `Prop` and `fun`.
   `distrib_lattice` when `order_bot`.
 * Bounded and distributive lattice. Notated by `[distrib_lattice α] [bounded_order α]`.
   Typical examples include `Prop` and `set α`.
-
-## Implementation notes
-
-We didn't prove things about `[distrib_lattice α] [order_top α]` because the dual notion of
-`disjoint` isn't really used anywhere.
 -/
 
 open order_dual
@@ -1274,29 +1269,129 @@ hd.left_le_of_le_sup_right $ by rwa sup_comm
 end distrib_lattice_bot
 end disjoint
 
+section codisjoint
+section semilattice_sup_top
+variables [semilattice_sup α] [order_top α] {a b c d : α}
+
+/-- Two elements of a lattice are codisjoint if their sup is the top element. -/
+def codisjoint (a b : α) : Prop := ⊤ ≤ a ⊔ b
+
+lemma codisjoint_iff : codisjoint a b ↔ a ⊔ b = ⊤ := top_le_iff
+lemma codisjoint.eq_top : codisjoint a b → a ⊔ b = ⊤ := top_unique
+lemma codisjoint.comm : codisjoint a b ↔ codisjoint b a := by rw [codisjoint, codisjoint, sup_comm]
+@[symm] lemma codisjoint.symm ⦃a b : α⦄ : codisjoint a b → codisjoint b a := codisjoint.comm.1
+lemma symmetric_codisjoint : symmetric (codisjoint : α → α → Prop) := codisjoint.symm
+lemma codisjoint_assoc : codisjoint (a ⊔ b) c ↔ codisjoint a (b ⊔ c) :=
+by rw [codisjoint, codisjoint, sup_assoc]
+
+@[simp] lemma codisjoint_top_left : codisjoint ⊤ a := le_sup_left
+@[simp] lemma codisjoint_top_right : codisjoint a ⊤ := le_sup_right
+
+lemma codisjoint.mono (h₁ : a ≤ b) (h₂ : c ≤ d) : codisjoint a c → codisjoint b d :=
+le_trans' $ sup_le_sup h₁ h₂
+
+lemma codisjoint.mono_left (h : a ≤ b) : codisjoint a c → codisjoint b c := codisjoint.mono h le_rfl
+lemma codisjoint.mono_right : b ≤ c → codisjoint a b → codisjoint a c := codisjoint.mono le_rfl
+
+variables (c)
+
+lemma codisjoint.sup_left (h : codisjoint a b) : codisjoint (a ⊔ c) b := h.mono_left le_sup_left
+lemma codisjoint.sup_left' (h : codisjoint a b) : codisjoint (c ⊔ a) b := h.mono_left le_sup_right
+lemma codisjoint.sup_right (h : codisjoint a b) : codisjoint a (b ⊔ c) := h.mono_right le_sup_left
+lemma codisjoint.sup_right' (h : codisjoint a b) : codisjoint a (c ⊔ b) := h.mono_right le_sup_right
+
+variables {c}
+
+@[simp] lemma codisjoint_self : codisjoint a a ↔ a = ⊤ := by simp [codisjoint]
+
+/- TODO: Rename `codisjoint.eq_top` to `codisjoint.sup_eq` and `codisjoint.eq_top_of_self` to
+`codisjoint.eq_top` -/
+alias codisjoint_self ↔ codisjoint.eq_top_of_self _
+
+lemma codisjoint.ne (ha : a ≠ ⊤) (hab : codisjoint a b) : a ≠ b :=
+λ h, ha $ codisjoint_self.1 $ by rwa ←h at hab
+
+lemma codisjoint.eq_top_of_ge (hab : codisjoint a b) (h : b ≤ a) : a = ⊤ :=
+eq_top_iff.2 $ by rwa ←sup_eq_left.2 h
+
+lemma codisjoint.eq_top_of_le (hab : codisjoint a b) : a ≤ b → b = ⊤ := hab.symm.eq_top_of_ge
+
+lemma codisjoint.of_codisjoint_sup_of_le (h : codisjoint (a ⊔ b) c) (hle : c ≤ a) :
+  codisjoint a b :=
+codisjoint_iff.2 $ h.eq_top_of_ge $ le_sup_of_le_left hle
+
+lemma codisjoint.of_codisjoint_sup_of_le' (h : codisjoint (a ⊔ b) c) (hle : c ≤ b) :
+  codisjoint a b :=
+codisjoint_iff.2 $ h.eq_top_of_ge $ le_sup_of_le_right hle
+
+end semilattice_sup_top
+
+section lattice
+variables [lattice α] [bounded_order α] {a : α}
+
+@[simp] lemma codisjoint_bot : codisjoint a ⊥ ↔ a = ⊤ := by simp [codisjoint_iff]
+@[simp] lemma bot_codisjoint : codisjoint ⊥ a ↔ a = ⊤ := by simp [codisjoint_iff]
+
+end lattice
+
+section distrib_lattice_top
+variables [distrib_lattice α] [order_top α] {a b c : α}
+
+@[simp] lemma codisjoint_inf_left : codisjoint (a ⊓ b) c ↔ codisjoint a c ∧ codisjoint b c :=
+by simp only [codisjoint_iff, sup_inf_right, inf_eq_top_iff]
+
+@[simp] lemma codisjoint_inf_right : codisjoint a (b ⊓ c) ↔ codisjoint a b ∧ codisjoint a c :=
+by simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]
+
+lemma codisjoint.inf_left (ha : codisjoint a c) (hb : codisjoint b c) : codisjoint (a ⊓ b) c :=
+codisjoint_inf_left.2 ⟨ha, hb⟩
+
+lemma codisjoint.inf_right (hb : codisjoint a b) (hc : codisjoint a c) : codisjoint a (b ⊓ c) :=
+codisjoint_inf_right.2 ⟨hb, hc⟩
+
+lemma codisjoint.left_le_of_le_inf_right (h : a ⊓ b ≤ c) (hd : codisjoint b c) : a ≤ c :=
+le_of_inf_le_sup_le (le_inf h inf_le_right) $ le_top.trans hd.symm
+
+lemma codisjoint.left_le_of_le_inf_left (h : b ⊓ a ≤ c) (hd : codisjoint b c) : a ≤ c :=
+hd.left_le_of_le_inf_right $ by rwa inf_comm
+
+end distrib_lattice_top
+end codisjoint
+
+lemma disjoint.dual [semilattice_inf α] [order_bot α] {a b : α} :
+  disjoint a b → codisjoint (to_dual a) (to_dual b) := id
+
+lemma codisjoint.dual [semilattice_sup α] [order_top α] {a b : α} :
+  codisjoint a b → disjoint (to_dual a) (to_dual b) := id
+
+@[simp] lemma disjoint_to_dual_iff [semilattice_sup α] [order_top α] {a b : α} :
+  disjoint (to_dual a) (to_dual b) ↔ codisjoint a b := iff.rfl
+@[simp] lemma disjoint_of_dual_iff [semilattice_inf α] [order_bot α] {a b : αᵒᵈ} :
+  disjoint (of_dual a) (of_dual b) ↔ codisjoint a b := iff.rfl
+@[simp] lemma codisjoint_to_dual_iff [semilattice_inf α] [order_bot α] {a b : α} :
+  codisjoint (to_dual a) (to_dual b) ↔ disjoint a b := iff.rfl
+@[simp] lemma codisjoint_of_dual_iff [semilattice_sup α] [order_top α] {a b : αᵒᵈ} :
+  codisjoint (of_dual a) (of_dual b) ↔ disjoint a b := iff.rfl
+
 section is_compl
 
 /-- Two elements `x` and `y` are complements of each other if `x ⊔ y = ⊤` and `x ⊓ y = ⊥`. -/
-structure is_compl [lattice α] [bounded_order α] (x y : α) : Prop :=
-(inf_le_bot : x ⊓ y ≤ ⊥)
-(top_le_sup : ⊤ ≤ x ⊔ y)
+@[protect_proj] structure is_compl [lattice α] [bounded_order α] (x y : α) : Prop :=
+(disjoint : disjoint x y)
+(codisjoint : codisjoint x y)
 
 namespace is_compl
 
 section bounded_order
 
 variables [lattice α] [bounded_order α] {x y z : α}
 
-protected lemma disjoint (h : is_compl x y) : disjoint x y := h.1
+@[symm] protected lemma symm (h : is_compl x y) : is_compl y x := ⟨h.1.symm, h.2.symm⟩
 
-@[symm] protected lemma symm (h : is_compl x y) : is_compl y x :=
-⟨by { rw inf_comm, exact h.1 }, by { rw sup_comm, exact h.2 }⟩
-
-lemma of_eq (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : is_compl x y := ⟨h₁.le, h₂.ge⟩
+lemma of_eq (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : is_compl x y := ⟨le_of_eq h₁, ge_of_eq h₂⟩
 
 lemma inf_eq_bot (h : is_compl x y) : x ⊓ y = ⊥ := h.disjoint.eq_bot
-
-lemma sup_eq_top (h : is_compl x y) : x ⊔ y = ⊤ := top_unique h.top_le_sup
+lemma sup_eq_top (h : is_compl x y) : x ⊔ y = ⊤ := h.codisjoint.eq_top
 
 lemma dual (h : is_compl x y) : is_compl (to_dual x) (to_dual y) := ⟨h.2, h.1⟩
 lemma of_dual {a b : αᵒᵈ} (h : is_compl a b) : is_compl (of_dual a) (of_dual b) := ⟨h.2, h.1⟩
@@ -1339,7 +1434,7 @@ h.symm.left_le_iff
 
 protected lemma antitone {x' y'} (h : is_compl x y) (h' : is_compl x' y') (hx : x ≤ x') :
   y' ≤ y :=
-h'.right_le_iff.2 $ le_trans h.symm.top_le_sup (sup_le_sup_left hx _)
+h'.right_le_iff.2 $ le_trans h.symm.codisjoint (sup_le_sup_left hx _)
 
 lemma right_unique (hxy : is_compl x y) (hxz : is_compl x z) :
   y = z :=

src/order/compactly_generated.lean

@@ -440,9 +440,7 @@ theorem is_complemented_of_Sup_atoms_eq_top (h : Sup {a : α | is_atom a} = ⊤)
 ⟨λ b, begin
   obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn_subset
     {s : set α | complete_lattice.set_independent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _,
-  { refine ⟨Sup s, le_of_eq b_inf_Sup_s, _⟩,
-    rw [← h, Sup_le_iff],
-    intros a ha,
+  { refine ⟨Sup s, le_of_eq b_inf_Sup_s, h.symm.trans_le $ Sup_le_iff.2 $ λ a ha, _⟩,
     rw ← inf_eq_left,
     refine (ha.le_iff.mp inf_le_left).resolve_left (λ con, ha.1 _),
     rw [eq_bot_iff, ← con],

src/order/filter/basic.lean

@@ -852,8 +852,8 @@ empty_mem_iff_bot.symm.trans $ mem_principal.trans subset_empty_iff
 ne_bot_iff.trans $ (not_congr principal_eq_bot_iff).trans ne_empty_iff_nonempty
 
 lemma is_compl_principal (s : set α) : is_compl (𝓟 s) (𝓟 sᶜ) :=
-⟨by simp only [inf_principal, inter_compl_self, principal_empty, le_refl],
-  by simp only [sup_principal, union_compl_self, principal_univ, le_refl]⟩
+is_compl.of_eq (by rw [inf_principal, inter_compl_self, principal_empty]) $
+  by rw [sup_principal, union_compl_self, principal_univ]
 
 theorem mem_inf_principal' {f : filter α} {s t : set α} :
   s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f :=

src/order/hom/basic.lean

@@ -770,40 +770,42 @@ lemma order_iso.map_top [has_le α] [partial_order β] [order_top α] [order_top
   f ⊤ = ⊤ :=
 f.dual.map_bot
 
-lemma order_embedding.map_inf_le [semilattice_inf α] [semilattice_inf β]
-  (f : α ↪o β) (x y : α) :
+lemma order_embedding.map_inf_le [semilattice_inf α] [semilattice_inf β] (f : α ↪o β) (x y : α) :
   f (x ⊓ y) ≤ f x ⊓ f y :=
 f.monotone.map_inf_le x y
 
-lemma order_iso.map_inf [semilattice_inf α] [semilattice_inf β]
-  (f : α ≃o β) (x y : α) :
+lemma order_embedding.le_map_sup [semilattice_sup α] [semilattice_sup β] (f : α ↪o β) (x y : α) :
+  f x ⊔ f y ≤ f (x ⊔ y) :=
+f.monotone.le_map_sup x y
+
+lemma order_iso.map_inf [semilattice_inf α] [semilattice_inf β] (f : α ≃o β) (x y : α) :
   f (x ⊓ y) = f x ⊓ f y :=
 begin
   refine (f.to_order_embedding.map_inf_le x y).antisymm _,
   simpa [← f.symm.le_iff_le] using f.symm.to_order_embedding.map_inf_le (f x) (f y)
 end
 
+lemma order_iso.map_sup [semilattice_sup α] [semilattice_sup β] (f : α ≃o β) (x y : α) :
+  f (x ⊔ y) = f x ⊔ f y :=
+f.dual.map_inf x y
+
 /-- Note that this goal could also be stated `(disjoint on f) a b` -/
 lemma disjoint.map_order_iso [semilattice_inf α] [order_bot α] [semilattice_inf β] [order_bot β]
   {a b : α} (f : α ≃o β) (ha : disjoint a b) : disjoint (f a) (f b) :=
-begin
-  rw [disjoint, ←f.map_inf, ←f.map_bot],
-  exact f.monotone ha,
-end
+by { rw [disjoint, ←f.map_inf, ←f.map_bot], exact f.monotone ha }
+
+/-- Note that this goal could also be stated `(codisjoint on f) a b` -/
+lemma codisjoint.map_order_iso [semilattice_sup α] [order_top α] [semilattice_sup β] [order_top β]
+  {a b : α} (f : α ≃o β) (ha : codisjoint a b) : codisjoint (f a) (f b) :=
+by { rw [codisjoint, ←f.map_sup, ←f.map_top], exact f.monotone ha }
 
 @[simp] lemma disjoint_map_order_iso_iff [semilattice_inf α] [order_bot α] [semilattice_inf β]
   [order_bot β] {a b : α} (f : α ≃o β) : disjoint (f a) (f b) ↔ disjoint a b :=
 ⟨λ h, f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_order_iso f.symm, λ h, h.map_order_iso f⟩
 
-lemma order_embedding.le_map_sup [semilattice_sup α] [semilattice_sup β]
-  (f : α ↪o β) (x y : α) :
-  f x ⊔ f y ≤ f (x ⊔ y) :=
-f.monotone.le_map_sup x y
-
-lemma order_iso.map_sup [semilattice_sup α] [semilattice_sup β]
-  (f : α ≃o β) (x y : α) :
-  f (x ⊔ y) = f x ⊔ f y :=
-f.dual.map_inf x y
+@[simp] lemma codisjoint_map_order_iso_iff [semilattice_sup α] [order_top α] [semilattice_sup β]
+  [order_top β] {a b : α} (f : α ≃o β) : codisjoint (f a) (f b) ↔ codisjoint a b :=
+⟨λ h, f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_order_iso f.symm, λ h, h.map_order_iso f⟩
 
 namespace with_bot
 
@@ -873,15 +875,11 @@ variables [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : 
 include f
 
 lemma order_iso.is_compl {x y : α} (h : is_compl x y) : is_compl (f x) (f y) :=
-⟨by { rw [← f.map_bot, ← f.map_inf, f.map_rel_iff], exact h.1 },
-  by { rw [← f.map_top, ← f.map_sup, f.map_rel_iff], exact h.2 }⟩
+⟨h.1.map_order_iso _, h.2.map_order_iso _⟩
 
 theorem order_iso.is_compl_iff {x y : α} :
   is_compl x y ↔ is_compl (f x) (f y) :=
-⟨f.is_compl, λ h, begin
-  rw [← f.symm_apply_apply x, ← f.symm_apply_apply y],
-  exact f.symm.is_compl h,
-end⟩
+⟨f.is_compl, λ h, f.symm_apply_apply x ▸ f.symm_apply_apply y ▸ f.symm.is_compl h⟩
 
 lemma order_iso.is_complemented
   [is_complemented α] : is_complemented β :=

src/order/hom/lattice.lean

@@ -223,9 +223,10 @@ include β
 lemma disjoint.map (h : disjoint a b) : disjoint (f a) (f b) :=
 by rw [disjoint_iff, ←map_inf, h.eq_bot, map_bot]
 
-lemma is_compl.map (h : is_compl a b) : is_compl (f a) (f b) :=
-{ inf_le_bot := h.disjoint.map _,
-  top_le_sup := by rw [←map_sup, h.sup_eq_top, map_top] }
+lemma codisjoint.map (h : codisjoint a b) : codisjoint (f a) (f b) :=
+by rw [codisjoint_iff, ←map_sup, h.eq_top, map_top]
+
+lemma is_compl.map (h : is_compl a b) : is_compl (f a) (f b) := ⟨h.1.map _, h.2.map _⟩
 
 end bounded_lattice