feat(order/modular_lattice): Modular lattices are lower modular (#17403)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>



Co-authored-by: D.M.H. van Gent <gentdmhvan@u0031838.vuw.leidenuniv.nl>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/data/set/function.lean

@@ -1127,6 +1127,12 @@ lemma strict_anti_on.comp_strict_mono_on [preorder α] [preorder β] [preorder 
   strict_anti_on (g ∘ f) s :=
 λ x hx y hy hxy, hg (hs hx) (hs hy) $ hf hx hy hxy
 
+@[simp] lemma strict_mono_restrict [preorder α] [preorder β] {f : α → β} {s : set α} :
+  strict_mono (s.restrict f) ↔ strict_mono_on f s :=
+by simp [set.restrict, strict_mono, strict_mono_on]
+
+alias strict_mono_restrict ↔ _root_.strict_mono.of_restrict _root_.strict_mono_on.restrict
+
 lemma strict_mono.cod_restrict [preorder α] [preorder β] {f : α → β} (hf : strict_mono f)
   {s : set β} (hs : ∀ x, f x ∈ s) :
   strict_mono (set.cod_restrict f s hs) :=

src/order/modular_lattice.lean

@@ -48,9 +48,10 @@ We define (semi)modularity typeclasses as Prop-valued mixins.
 ## TODO
 
 - Relate atoms and coatoms in modular lattices
-- Prove that a modular lattice is both upper and lower modular.
 -/
 
+open set
+
 variable {α : Type*}
 
 /-- A weakly upper modular lattice is a lattice where `a ⊔ b` covers `a` and `b` if `a` and `b` both
@@ -239,6 +240,7 @@ theorem well_founded_gt_exact_sequence
 @well_founded_lt_exact_sequence αᵒᵈ _ _ γᵒᵈ βᵒᵈ _ _ h₂ h₁ K g₁ g₂ f₁ f₂ gi.dual gci.dual hg hf
 
 /-- The diamond isomorphism between the intervals `[a ⊓ b, a]` and `[b, a ⊔ b]` -/
+@[simps]
 def inf_Icc_order_iso_Icc_sup (a b : α) : set.Icc (a ⊓ b) a ≃o set.Icc b (a ⊔ b) :=
 { to_fun := λ x, ⟨x ⊔ b, ⟨le_sup_right, sup_le_sup_right x.prop.2 b⟩⟩,
   inv_fun := λ x, ⟨a ⊓ x, ⟨inf_le_inf_left a x.prop.1, inf_le_left⟩⟩,
@@ -254,6 +256,42 @@ def inf_Icc_order_iso_Icc_sup (a b : α) : set.Icc (a ⊓ b) a ≃o set.Icc b (a
       ← sup_eq_right.2 y.prop.1, inf_sup_assoc_of_le _ y.prop.2, @sup_comm _ _ b],
     exact inf_le_inf_left _ h
   end }
+
+lemma inf_strict_mono_on_Icc_sup {a b : α} : strict_mono_on (λ c, a ⊓ c) (Icc b (a ⊔ b)) :=
+strict_mono.of_restrict (inf_Icc_order_iso_Icc_sup a b).symm.strict_mono
+
+lemma sup_strict_mono_on_Icc_inf {a b : α} : strict_mono_on (λ c, c ⊔ b) (Icc (a ⊓ b) a) :=
+strict_mono.of_restrict (inf_Icc_order_iso_Icc_sup a b).strict_mono
+
+/-- The diamond isomorphism between the intervals `]a ⊓ b, a[` and `}b, a ⊔ b[`. -/
+@[simps]
+def inf_Ioo_order_iso_Ioo_sup (a b : α) : Ioo (a ⊓ b) a ≃o Ioo b (a ⊔ b) :=
+{ to_fun := λ c, ⟨c ⊔ b,
+    le_sup_right.trans_lt $ sup_strict_mono_on_Icc_inf (left_mem_Icc.2 inf_le_left)
+      (Ioo_subset_Icc_self c.2) c.2.1,
+    sup_strict_mono_on_Icc_inf (Ioo_subset_Icc_self c.2) (right_mem_Icc.2 inf_le_left) c.2.2⟩,
+  inv_fun := λ c, ⟨a ⊓ c,
+    inf_strict_mono_on_Icc_sup (left_mem_Icc.2 le_sup_right) (Ioo_subset_Icc_self c.2) c.2.1,
+    inf_le_left.trans_lt' $ inf_strict_mono_on_Icc_sup (Ioo_subset_Icc_self c.2)
+      (right_mem_Icc.2 le_sup_right) c.2.2⟩,
+  left_inv := λ c, subtype.ext $
+    by { dsimp, rw [sup_comm, ←inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le] },
+  right_inv := λ c, subtype.ext $
+    by { dsimp, rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le] },
+  map_rel_iff' := λ c d, @order_iso.le_iff_le _ _ _ _ (inf_Icc_order_iso_Icc_sup _ _)
+    ⟨c.1, Ioo_subset_Icc_self c.2⟩ ⟨d.1, Ioo_subset_Icc_self d.2⟩ }
+
+@[priority 100] -- See note [lower instance priority]
+instance is_modular_lattice.to_is_lower_modular_lattice : is_lower_modular_lattice α :=
+⟨λ a b, by { simp_rw [covby_iff_Ioo_eq, @sup_comm _ _ a, @inf_comm _ _ a, ←is_empty_coe_sort,
+  right_lt_sup, inf_lt_left, (inf_Ioo_order_iso_Ioo_sup _ _).symm.to_equiv.is_empty_congr],
+    exact id }⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance is_modular_lattice.to_is_upper_modular_lattice : is_upper_modular_lattice α :=
+⟨λ a b, by { simp_rw [covby_iff_Ioo_eq, ←is_empty_coe_sort,
+  right_lt_sup, inf_lt_left, (inf_Ioo_order_iso_Ioo_sup _ _).to_equiv.is_empty_congr], exact id }⟩
+
 end is_modular_lattice
 
 namespace is_compl