Mathlib.Order.ModularLattice

IsWeakUpperModularLattice structure

(α : Type*) [Lattice α]

Full source

/-- A weakly upper modular lattice is a lattice where `a ⊔ b` covers `a` and `b` if `a` and `b` both
cover `a ⊓ b`. -/
class IsWeakUpperModularLattice (α : Type*) [Lattice α] : Prop where
/-- `a ⊔ b` covers `a` and `b` if `a` and `b` both cover `a ⊓ b`. -/
  covBy_sup_of_inf_covBy_covBy {a b : α} : a ⊓ ba ⊓ b ⋖ a → a ⊓ ba ⊓ b ⋖ b → a ⋖ a ⊔ b

Weakly upper modular lattice

Informal description

A weakly upper modular lattice is a lattice $\alpha$ where for any elements $a$ and $b$, if both $a$ and $b$ cover their meet $a \sqcap b$, then their join $a \sqcup b$ covers both $a$ and $b$. Here, "covers" means that there is no element strictly between them in the lattice order.

IsWeakLowerModularLattice structure

(α : Type*) [Lattice α]

Full source

/-- A weakly lower modular lattice is a lattice where `a` and `b` cover `a ⊓ b` if `a ⊔ b` covers
both `a` and `b`. -/
class IsWeakLowerModularLattice (α : Type*) [Lattice α] : Prop where
/-- `a` and `b` cover `a ⊓ b` if `a ⊔ b` covers both `a` and `b` -/
  inf_covBy_of_covBy_covBy_sup {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ ba ⊓ b ⋖ a

Weakly lower modular lattice

Informal description

A weakly lower modular lattice is a lattice where for any two elements $a$ and $b$, if the join $a \sqcup b$ covers both $a$ and $b$, then the meet $a \sqcap b$ is covered by both $a$ and $b$. Here, "covers" means that there is no element strictly between them in the lattice order.

IsUpperModularLattice structure

(α : Type*) [Lattice α]

Full source

/-- An upper modular lattice, aka semimodular lattice, is a lattice where `a ⊔ b` covers `a` and `b`
if either `a` or `b` covers `a ⊓ b`. -/
class IsUpperModularLattice (α : Type*) [Lattice α] : Prop where
/-- `a ⊔ b` covers `a` and `b` if either `a` or `b` covers `a ⊓ b` -/
  covBy_sup_of_inf_covBy {a b : α} : a ⊓ ba ⊓ b ⋖ a → b ⋖ a ⊔ b

Upper Modular Lattice (Semimodular Lattice)

Informal description

An upper modular lattice (also known as a semimodular lattice) is a lattice where for any elements $a$ and $b$, if either $a$ or $b$ covers their meet $a \sqcap b$, then their join $a \sqcup b$ covers both $a$ and $b$.

IsLowerModularLattice structure

(α : Type*) [Lattice α]

Full source

/-- A lower modular lattice is a lattice where `a` and `b` both cover `a ⊓ b` if `a ⊔ b` covers
either `a` or `b`. -/
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 ⊓ ba ⊓ b ⋖ b

Lower modular lattice

Informal description

A lattice $\alpha$ is called lower modular if for any elements $a, b \in \alpha$, the condition that $a \sqcup b$ covers either $a$ or $b$ implies that both $a$ and $b$ cover their meet $a \sqcap b$. Here, "$x$ covers $y$" (denoted $y \lessdot x$) means that $y < x$ and there is no element strictly between them.

IsModularLattice structure

(α : Type*) [Lattice α]

Full source

/-- 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

Modular Lattice

Informal description

A modular lattice is a lattice $\alpha$ where for any elements $a, b, c \in \alpha$ with $a \leq c$, the modular law holds: $(a \sqcup b) \sqcap c = a \sqcup (b \sqcap c)$. This condition captures a limited form of associativity between the join ($\sqcup$) and meet ($\sqcap$) operations.

covBy_sup_of_inf_covBy_of_inf_covBy_left theorem

: a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

Full source

theorem covBy_sup_of_inf_covBy_of_inf_covBy_left : a ⊓ ba ⊓ b ⋖ a → a ⊓ ba ⊓ b ⋖ b → a ⋖ a ⊔ b :=
  IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy

Covering property of joins in weakly upper modular lattices

Informal description

In a weakly upper modular lattice, for any elements $a$ and $b$, if the meet $a \sqcap b$ is covered by both $a$ and $b$, then the join $a \sqcup b$ covers $a$. Here, "$x$ covers $y$" (denoted $y \lessdot x$) means that $y < x$ and there is no element strictly between them.

covBy_sup_of_inf_covBy_of_inf_covBy_right theorem

: a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Full source

theorem covBy_sup_of_inf_covBy_of_inf_covBy_right : a ⊓ ba ⊓ b ⋖ a → a ⊓ ba ⊓ b ⋖ b → b ⋖ a ⊔ b := by
  rw [inf_comm, sup_comm]
  exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

Covering property of joins in weakly upper modular lattices (right version)

Informal description

In a weakly upper modular lattice, for any elements $a$ and $b$, if the meet $a \sqcap b$ is covered by both $a$ and $b$, then the join $a \sqcup b$ covers $b$. Here, "$x$ covers $y$" (denoted $y \lessdot x$) means that $y < x$ and there is no element strictly between them.

instIsWeakLowerModularLatticeOrderDual instance

: IsWeakLowerModularLattice (OrderDual α)

Full source

instance : IsWeakLowerModularLattice (OrderDual α) :=
  ⟨fun ha hb => (ha.ofDual.sup_of_inf_of_inf_left hb.ofDual).toDual⟩

Order Dual of a Weakly Lower Modular Lattice is Weakly Lower Modular

Informal description

For any lattice $\alpha$ that is weakly lower modular, its order dual $\alpha^{\text{op}}$ is also weakly lower modular.

inf_covBy_of_covBy_sup_of_covBy_sup_left theorem

: a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

Full source

theorem inf_covBy_of_covBy_sup_of_covBy_sup_left : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ ba ⊓ b ⋖ a :=
  IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup

Covering Property of Meet in Weakly Lower Modular Lattices

Informal description

In a weakly lower modular lattice, if the join $a \sqcup b$ covers both $a$ and $b$, then the meet $a \sqcap b$ is covered by $a$.

inf_covBy_of_covBy_sup_of_covBy_sup_right theorem

: a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

Full source

theorem inf_covBy_of_covBy_sup_of_covBy_sup_right : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ ba ⊓ b ⋖ b := by
  rw [sup_comm, inf_comm]
  exact fun ha hb => inf_covBy_of_covBy_sup_of_covBy_sup_left hb ha

Covering Property of Meet in Weakly Lower Modular Lattices (Right Version)

Informal description

In a weakly lower modular lattice, if the join $a \sqcup b$ covers both $a$ and $b$, then the meet $a \sqcap b$ is covered by $b$.

instIsWeakUpperModularLatticeOrderDual instance

: IsWeakUpperModularLattice (OrderDual α)

Full source

instance : IsWeakUpperModularLattice (OrderDual α) :=
  ⟨fun ha hb => (ha.ofDual.inf_of_sup_of_sup_left hb.ofDual).toDual⟩

Order Dual of a Weakly Lower Modular Lattice is Weakly Upper Modular

Informal description

For any lattice $\alpha$, if $\alpha$ is weakly lower modular, then its order dual $\alpha^{\text{op}}$ is weakly upper modular.

covBy_sup_of_inf_covBy_left theorem

: a ⊓ b ⋖ a → b ⋖ a ⊔ b

Full source

theorem covBy_sup_of_inf_covBy_left : a ⊓ ba ⊓ b ⋖ a → b ⋖ a ⊔ b :=
  IsUpperModularLattice.covBy_sup_of_inf_covBy

Covering Property in Upper Modular Lattices: $\text{if } a \sqcap b \lessdot a \text{ then } b \lessdot a \sqcup b$

Informal description

In an upper modular lattice, if the meet $a \sqcap b$ is covered by $a$, then the join $a \sqcup b$ covers $b$.

covBy_sup_of_inf_covBy_right theorem

: a ⊓ b ⋖ b → a ⋖ a ⊔ b

Full source

theorem covBy_sup_of_inf_covBy_right : a ⊓ ba ⊓ b ⋖ b → a ⋖ a ⊔ b := by
  rw [sup_comm, inf_comm]
  exact covBy_sup_of_inf_covBy_left

Covering Property in Upper Modular Lattices: $\text{if } a \sqcap b \lessdot b \text{ then } a \lessdot a \sqcup b$

Informal description

In an upper modular lattice, if the meet $a \sqcap b$ is covered by $b$, then the join $a \sqcup b$ covers $a$.

IsUpperModularLattice.to_isWeakUpperModularLattice instance

: IsWeakUpperModularLattice α

Full source

instance (priority := 100) IsUpperModularLattice.to_isWeakUpperModularLattice :
    IsWeakUpperModularLattice α :=
  ⟨fun _ => CovBy.sup_of_inf_right⟩

Upper Modular Lattices are Weakly Upper Modular

Informal description

Every upper modular lattice is a weakly upper modular lattice.

instIsLowerModularLatticeOrderDual instance

: IsLowerModularLattice (OrderDual α)

Full source

instance : IsLowerModularLattice (OrderDual α) :=
  ⟨fun h => h.ofDual.sup_of_inf_left.toDual⟩

Order Dual of a Lower Modular Lattice is Lower Modular

Informal description

For any lattice $\alpha$, if $\alpha$ is a lower modular lattice, then its order dual $\alpha^{\text{op}}$ is also a lower modular lattice.

inf_covBy_of_covBy_sup_left theorem

: a ⋖ a ⊔ b → a ⊓ b ⋖ b

Full source

theorem inf_covBy_of_covBy_sup_left : a ⋖ a ⊔ b → a ⊓ ba ⊓ b ⋖ b :=
  IsLowerModularLattice.inf_covBy_of_covBy_sup

Covering Property in Lower Modular Lattices: $a \lessdot a \sqcup b \implies a \sqcap b \lessdot b$

Informal description

In a lower modular lattice, if the join $a \sqcup b$ covers $a$, then the meet $a \sqcap b$ is covered by $b$. Here, "$x$ covers $y$" (denoted $y \lessdot x$) means that $y < x$ and there is no element strictly between them.

inf_covBy_of_covBy_sup_right theorem

: b ⋖ a ⊔ b → a ⊓ b ⋖ a

Full source

theorem inf_covBy_of_covBy_sup_right : b ⋖ a ⊔ b → a ⊓ ba ⊓ b ⋖ a := by
  rw [inf_comm, sup_comm]
  exact inf_covBy_of_covBy_sup_left

Covering Property in Lower Modular Lattices: $b \lessdot a \sqcup b \implies a \sqcap b \lessdot a$

Informal description

In a lower modular lattice, if the join $a \sqcup b$ covers $b$ (denoted $b \lessdot a \sqcup b$), then the meet $a \sqcap b$ is covered by $a$ (denoted $a \sqcap b \lessdot a$). Here, "$x$ covers $y$" means that $y < x$ and there is no element strictly between them.

IsLowerModularLattice.to_isWeakLowerModularLattice instance

: IsWeakLowerModularLattice α

Full source

instance (priority := 100) IsLowerModularLattice.to_isWeakLowerModularLattice :
    IsWeakLowerModularLattice α :=
  ⟨fun _ => CovBy.inf_of_sup_right⟩

Lower Modular Lattices are Weakly Lower Modular

Informal description

Every lower modular lattice is a weakly lower modular lattice.

instIsUpperModularLatticeOrderDual instance

: IsUpperModularLattice (OrderDual α)

Full source

instance : IsUpperModularLattice (OrderDual α) :=
  ⟨fun h => h.ofDual.inf_of_sup_left.toDual⟩

Order Dual of an Upper Modular Lattice is Upper Modular

Informal description

The order dual of an upper modular lattice is also an upper modular lattice. That is, if $\alpha$ is an upper modular lattice, then the lattice $\alpha^{\text{op}}$ (with the order reversed) is also upper modular.

sup_inf_assoc_of_le theorem

{x : α} (y : α) {z : α} (h : x ≤ z) : (x ⊔ y) ⊓ z = x ⊔ y ⊓ z

Full source

theorem sup_inf_assoc_of_le {x : α} (y : α) {z : α} (h : x ≤ z) : (x ⊔ y) ⊓ z = x ⊔ y ⊓ z :=
  le_antisymm (IsModularLattice.sup_inf_le_assoc_of_le y h)
    (le_inf (sup_le_sup_left inf_le_left _) (sup_le h inf_le_right))

Modular Law: $(x \sqcup y) \sqcap z = x \sqcup (y \sqcap z)$ when $x \leq z$

Informal description

Let $\alpha$ be a modular lattice. For any elements $x, y, z \in \alpha$ with $x \leq z$, the following equality holds: $$(x \sqcup y) \sqcap z = x \sqcup (y \sqcap z).$$

IsModularLattice.inf_sup_inf_assoc theorem

{x y z : α} : x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z

Full source

theorem IsModularLattice.inf_sup_inf_assoc {x y z : α} : x ⊓ zx ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z :=
  (sup_inf_assoc_of_le y inf_le_right).symm

Modular Associativity Law: $(x \sqcap z) \sqcup (y \sqcap z) = ((x \sqcap z) \sqcup y) \sqcap z$

Informal description

In a modular lattice $\alpha$, for any elements $x, y, z \in \alpha$, the following associativity law holds: $$(x \sqcap z) \sqcup (y \sqcap z) = ((x \sqcap z) \sqcup y) \sqcap z.$$

inf_sup_assoc_of_le theorem

{x : α} (y : α) {z : α} (h : z ≤ x) : x ⊓ y ⊔ z = x ⊓ (y ⊔ z)

Full source

theorem inf_sup_assoc_of_le {x : α} (y : α) {z : α} (h : z ≤ x) : x ⊓ yx ⊓ y ⊔ z = x ⊓ (y ⊔ z) := by
  rw [inf_comm, sup_comm, ← sup_inf_assoc_of_le y h, inf_comm, sup_comm]

Modular Law: $(x \sqcap y) \sqcup z = x \sqcap (y \sqcup z)$ when $z \leq x$

Informal description

Let $\alpha$ be a modular lattice. For any elements $x, y, z \in \alpha$ with $z \leq x$, the following equality holds: $$(x \sqcap y) \sqcup z = x \sqcap (y \sqcup z).$$

instIsModularLatticeOrderDual instance

: IsModularLattice αᵒᵈ

Full source

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)⟩

Order Dual of a Modular Lattice is Modular

Informal description

For any modular lattice $\alpha$, the order dual $\alpha^{\text{op}}$ is also a modular lattice.

IsModularLattice.sup_inf_sup_assoc theorem

: (x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ z) ⊓ y ⊔ z

Full source

theorem IsModularLattice.sup_inf_sup_assoc : (x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ z) ⊓ y(x ⊔ z) ⊓ y ⊔ z :=
  @IsModularLattice.inf_sup_inf_assoc αᵒᵈ _ _ _ _ _

Modular Associativity Law: $(x \sqcup z) \sqcap (y \sqcup z) = ((x \sqcup z) \sqcap y) \sqcup z$

Informal description

In a modular lattice $\alpha$, for any elements $x, y, z \in \alpha$, the following associativity law holds: $$(x \sqcup z) \sqcap (y \sqcup z) = ((x \sqcup z) \sqcap y) \sqcup z.$$

sup_lt_sup_of_lt_of_inf_le_inf theorem

(hxy : x < y) (hinf : y ⊓ z ≤ x ⊓ z) : x ⊔ z < y ⊔ z

Full source

theorem sup_lt_sup_of_lt_of_inf_le_inf (hxy : x < y) (hinf : y ⊓ z ≤ x ⊓ z) : x ⊔ z < y ⊔ 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)

Strict Join Inequality under Meet Condition

Informal description

For any elements $x, y, z$ in a lattice, if $x < y$ and $y \sqcap z \leq x \sqcap z$, then $x \sqcup z < y \sqcup z$.

strictMono_inf_prod_sup theorem

: StrictMono fun x ↦ (x ⊓ z, x ⊔ z)

Full source

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_le sup_le⟩

Strict Monotonicity of the Pair $(x \sqcap z, x \sqcup z)$ in a Lattice

Informal description

For any fixed element $z$ in a lattice, the function $x \mapsto (x \sqcap z, x \sqcup z)$ is strictly monotone. That is, if $x < y$, then both $x \sqcap z < y \sqcap z$ and $x \sqcup z < y \sqcup z$ hold.

wellFounded_lt_exact_sequence theorem

 {β γ : Type*} [Preorder β] [Preorder γ] [h₁ : WellFoundedLT β] [h₂ : WellFoundedLT γ] (K : α) (f₁ : β → α) (f₂ : α → β)
  (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K)
  (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) : WellFoundedLT α

Full source

/-- 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 γ]
    [h₁ : WellFoundedLT β] [h₂ : WellFoundedLT γ] (K : α)
    (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂)
    (gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K) (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) :
    WellFoundedLT α :=
  StrictMono.wellFoundedLT (f := fun A ↦ (f₂ A, g₂ A)) fun A B hAB ↦ by
    simp only [Prod.le_def, lt_iff_le_not_le, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]
    exact strictMono_inf_prod_sup hAB

Well-foundedness of modular lattice via exact sequences

Informal description

Let $\alpha$ be a modular lattice, and let $\beta$ and $\gamma$ be preorders with well-founded strict order relations. Given an element $K \in \alpha$ and functions $f_1: \beta \to \alpha$, $f_2: \alpha \to \beta$, $g_1: \gamma \to \alpha$, $g_2: \alpha \to \gamma$ such that: 1. $(f_1, f_2)$ forms a Galois coinsertion, 2. $(g_2, g_1)$ forms a Galois insertion, 3. For all $a \in \alpha$, $f_1(f_2(a)) = a \sqcap K$, 4. For all $a \in \alpha$, $g_1(g_2(a)) = a \sqcup K$, then the strict order relation on $\alpha$ is well-founded.

wellFounded_gt_exact_sequence theorem

 {β γ : Type*} [Preorder β] [Preorder γ] [WellFoundedGT β] [WellFoundedGT γ] (K : α) (f₁ : β → α) (f₂ : α → β)
  (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K)
  (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) : WellFoundedGT α

Full source

/-- A generalization of the theorem that if `N` is a submodule of `M` and
  `N` and `M / N` are both Noetherian, then `M` is Noetherian. -/
theorem wellFounded_gt_exact_sequence {β γ : Type*} [Preorder β] [Preorder γ]
    [WellFoundedGT β] [WellFoundedGT γ] (K : α)
    (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂)
    (gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K) (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) :
    WellFoundedGT α :=
  wellFounded_lt_exact_sequence (α := αᵒᵈ) (β := γᵒᵈ) (γ := βᵒᵈ)
    K g₁ g₂ f₁ f₂ gi.dual gci.dual hg hf

Well-foundedness of strict greater-than relation in modular lattices via exact sequences

Informal description

Let $\alpha$ be a modular lattice, and let $\beta$ and $\gamma$ be preorders with well-founded strict greater-than relations. Given an element $K \in \alpha$ and functions $f_1: \beta \to \alpha$, $f_2: \alpha \to \beta$, $g_1: \gamma \to \alpha$, $g_2: \alpha \to \gamma$ such that: 1. $(f_1, f_2)$ forms a Galois coinsertion, 2. $(g_2, g_1)$ forms a Galois insertion, 3. For all $a \in \alpha$, $f_1(f_2(a)) = a \sqcap K$, 4. For all $a \in \alpha$, $g_1(g_2(a)) = a \sqcup K$, then the strict greater-than relation on $\alpha$ is well-founded.

infIccOrderIsoIccSup definition

(a b : α) : Set.Icc (a ⊓ b) a ≃o Set.Icc b (a ⊔ b)

Full source

/-- The diamond isomorphism between the intervals `[a ⊓ b, a]` and `[b, a ⊔ b]` -/
@[simps]
def infIccOrderIsoIccSup (a b : α) : Set.IccSet.Icc (a ⊓ b) a ≃o Set.Icc b (a ⊔ b) where
  toFun x := ⟨x ⊔ b, ⟨le_sup_right, sup_le_sup_right x.prop.2 b⟩⟩
  invFun x := ⟨a ⊓ x, ⟨inf_le_inf_left a x.prop.1, inf_le_left⟩⟩
  left_inv x :=
    Subtype.ext
      (by
        change a ⊓ (↑x ⊔ b) = ↑x
        rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1])
  right_inv x :=
    Subtype.ext
      (by
        change a ⊓ ↑xa ⊓ ↑x ⊔ b = ↑x
        rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2])
  map_rel_iff' {x y} := by
    simp only [Subtype.mk_le_mk, Equiv.coe_fn_mk, le_sup_right]
    rw [← Subtype.coe_le_coe]
    refine ⟨fun h => ?_, fun h => sup_le_sup_right h _⟩
    rw [← sup_eq_right.2 x.prop.1, inf_sup_assoc_of_le _ x.prop.2, sup_comm, ←
      sup_eq_right.2 y.prop.1, inf_sup_assoc_of_le _ y.prop.2, sup_comm b]
    exact inf_le_inf_left _ h

Diamond isomorphism theorem for modular lattices

Informal description

For any elements $ a $ and $ b $ in a modular lattice $ \alpha $, there is an order isomorphism between the closed intervals $[a \sqcap b, a]$ and $[b, a \sqcup b]$. Specifically, the isomorphism maps an element $ x \in [a \sqcap b, a] $ to $ x \sqcup b \in [b, a \sqcup b] $, and its inverse maps an element $ y \in [b, a \sqcup b] $ to $ a \sqcap y \in [a \sqcap b, a] $.

inf_strictMonoOn_Icc_sup theorem

{a b : α} : StrictMonoOn (fun c => a ⊓ c) (Icc b (a ⊔ b))

Full source

theorem inf_strictMonoOn_Icc_sup {a b : α} : StrictMonoOn (fun c => a ⊓ c) (Icc b (a ⊔ b)) :=
  StrictMono.of_restrict (infIccOrderIsoIccSup a b).symm.strictMono

Strict Monotonicity of Meet Operation on Interval $[b, a \sqcup b]$

Informal description

For any elements $a$ and $b$ in a modular lattice $\alpha$, the function $c \mapsto a \sqcap c$ is strictly monotone on the closed interval $[b, a \sqcup b]$. That is, for any $c_1, c_2 \in [b, a \sqcup b]$, if $c_1 < c_2$ then $a \sqcap c_1 < a \sqcap c_2$.

sup_strictMonoOn_Icc_inf theorem

{a b : α} : StrictMonoOn (fun c => c ⊔ b) (Icc (a ⊓ b) a)

Full source

theorem sup_strictMonoOn_Icc_inf {a b : α} : StrictMonoOn (fun c => c ⊔ b) (Icc (a ⊓ b) a) :=
  StrictMono.of_restrict (infIccOrderIsoIccSup a b).strictMono

Strict Monotonicity of Join Operation on Interval $[a \sqcap b, a]$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the function $c \mapsto c \sqcup b$ is strictly monotone on the closed interval $[a \sqcap b, a]$. That is, for any $x, y \in [a \sqcap b, a]$, if $x < y$ then $x \sqcup b < y \sqcup b$.

infIooOrderIsoIooSup definition

(a b : α) : Ioo (a ⊓ b) a ≃o Ioo b (a ⊔ b)

Full source

/-- The diamond isomorphism between the intervals `]a ⊓ b, a[` and `}b, a ⊔ b[`. -/
@[simps]
def infIooOrderIsoIooSup (a b : α) : IooIoo (a ⊓ b) a ≃o Ioo b (a ⊔ b) where
  toFun c :=
    ⟨c ⊔ b,
      le_sup_right.trans_lt <|
        sup_strictMonoOn_Icc_inf (left_mem_Icc.2 inf_le_left) (Ioo_subset_Icc_self c.2) c.2.1,
      sup_strictMonoOn_Icc_inf (Ioo_subset_Icc_self c.2) (right_mem_Icc.2 inf_le_left) c.2.2⟩
  invFun c :=
    ⟨a ⊓ c,
      inf_strictMonoOn_Icc_sup (left_mem_Icc.2 le_sup_right) (Ioo_subset_Icc_self c.2) c.2.1,
      inf_le_left.trans_lt' <|
        inf_strictMonoOn_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' := @fun c d =>
    @OrderIso.le_iff_le _ _ _ _ (infIccOrderIsoIccSup _ _) ⟨c.1, Ioo_subset_Icc_self c.2⟩
      ⟨d.1, Ioo_subset_Icc_self d.2⟩

Diamond isomorphism between intervals $(a \sqcap b, a)$ and $(b, a \sqcup b)$ in a modular lattice

Informal description

Given elements $a$ and $b$ in a modular lattice $\alpha$, there is an order isomorphism between the open intervals $(a \sqcap b, a)$ and $(b, a \sqcup b)$. This isomorphism maps an element $c$ in $(a \sqcap b, a)$ to $c \sqcup b$ in $(b, a \sqcup b)$, and its inverse maps an element $d$ in $(b, a \sqcup b)$ to $a \sqcap d$ in $(a \sqcap b, a)$. This captures the diamond isomorphism theorem for modular lattices.

IsModularLattice.to_isLowerModularLattice instance

: IsLowerModularLattice α

Full source

instance (priority := 100) IsModularLattice.to_isLowerModularLattice : IsLowerModularLattice α :=
  ⟨fun {a b} => by
    simp_rw [covBy_iff_Ioo_eq, sup_comm a, inf_comm a, ← isEmpty_coe_sort, right_lt_sup,
      inf_lt_left, (infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr]
    exact id⟩

Modular Lattices are Lower Modular

Informal description

Every modular lattice is a lower modular lattice.

IsModularLattice.to_isUpperModularLattice instance

: IsUpperModularLattice α

Full source

instance (priority := 100) IsModularLattice.to_isUpperModularLattice : IsUpperModularLattice α :=
  ⟨fun {a b} => by
    simp_rw [covBy_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
      (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr]
    exact id⟩

Modular Lattices are Upper Modular

Informal description

Every modular lattice is an upper modular lattice.

IsCompl.IicOrderIsoIci definition

{a b : α} (h : IsCompl a b) : Set.Iic a ≃o Set.Ici b

Full source

/-- The diamond isomorphism between the intervals `Set.Iic a` and `Set.Ici b`. -/
def IicOrderIsoIci {a b : α} (h : IsCompl a b) : Set.IicSet.Iic a ≃o Set.Ici b :=
  (OrderIso.setCongr (Set.Iic a) (Set.Icc (a ⊓ b) a)
        (h.inf_eq_bot.symm ▸ Set.Icc_bot.symm)).trans <|
    (infIccOrderIsoIccSup a b).trans
      (OrderIso.setCongr (Set.Icc b (a ⊔ b)) (Set.Ici b) (h.sup_eq_top.symm ▸ Set.Icc_top))

Order isomorphism between complementary intervals in a modular lattice

Informal description

Given two complementary elements $ a $ and $ b $ in a bounded modular lattice $ \alpha $ (i.e., $ a \sqcap b = \bot $ and $ a \sqcup b = \top $), there is an order isomorphism between the left-infinite right-closed interval $ (-\infty, a] $ and the left-closed right-infinite interval $ [b, \infty) $. This isomorphism is constructed by first identifying $ (-\infty, a] $ with the closed interval $ [\bot, a] $ (since $ a \sqcap b = \bot $), then applying the diamond isomorphism $ [\bot, a] \simeq [b, \top] $ (since $ a \sqcup b = \top $), and finally identifying $ [b, \top] $ with $ [b, \infty) $.

isModularLattice_iff_inf_sup_inf_assoc theorem

[Lattice α] : IsModularLattice α ↔ ∀ x y z : α, x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z

Full source

theorem isModularLattice_iff_inf_sup_inf_assoc [Lattice α] :
    IsModularLatticeIsModularLattice α ↔ ∀ x y z : α, x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z :=
  ⟨fun h => @IsModularLattice.inf_sup_inf_assoc _ _ h, fun h =>
    ⟨fun y z xz => by rw [← inf_eq_left.2 xz, h]⟩⟩

Modular Lattice Characterization via Inf-Sup-Inf Associativity

Informal description

A lattice $\alpha$ is modular if and only if for all elements $x, y, z \in \alpha$, the following associativity law holds: $$(x \sqcap z) \sqcup (y \sqcap z) = ((x \sqcap z) \sqcup y) \sqcap z.$$

DistribLattice.instIsModularLattice instance

[DistribLattice α] : IsModularLattice α

Full source

instance (priority := 100) [DistribLattice α] : IsModularLattice α :=
  ⟨fun y z xz => by rw [inf_sup_right, inf_eq_left.2 xz]⟩

Distributive Lattices are Modular

Informal description

Every distributive lattice is a modular lattice.

Disjoint.disjoint_sup_right_of_disjoint_sup_left theorem

 [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint a b) (hsup : Disjoint (a ⊔ b) c) : Disjoint a (b ⊔ c)

Full source

theorem disjoint_sup_right_of_disjoint_sup_left [Lattice α] [OrderBot α]
    [IsModularLattice α] (h : Disjoint a b) (hsup : Disjoint (a ⊔ b) c) :
    Disjoint a (b ⊔ c) := by
  rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]
  apply le_inf inf_le_left
  apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans
  rw [sup_comm, IsModularLattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]

Disjointness Preservation Under Supremum in Modular Lattices

Informal description

Let $\alpha$ be a modular lattice with a bottom element $\bot$. For any elements $a, b, c \in \alpha$, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$) and $a \sqcup b$ is disjoint with $c$, then $a$ is disjoint with $b \sqcup c$.

Disjoint.disjoint_sup_left_of_disjoint_sup_right theorem

 [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint b c) (hsup : Disjoint a (b ⊔ c)) : Disjoint (a ⊔ b) c

Full source

theorem disjoint_sup_left_of_disjoint_sup_right [Lattice α] [OrderBot α]
    [IsModularLattice α] (h : Disjoint b c) (hsup : Disjoint a (b ⊔ c)) :
    Disjoint (a ⊔ b) c := by
  rw [disjoint_comm, sup_comm]
  apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm
  rwa [sup_comm, disjoint_comm] at hsup

Disjointness Preservation Under Supremum in Modular Lattices (Symmetric Version)

Informal description

Let $\alpha$ be a modular lattice with a bottom element $\bot$. For any elements $a, b, c \in \alpha$, if $b$ and $c$ are disjoint (i.e., $b \sqcap c = \bot$) and $a$ is disjoint with $b \sqcup c$, then $a \sqcup b$ is disjoint with $c$.

Disjoint.isCompl_sup_right_of_isCompl_sup_left theorem

 [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint a b) (hcomp : IsCompl (a ⊔ b) c) : IsCompl a (b ⊔ c)

Full source

theorem isCompl_sup_right_of_isCompl_sup_left [Lattice α] [BoundedOrder α] [IsModularLattice α]
    (h : Disjoint a b) (hcomp : IsCompl (a ⊔ b) c) :
    IsCompl a (b ⊔ c) :=
  ⟨h.disjoint_sup_right_of_disjoint_sup_left hcomp.disjoint, codisjoint_assoc.mp hcomp.codisjoint⟩

Complement Preservation Under Supremum in Modular Lattices: $a$ and $b \sqcup c$ are complements when $a \sqcap b = \bot$ and $a \sqcup b$ is a complement of $c$

Informal description

Let $\alpha$ be a modular lattice with a bounded order structure (having both a greatest element $\top$ and a least element $\bot$). For any elements $a, b, c \in \alpha$, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$) and $a \sqcup b$ is a complement of $c$ (i.e., $(a \sqcup b) \sqcup c = \top$ and $(a \sqcup b) \sqcap c = \bot$), then $a$ is a complement of $b \sqcup c$ (i.e., $a \sqcup (b \sqcup c) = \top$ and $a \sqcap (b \sqcup c) = \bot$).

Disjoint.isCompl_sup_left_of_isCompl_sup_right theorem

 [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint b c) (hcomp : IsCompl a (b ⊔ c)) : IsCompl (a ⊔ b) c

Full source

theorem isCompl_sup_left_of_isCompl_sup_right [Lattice α] [BoundedOrder α] [IsModularLattice α]
    (h : Disjoint b c) (hcomp : IsCompl a (b ⊔ c)) :
    IsCompl (a ⊔ b) c :=
  ⟨h.disjoint_sup_left_of_disjoint_sup_right hcomp.disjoint, codisjoint_assoc.mpr hcomp.codisjoint⟩

Complement Preservation Under Supremum in Modular Lattices: $(a \sqcup b)$ and $c$ are complements when $b \sqcap c = \bot$ and $a$ is a complement of $b \sqcup c$

Informal description

Let $\alpha$ be a modular lattice with a greatest element $\top$ and a least element $\bot$. For any elements $a, b, c \in \alpha$, if $b$ and $c$ are disjoint (i.e., $b \sqcap c = \bot$) and $a$ is a complement of $b \sqcup c$ (i.e., $a \sqcup (b \sqcup c) = \top$ and $a \sqcap (b \sqcup c) = \bot$), then $a \sqcup b$ is a complement of $c$ (i.e., $(a \sqcup b) \sqcup c = \top$ and $(a \sqcup b) \sqcap c = \bot$).

Set.Iic.isCompl_inf_inf_of_isCompl_of_le theorem

 [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b c : α} (h₁ : IsCompl b c) (h₂ : b ≤ a) :
  IsCompl (⟨a ⊓ b, inf_le_left⟩ : Iic a) (⟨a ⊓ c, inf_le_left⟩ : Iic a)

Full source

lemma Set.Iic.isCompl_inf_inf_of_isCompl_of_le [Lattice α] [BoundedOrder α] [IsModularLattice α]
    {a b c : α} (h₁ : IsCompl b c) (h₂ : b ≤ a) :
    IsCompl (⟨a ⊓ b, inf_le_left⟩ : Iic a) (⟨a ⊓ c, inf_le_left⟩ : Iic a) := by
  constructor
  · simp [disjoint_iff, Subtype.ext_iff, inf_comm a c, inf_assoc a, ← inf_assoc b, h₁.inf_eq_bot]
  · simp only [Iic.codisjoint_iff, inf_comm a, IsModularLattice.inf_sup_inf_assoc]
    simp [inf_of_le_left h₂, h₁.sup_eq_top]

Complement Preservation in Modular Lattice Intervals: $a \sqcap b$ and $a \sqcap c$ are complements in $(-\infty, a]$ when $b$ and $c$ are complements and $b \leq a$

Informal description

Let $\alpha$ be a modular lattice with a bounded order structure. Given elements $a, b, c \in \alpha$ such that $b$ and $c$ are complements (i.e., $b \sqcup c = \top$ and $b \sqcap c = \bot$) and $b \leq a$, then the elements $a \sqcap b$ and $a \sqcap c$ in the interval $(-\infty, a]$ are complements.

IsModularLattice.isModularLattice_Iic instance

: IsModularLattice (Set.Iic a)

Full source

instance isModularLattice_Iic : IsModularLattice (Set.Iic a) :=
  ⟨@fun x y z xz => (sup_inf_le_assoc_of_le (y : α) xz : (↑x ⊔ ↑y) ⊓ ↑z ≤ ↑x ⊔ ↑y ⊓ ↑z)⟩

Modular Lattice Structure on $(-\infty, a]$

Informal description

For any modular lattice $\alpha$ and element $a \in \alpha$, the left-infinite right-closed interval $(-\infty, a]$ inherits a modular lattice structure from $\alpha$.

IsModularLattice.isModularLattice_Ici instance

: IsModularLattice (Set.Ici a)

Full source

instance isModularLattice_Ici : IsModularLattice (Set.Ici a) :=
  ⟨@fun x y z xz => (sup_inf_le_assoc_of_le (y : α) xz : (↑x ⊔ ↑y) ⊓ ↑z ≤ ↑x ⊔ ↑y ⊓ ↑z)⟩

Modularity of the interval $[a, \infty)$ in a modular lattice

Informal description

For any element $a$ in a modular lattice $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is also a modular lattice.

IsModularLattice.complementedLattice_Iic instance

: ComplementedLattice (Set.Iic a)

Full source

instance complementedLattice_Iic : ComplementedLattice (Set.Iic a) :=
  ⟨fun ⟨x, hx⟩ =>
    let ⟨y, hy⟩ := exists_isCompl x
    ⟨⟨y ⊓ a, Set.mem_Iic.2 inf_le_right⟩, by
      constructor
      · rw [disjoint_iff_inf_le]
        change x ⊓ (y ⊓ a) ≤ ⊥
        -- improve lattice subtype API
        rw [← inf_assoc]
        exact le_trans inf_le_left hy.1.le_bot
      · rw [codisjoint_iff_le_sup]
        change a ≤ x ⊔ y ⊓ a
        -- improve lattice subtype API
        rw [← sup_inf_assoc_of_le _ (Set.mem_Iic.1 hx), hy.2.eq_top, top_inf_eq]⟩⟩

Complemented Lattice Structure on $(-\infty, a]$ in a Modular Lattice

Informal description

For any element $a$ in a modular lattice $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ is a complemented lattice.

IsModularLattice.complementedLattice_Ici instance

: ComplementedLattice (Set.Ici a)

Full source

instance complementedLattice_Ici : ComplementedLattice (Set.Ici a) :=
  ⟨fun ⟨x, hx⟩ =>
    let ⟨y, hy⟩ := exists_isCompl x
    ⟨⟨y ⊔ a, Set.mem_Ici.2 le_sup_right⟩, by
      constructor
      · rw [disjoint_iff_inf_le]
        change x ⊓ (y ⊔ a) ≤ a
        -- improve lattice subtype API
        rw [← inf_sup_assoc_of_le _ (Set.mem_Ici.1 hx), hy.1.eq_bot, bot_sup_eq]
      · rw [codisjoint_iff_le_sup]
        change ⊤ ≤ x ⊔ (y ⊔ a)
        -- improve lattice subtype API
        rw [← sup_assoc]
        exact le_trans hy.2.top_le le_sup_left⟩⟩

Complemented Lattice Structure on $[a, \infty)$ in a Modular Lattice

Informal description

For any element $a$ in a modular lattice $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is a complemented lattice.

Mathlib.Order.ModularLattice

Typeclasses

Main Definitions

Main Results

References

TODO