feat(GCDMonoid): Associates form DistribLattice

Mathlib.lean

@@ -349,6 +349,7 @@ public import Mathlib.Algebra.GCDMonoid.Basic
 public import Mathlib.Algebra.GCDMonoid.Finset
 public import Mathlib.Algebra.GCDMonoid.FinsetLemmas
 public import Mathlib.Algebra.GCDMonoid.IntegrallyClosed
+public import Mathlib.Algebra.GCDMonoid.Lattice
 public import Mathlib.Algebra.GCDMonoid.Multiset
 public import Mathlib.Algebra.GCDMonoid.Nat
 public import Mathlib.Algebra.GCDMonoid.PUnit
@@ -6148,6 +6149,7 @@ public import Mathlib.Order.KonigLemma
 public import Mathlib.Order.KrullDimension
 public import Mathlib.Order.Lattice
 public import Mathlib.Order.Lattice.Congruence
+public import Mathlib.Order.Lattice.Constructor
 public import Mathlib.Order.Lattice.Nat
 public import Mathlib.Order.LatticeIntervals
 public import Mathlib.Order.Lex

Mathlib/Algebra/GCDMonoid/Lattice.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Aaron Liu, Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Liu, Junyan Xu
+-/
+module
+
+public import Mathlib.Algebra.GCDMonoid.Nat
+public import Mathlib.Order.Lattice.Constructor
+
+/-!
+# `Associates` in a `GCDMonoid` form a lattice
+-/
+
+public section
+
+variable (α : Type*) [CommMonoidWithZero α] (a b c : α)
+
+section GCDMonoid
+
+variable [GCDMonoid α]
+
+/-- If `α` is a GCD monoid, then `α ⧸ αˣ` is distributive lattice with `lcm` as `⊔` and
+`gcd` as `⊓`. This is not an instance to avoid conflict with `Associates.instLattice` for
+`UniqueFactorizationMonoid`s. -/
+abbrev Associates.distribLattice : DistribLattice (Associates α) :=
+  let : Lattice (Associates α) :=
+  { sup := lcm
+    le_sup_left := dvd_lcm_left
+    le_sup_right := dvd_lcm_right
+    sup_le _ _ _ := lcm_dvd
+    inf := gcd
+    inf_le_left := gcd_dvd_left
+    inf_le_right := gcd_dvd_right
+    le_inf _ _ _ := dvd_gcd }
+  .ofEqOfInfSupEq _ fun a b c inf_eq sup_eq ↦ by
+    obtain rfl | hx := eq_or_ne a 0
+    · simpa using inf_eq
+    apply mul_left_cancel₀ hx
+    grw [← associated_iff_eq, ← gcd_mul_lcm, ← gcd_mul_lcm a c]
+    exact .of_eq congr($inf_eq * $sup_eq)
+
+variable {α}
+
+attribute [local instance] Associates.distribLattice
+
+theorem associated_gcd_lcm_left : Associated (gcd a (lcm b c)) (lcm (gcd a b) (gcd a c)) :=
+  Associates.mk_eq_mk_iff_associated.mp (inf_sup_left (Associates.mk a) (.mk b) (.mk c))
+
+theorem associated_gcd_lcm_right : Associated (gcd (lcm a b) c) (lcm (gcd a c) (gcd b c)) :=
+  Associates.mk_eq_mk_iff_associated.mp (inf_sup_right (Associates.mk a) (.mk b) (.mk c))
+
+theorem associated_lcm_gcd_left : Associated (lcm a (gcd b c)) (gcd (lcm a b) (lcm a c)) :=
+  Associates.mk_eq_mk_iff_associated.mp (sup_inf_left (Associates.mk a) (.mk b) (.mk c))
+
+theorem associated_lcm_gcd_right : Associated (lcm (gcd a b) c) (gcd (lcm a c) (lcm b c)) :=
+  Associates.mk_eq_mk_iff_associated.mp (sup_inf_right (Associates.mk a) (.mk b) (.mk c))
+
+end GCDMonoid
+
+section NormalizedGCDMonoid
+
+variable {α} [NormalizedGCDMonoid α] {a b c : α}
+
+theorem gcd_lcm_left : gcd a (lcm b c) = lcm (gcd a b) (gcd a c) :=
+  (associated_gcd_lcm_left a b c).eq_of_normalized (normalize_gcd ..) (normalize_lcm ..)
+
+theorem gcd_lcm_right : gcd (lcm a b) c = lcm (gcd a c) (gcd b c) :=
+  (associated_gcd_lcm_right a b c).eq_of_normalized (normalize_gcd ..) (normalize_lcm ..)
+
+theorem lcm_gcd_left : lcm a (gcd b c) = gcd (lcm a b) (lcm a c) :=
+  (associated_lcm_gcd_left a b c).eq_of_normalized (normalize_lcm ..) (normalize_gcd ..)
+
+theorem lcm_gcd_right : lcm (gcd a b) c = gcd (lcm a c) (lcm b c) :=
+  (associated_lcm_gcd_right a b c).eq_of_normalized (normalize_lcm ..) (normalize_gcd ..)
+
+end NormalizedGCDMonoid
+
+namespace Nat
+
+variable {a b c : ℕ}
+
+protected theorem gcd_lcm_left : gcd a (lcm b c) = lcm (gcd a b) (gcd a c) := gcd_lcm_left
+protected theorem gcd_lcm_right : gcd (lcm a b) c = lcm (gcd a c) (gcd b c) := gcd_lcm_right
+protected theorem lcm_gcd_left : lcm a (gcd b c) = gcd (lcm a b) (lcm a c) := lcm_gcd_left
+protected theorem lcm_gcd_right : lcm (gcd a b) c = gcd (lcm a c) (lcm b c) := lcm_gcd_right
+
+end Nat

Mathlib/Order/Lattice.lean

@@ -34,6 +34,8 @@ of `sup` over `inf`, on the left or on the right.
   commutative, associative and satisfy a pair of "absorption laws".
 
 * `DistribLattice`: a type class for distributive lattices.
+* `IsModularLattice`: Modular lattices. Lattices where `a ≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)`. We
+  only require an inequality because the other direction holds in all lattices.
 
 ## Notation
 
@@ -481,6 +483,11 @@ class DistribLattice (α) extends Lattice α where
   /-- The infimum distributes over the supremum -/
   protected le_sup_inf : ∀ x y z : α, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
 
+/-- A modular lattice is one with a limited associativity between `⊓` and `⊔`. -/
+class IsModularLattice (α : Type*) [Lattice α] : Prop where
+/-- Whenever `x ≤ z`, then for any `y`, `(x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)` -/
+  sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
+
 section DistribLattice
 
 variable [DistribLattice α] {x y z : α}
@@ -539,6 +546,67 @@ abbrev DistribLattice.ofInfSupLe
   le_sup_inf := (@OrderDual.instDistribLattice αᵒᵈ { (inferInstance : Lattice αᵒᵈ) with
       le_sup_inf := inf_sup_le }).le_sup_inf
 
+/-- A lattice satisfying the (self-dual, ostensibly weaker) law `(x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)`
+is distributive. -/
+abbrev DistribLattice.ofSupInfLeAssoc [Lattice α] (h : ∀ x y z : α, (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z) :
+    DistribLattice α where
+  le_sup_inf x y z := (h x y (x ⊔ z)).trans <|
+    (sup_le_sup_left ((inf_comm ..).trans_le (h x z y)) _).trans <| by
+    rw [inf_comm, ← sup_assoc, sup_idem]
+
+section IsModularLattice
+
+variable [Lattice α] [IsModularLattice α]
+
+theorem sup_inf_le_assoc_of_le {x z : α} (y : α) : x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z :=
+  IsModularLattice.sup_inf_le_assoc_of_le y
+
+@[to_dual existing]
+theorem inf_sup_le_assoc_of_le {x z : α} (y : α) : z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z := by
+  simp_rw [inf_comm x, sup_comm _ z]
+  exact sup_inf_le_assoc_of_le y
+
+@[to_dual]
+theorem sup_inf_assoc_of_le {x : α} (y : α) {z : α} (h : x ≤ z) : (x ⊔ y) ⊓ z = x ⊔ y ⊓ z :=
+  le_antisymm (sup_inf_le_assoc_of_le y h)
+    (le_inf (sup_le_sup_left inf_le_left _) (sup_le h inf_le_right))
+
+@[to_dual]
+theorem IsModularLattice.inf_sup_inf_assoc {x y z : α} : x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z :=
+  (sup_inf_assoc_of_le y inf_le_right).symm
+
+instance : IsModularLattice αᵒᵈ :=
+  ⟨fun y z xz =>
+    le_of_eq
+      (by
+        rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]
+        exact @sup_inf_assoc_of_le α _ _ _ y _ xz)⟩
+
+variable {x y z : α}
+
+@[to_dual]
+theorem eq_of_le_of_inf_le_of_le_sup (hxy : x ≤ y) (hinf : y ⊓ z ≤ x) (hsup : y ≤ x ⊔ z) :
+    x = y := by
+  refine hxy.antisymm ?_
+  rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup
+  rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]
+
+@[to_dual]
+theorem eq_of_le_of_inf_le_of_sup_le (hxy : x ≤ y) (hinf : y ⊓ z ≤ x ⊓ z) (hsup : y ⊔ z ≤ x ⊔ z) :
+    x = y :=
+  eq_of_le_of_inf_le_of_le_sup hxy (hinf.trans inf_le_left) (le_sup_left.trans hsup)
+
+@[to_dual]
+theorem sup_lt_sup_of_lt_of_inf_le_inf (hxy : y < x) (hinf : x ⊓ z ≤ y ⊓ z) : y ⊔ z < x ⊔ z :=
+  lt_of_le_of_ne (sup_le_sup_right (le_of_lt hxy) _) fun hsup =>
+    ne_of_lt hxy <| eq_of_le_of_inf_le_of_sup_le (le_of_lt hxy) hinf (le_of_eq hsup.symm)
+
+theorem strictMono_inf_prod_sup : StrictMono fun x ↦ (x ⊓ z, x ⊔ z) := fun _x _y hxy ↦
+  ⟨⟨inf_le_inf_right _ hxy.le, sup_le_sup_right hxy.le _⟩,
+    fun ⟨inf_le, sup_le⟩ ↦ (sup_lt_sup_of_lt_of_inf_le_inf hxy inf_le).not_ge sup_le⟩
+
+end IsModularLattice
+
 /-!
 ### Lattices derived from linear orders
 -/

Mathlib/Order/Lattice/Constructor.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 Aaron Liu, Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Liu, Junyan Xu
+-/
+module
+
+public import Mathlib.Order.Lattice
+
+import Mathlib.Tactic.Order
+
+/-!
+# Constructors for distributive and modular lattices
+
+This file provides some constructors for `DistribLattice` with weaker conditions to verify,
+using the `order` tactic to facilitate proofs. It also proves an equivalent condition for
+`IsModularLattice`, which can be used as a constructor.
+-/
+
+public section
+
+theorem isModularLattice_iff_eq_of_le_of_inf_le_of_le_sup {α : Type*} [Lattice α] :
+    IsModularLattice α ↔ ∀ x y z : α, x ≤ y → y ⊓ z ≤ x → y ≤ x ⊔ z → x = y :=
+  ⟨@eq_of_le_of_inf_le_of_le_sup α _, fun h ↦
+    ⟨fun {x} y {z} _ ↦ (h _ _ y (by order) (by order) (by order)).ge⟩⟩
+
+namespace DistribLattice
+
+variable (α : Type*) [Lattice α]
+
+/-- A lattice `α` satisfying `(a ⊔ b) ⊓ (a ⊔ c) ⊓ (b ⊔ c) ≤ (a ⊓ b) ⊔ (a ⊓ c) ⊔ (b ⊓ c)` for all
+`a b c : α` is distributive. -/
+abbrev ofInfSupLeSupInf (h : ∀ a b c : α, (a ⊔ b) ⊓ (a ⊔ c) ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c ⊔ b ⊓ c) :
+    DistribLattice α where
+  le_sup_inf := by
+    suffices h : ∀ x y z : α, x ⊔ (x ⊔ y) ⊓ (x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ y) ⊓ (x ⊔ z) → _
+      from fun x y z ↦ Eq.ge (h x y z ?_)
+    on_goal 1 => rw [← inf_comm, h x (y ⊔ z) _ (by order)]
+    on_goal 2 => intro x y z; specialize h x y z
+    all_goals order
+
+/-- A lattice `α` satisfying the cancellation law `b ⊓ a = c ⊓ a → b ⊔ a = c ⊔ a → b = c` for all
+`a b c : α` is distributive. -/
+abbrev ofEqOfInfSupEq (h : ∀ a b c : α, a ⊓ b = a ⊓ c → a ⊔ b = a ⊔ c → b = c) :
+    DistribLattice α :=
+  .ofInfSupLeSupInf α fun a b c ↦
+    have : IsModularLattice α :=
+      isModularLattice_iff_eq_of_le_of_inf_le_of_le_sup.2
+        fun x y z _ _ _ ↦ h z x y (by order) (by order)
+    let u (i j k : α) := i ⊓ (j ⊔ k) ⊔ (j ⊓ k)
+    let is (i j k : α) := (i ⊔ j) ⊓ (i ⊔ k) ⊓ (j ⊔ k)
+    let si (i j k : α) := (i ⊓ j) ⊔ (i ⊓ k) ⊔ (j ⊓ k)
+    have u_eq i j k : u i j k = (i ⊔ (j ⊓ k)) ⊓ (j ⊔ k) := by
+      unfold u; rw [inf_comm, inf_sup_assoc_of_le _ (by order), inf_comm]
+    have u_inf_u i j k : u i j k ⊓ u j i k = si i j k := by
+      unfold u si
+      rw [← inf_sup_assoc_of_le _ (by order),
+        ← sup_comm (j ⊓ k), sup_inf_assoc_of_le _ (by order)]
+      order
+    have u_sup_u i j k : u i j k ⊔ u j i k = is i j k := by
+      unfold is
+      rw [u_eq, u_eq, ← sup_inf_assoc_of_le _ (by order),
+        ← inf_comm (j ⊔ k), inf_sup_assoc_of_le _ (by order)]
+      order
+    have u₂₃ i j k : u i j k = u i k j := by unfold u; order
+    have u₁₂ i j k : u i j k = u j i k := h (u k i j) _ _
+      (by rw [u₂₃ i, u_inf_u, u₂₃, u₂₃ j, u_inf_u]; unfold si; order)
+      (by rw [u₂₃ i, u_sup_u, u₂₃, u₂₃ j, u_sup_u]; unfold is; order)
+    show is a b c ≤ si a b c by simp [← u_inf_u, ← u_sup_u, u₁₂]
+
+end DistribLattice
+
+end

Mathlib/Order/ModularLattice.lean

@@ -29,8 +29,6 @@ We define (semi)modularity typeclasses as Prop-valued mixins.
   covers `a ⊓ b`.
 * `IsLowerModularLattice`: Lower modular lattices. Lattices where `a` covers `a ⊓ b` if `a ⊔ b`
   covers `b`.
-- `IsModularLattice`: Modular lattices. Lattices where `a ≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)`. We
-  only require an inequality because the other direction holds in all lattices.
 
 ## Main Definitions
 
@@ -87,11 +85,6 @@ class IsLowerModularLattice (α : Type*) [Lattice α] : Prop where
 /-- `a` and `b` both cover `a ⊓ b` if `a ⊔ b` covers either `a` or `b` -/
   inf_covBy_of_covBy_sup {a b : α} : a ⋖ a ⊔ b → a ⊓ b ⋖ b
 
-/-- A modular lattice is one with a limited associativity between `⊓` and `⊔`. -/
-class IsModularLattice (α : Type*) [Lattice α] : Prop where
-/-- Whenever `x ≤ z`, then for any `y`, `(x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)` -/
-  sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
-
 section WeakUpperModular
 
 variable [Lattice α] [IsWeakUpperModularLattice α] {a b : α}
@@ -152,53 +145,6 @@ section IsModularLattice
 
 variable [Lattice α] [IsModularLattice α]
 
-theorem sup_inf_le_assoc_of_le {x z : α} (y : α) : x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z :=
-  IsModularLattice.sup_inf_le_assoc_of_le y
-
-@[to_dual existing]
-theorem inf_sup_le_assoc_of_le {x z : α} (y : α) : z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z := by
-  simp_rw [inf_comm x, sup_comm _ z]
-  exact sup_inf_le_assoc_of_le y
-
-@[to_dual]
-theorem sup_inf_assoc_of_le {x : α} (y : α) {z : α} (h : x ≤ z) : (x ⊔ y) ⊓ z = x ⊔ y ⊓ z :=
-  le_antisymm (sup_inf_le_assoc_of_le y h)
-    (le_inf (sup_le_sup_left inf_le_left _) (sup_le h inf_le_right))
-
-@[to_dual]
-theorem IsModularLattice.inf_sup_inf_assoc {x y z : α} : x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z :=
-  (sup_inf_assoc_of_le y inf_le_right).symm
-
-instance : IsModularLattice αᵒᵈ :=
-  ⟨fun y z xz =>
-    le_of_eq
-      (by
-        rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]
-        exact @sup_inf_assoc_of_le α _ _ _ y _ xz)⟩
-
-variable {x y z : α}
-
-@[to_dual]
-theorem eq_of_le_of_inf_le_of_le_sup (hxy : x ≤ y) (hinf : y ⊓ z ≤ x) (hsup : y ≤ x ⊔ z) :
-    x = y := by
-  refine hxy.antisymm ?_
-  rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup
-  rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]
-
-@[to_dual]
-theorem eq_of_le_of_inf_le_of_sup_le (hxy : x ≤ y) (hinf : y ⊓ z ≤ x ⊓ z) (hsup : y ⊔ z ≤ x ⊔ z) :
-    x = y :=
-  eq_of_le_of_inf_le_of_le_sup hxy (hinf.trans inf_le_left) (le_sup_left.trans hsup)
-
-@[to_dual]
-theorem sup_lt_sup_of_lt_of_inf_le_inf (hxy : y < x) (hinf : x ⊓ z ≤ y ⊓ z) : y ⊔ z < x ⊔ z :=
-  lt_of_le_of_ne (sup_le_sup_right (le_of_lt hxy) _) fun hsup =>
-    ne_of_lt hxy <| eq_of_le_of_inf_le_of_sup_le (le_of_lt hxy) hinf (le_of_eq hsup.symm)
-
-theorem strictMono_inf_prod_sup : StrictMono fun x ↦ (x ⊓ z, x ⊔ z) := fun _x _y hxy ↦
-  ⟨⟨inf_le_inf_right _ hxy.le, sup_le_sup_right hxy.le _⟩,
-    fun ⟨inf_le, sup_le⟩ ↦ (sup_lt_sup_of_lt_of_inf_le_inf hxy inf_le).not_ge sup_le⟩
-
 /-- A generalization of the theorem that if `N` is a submodule of `M` and
   `N` and `M / N` are both Artinian, then `M` is Artinian. -/
 theorem wellFounded_lt_exact_sequence {β γ : Type*} [Preorder β] [Preorder γ]