Mathlib.Algebra.Order.Group.Lattice

Module docstring

{"# Lattice ordered groups

Lattice ordered groups were introduced by [Birkhoff][birkhoff1942]. They form the algebraic underpinnings of vector lattices, Banach lattices, AL-space, AM-space etc.

A lattice ordered group is a type α satisfying: * Lattice α * CommGroup α * MulLeftMono α * MulRightMono α

This file establishes basic properties of lattice ordered groups. It is shown that when the group is commutative, the lattice is distributive. This also holds in the non-commutative case ([Birkhoff][birkhoff1942],[Fuchs][fuchs1963]) but we do not yet have the machinery to establish this in mathlib.

References

[Birkhoff, Lattice-ordered Groups][birkhoff1942]
[Bourbaki, Algebra II][bourbaki1981]
[Fuchs, Partially Ordered Algebraic Systems][fuchs1963]
[Zaanen, Lectures on \"Riesz Spaces\"][zaanen1966]
[Banasiak, Banach Lattices in Applications][banasiak]

Tags

lattice, order, group "}

mul_sup theorem

[MulLeftMono α] (a b c : α) : c * (a ⊔ b) = c * a ⊔ c * b

Full source

@[to_additive]
lemma mul_sup [MulLeftMono α] (a b c : α) :
    c * (a ⊔ b) = c * a ⊔ c * b :=
  (OrderIso.mulLeft _).map_sup _ _

Left Multiplication Distributes Over Supremum in Lattice-Ordered Groups

Informal description

Let $\alpha$ be a lattice-ordered group with left multiplication monotonicity. For any elements $a, b, c \in \alpha$, the product of $c$ with the supremum of $a$ and $b$ equals the supremum of $c * a$ and $c * b$, i.e., $c * (a \sqcup b) = (c * a) \sqcup (c * b)$.

sup_mul theorem

[MulRightMono α] (a b c : α) : (a ⊔ b) * c = a * c ⊔ b * c

Full source

@[to_additive]
lemma sup_mul [MulRightMono α] (a b c : α) :
    (a ⊔ b) * c = a * c ⊔ b * c :=
  (OrderIso.mulRight _).map_sup _ _

Right Multiplication Distributes Over Supremum in Lattice-Ordered Groups

Informal description

Let $\alpha$ be a lattice-ordered group with right multiplication monotonicity. For any elements $a, b, c \in \alpha$, the supremum of $a$ and $b$ multiplied by $c$ equals the supremum of $a * c$ and $b * c$, i.e., $(a \sqcup b) * c = (a * c) \sqcup (b * c)$.

mul_inf theorem

[MulLeftMono α] (a b c : α) : c * (a ⊓ b) = c * a ⊓ c * b

Full source

@[to_additive]
lemma mul_inf [MulLeftMono α] (a b c : α) :
    c * (a ⊓ b) = c * a ⊓ c * b :=
  (OrderIso.mulLeft _).map_inf _ _

Left Multiplication Distributes Over Meet in Lattice-Ordered Groups

Informal description

Let $\alpha$ be a lattice-ordered group with left multiplication monotonicity. For any elements $a, b, c \in \alpha$, the product of $c$ with the meet of $a$ and $b$ equals the meet of $c * a$ and $c * b$, i.e., $c * (a \sqcap b) = (c * a) \sqcap (c * b)$.

inf_mul theorem

[MulRightMono α] (a b c : α) : (a ⊓ b) * c = a * c ⊓ b * c

Full source

@[to_additive]
lemma inf_mul [MulRightMono α] (a b c : α) :
    (a ⊓ b) * c = a * c ⊓ b * c :=
  (OrderIso.mulRight _).map_inf _ _

Right Multiplication Distributes Over Meet in Lattice-Ordered Groups

Informal description

Let $\alpha$ be a lattice-ordered group with right multiplication monotonicity. For any elements $a, b, c \in \alpha$, the meet of $a$ and $b$ multiplied by $c$ equals the meet of $a * c$ and $b * c$, i.e., $(a \sqcap b) * c = (a * c) \sqcap (b * c)$.

sup_div theorem

[MulRightMono α] (a b c : α) : (a ⊔ b) / c = a / c ⊔ b / c

Full source

@[to_additive]
lemma sup_div [MulRightMono α] (a b c : α) :
    (a ⊔ b) / c = a / c ⊔ b / c :=
  (OrderIso.divRight _).map_sup _ _

Supremum Distributes Over Right Division in Lattice-Ordered Groups

Informal description

Let $\alpha$ be a lattice-ordered group with right multiplication monotonicity. For any elements $a, b, c \in \alpha$, the supremum of $a$ and $b$ divided by $c$ equals the supremum of $a / c$ and $b / c$, i.e., $(a \sqcup b) / c = (a / c) \sqcup (b / c)$.

inf_div theorem

[MulRightMono α] (a b c : α) : (a ⊓ b) / c = a / c ⊓ b / c

Full source

@[to_additive]
lemma inf_div [MulRightMono α] (a b c : α) :
    (a ⊓ b) / c = a / c ⊓ b / c :=
  (OrderIso.divRight _).map_inf _ _

Meet Distributes Over Right Division in Lattice-Ordered Groups

Informal description

Let $\alpha$ be a lattice-ordered group with right multiplication monotonicity. For any elements $a, b, c \in \alpha$, the meet of $a$ and $b$ divided by $c$ equals the meet of $a / c$ and $b / c$, i.e., $(a \sqcap b) / c = (a / c) \sqcap (b / c)$.

inv_sup theorem

(a b : α) : (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹

Full source

@[to_additive] lemma inv_sup (a b : α) : (a ⊔ b)⁻¹ = a⁻¹a⁻¹ ⊓ b⁻¹ := (OrderIso.inv α).map_sup _ _

Inverse of Supremum Equals Infimum of Inverses in Lattice-Ordered Groups

Informal description

For any elements $a$ and $b$ in a lattice-ordered group $\alpha$, the inverse of their supremum equals the infimum of their inverses, i.e., $(a \sqcup b)^{-1} = a^{-1} \sqcap b^{-1}$.

inv_inf theorem

(a b : α) : (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹

Full source

@[to_additive] lemma inv_inf (a b : α) : (a ⊓ b)⁻¹ = a⁻¹a⁻¹ ⊔ b⁻¹ := (OrderIso.inv α).map_inf _ _

Inverse of Meet Equals Join of Inverses in Lattice-Ordered Groups

Informal description

For any elements $a$ and $b$ in a lattice-ordered group $\alpha$, the inverse of their meet equals the join of their inverses, i.e., $(a \sqcap b)^{-1} = a^{-1} \sqcup b^{-1}$.

div_sup theorem

(a b c : α) : c / (a ⊔ b) = c / a ⊓ c / b

Full source

@[to_additive]
lemma div_sup (a b c : α) : c / (a ⊔ b) = c / a ⊓ c / b := (OrderIso.divLeft c).map_sup _ _

Division by Supremum Equals Infimum of Divisions in Lattice-Ordered Groups

Informal description

For any elements $a, b, c$ in a lattice-ordered group $\alpha$, the division of $c$ by the supremum of $a$ and $b$ equals the infimum of $c/a$ and $c/b$, i.e., \[ c / (a \sqcup b) = (c / a) \sqcap (c / b). \]

div_inf theorem

(a b c : α) : c / (a ⊓ b) = c / a ⊔ c / b

Full source

@[to_additive]
lemma div_inf (a b c : α) : c / (a ⊓ b) = c / a ⊔ c / b := (OrderIso.divLeft c).map_inf _ _

Division by Infimum Equals Supremum of Divisions

Informal description

For any elements $a, b, c$ in a lattice-ordered group $\alpha$, the division of $c$ by the infimum of $a$ and $b$ equals the supremum of $c/a$ and $c/b$, i.e., \[ c / (a \sqcap b) = (c / a) \sqcup (c / b). \]

pow_two_semiclosed theorem

{a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a

Full source

@[to_additive]
lemma pow_two_semiclosed
    {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a := by
  suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
    rwa [← inf_eq_right, ← mul_eq_left]
  rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
    inf_assoc, inf_of_le_left ha]

Square Inequality Implies Element Inequality in Lattice-Ordered Groups

Informal description

For any element $a$ in a lattice-ordered group $\alpha$, if $1 \leq a^2$, then $1 \leq a$.

inf_mul_sup theorem

[MulLeftMono α] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b

Full source

@[to_additive]
lemma inf_mul_sup [MulLeftMono α] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b :=
  calc
    (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹b⁻¹ ⊔ a⁻¹)) := by
      rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
    _ = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) := by rw [inv_inf, sup_comm]
    _ = a * b := by rw [mul_comm, inv_mul_cancel_right]

Product of Meet and Join Equals Product in Lattice-Ordered Groups

Informal description

For any elements $a$ and $b$ in a lattice-ordered group $\alpha$ with left multiplication monotonicity, the product of their meet and join equals their product, i.e., $(a \sqcap b) * (a \sqcup b) = a * b$.

CommGroup.toDistribLattice definition

(α : Type*) [Lattice α] [CommGroup α] [MulLeftMono α] : DistribLattice α

Full source

/-- Every lattice ordered commutative group is a distributive lattice. -/
-- Non-comm case needs cancellation law https://ncatlab.org/nlab/show/distributive+lattice
@[to_additive "Every lattice ordered commutative additive group is a distributive lattice"]
def CommGroup.toDistribLattice (α : Type*) [Lattice α] [CommGroup α]
    [MulLeftMono α] : DistribLattice α where
  le_sup_inf x y z := by
    rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul,
      le_inf_iff]
    constructor
    · rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left
    · rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right

Distributive lattice property of lattice ordered commutative groups

Informal description

Every lattice ordered commutative group is a distributive lattice. That is, for any type $\alpha$ equipped with a lattice structure, a commutative group structure, and left multiplication monotonicity, the lattice is distributive.