mathlib documentation

algebra.lattice_ordered_group

Lattice ordered groups #

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

This file develops the basic theory, concentrating on the commutative case.

Main statements #

It is shown that the inf and sup operations are related to the absolute value operation by a number of equations and inequalities.

Notations #

Implementation notes #

A lattice ordered commutative group is a type α satisfying:

The remainder of the file establishes basic properties of lattice ordered commutative groups. A number of these results also hold in the non-commutative case (Birkhoff, Fuchs) but we have not developed that here, since we are primarily interested in vector lattices.

References #

Tags #

lattice, ordered, group

theorem add_sup_eq_add_sup_add {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
c + (a b) = c + a (c + b)
theorem mul_sup_eq_mul_sup_mul {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
c * (a b) = c * a c * b

Let α be a lattice ordered commutative group. For all elements a, b and c in α, $$c + (a ⊔ b) = (c + a) ⊔ (c + b).$$

theorem neg_sup_eq_neg_inf_neg {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
-(a b) = -a -b
theorem inv_sup_eq_inv_inf_inv {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :

Let α be a lattice ordered commutative group. For all elements a and b in α, $$-(a ⊔ b)=(-a) ⊓ (-b).$$

theorem inv_inf_eq_sup_inv {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :

Let α be a lattice ordered commutative group. For all elements a and b in α, $$ -(a ⊓ b) = -a ⊔ -b.$$

theorem neg_inf_eq_sup_neg {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
-(a b) = -a -b
theorem inf_add_sup {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
a b + (a b) = a + b
theorem inf_mul_sup {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
(a b) * (a b) = a * b

Let α be a lattice ordered commutative group. For all elements a and b in α, $$a ⊓ b + (a ⊔ b) = a + b.$$

def lattice_ordered_comm_group.mpos {α : Type u} [lattice α] [comm_group α] (a : α) :
α

Let α be a lattice ordered commutative group with identity 0. For an element a of type α, the element a ⊔ 0 is said to be the positive component of a, denoted a⁺.

Equations
def lattice_ordered_comm_group.pos {α : Type u} [lattice α] [add_comm_group α] (a : α) :
α

Let α be a lattice ordered commutative group with identity 0. For an element a of type α, the element a ⊔ 0 is said to be the positive component of a, denoted a⁺.

Equations
def lattice_ordered_comm_group.neg {α : Type u} [lattice α] [add_comm_group α] (a : α) :
α

Let α be a lattice ordered commutative group with identity 0. For an element a of type α, the element (-a) ⊔ 0 is said to be the negative component of a, denoted a⁻.

Equations
def lattice_ordered_comm_group.mneg {α : Type u} [lattice α] [comm_group α] (a : α) :
α

Let α be a lattice ordered commutative group with identity 0. For an element a of type α, the element (-a) ⊔ 0 is said to be the negative component of a, denoted a⁻.

Equations
theorem lattice_ordered_comm_group.le_mabs {α : Type u} [lattice α] [comm_group α] (a : α) :
a |a|

Let α be a lattice ordered commutative group and let a be an element in α with absolute value |a|. Then, $$a ≤ |a|.$$

theorem lattice_ordered_comm_group.le_abs {α : Type u} [lattice α] [add_comm_group α] (a : α) :
a |a|
theorem lattice_ordered_comm_group.neg_le_abs {α : Type u} [lattice α] [add_comm_group α] (a : α) :
-a |a|
theorem lattice_ordered_comm_group.inv_le_abs {α : Type u} [lattice α] [comm_group α] (a : α) :

Let α be a lattice ordered commutative group and let a be an element in α with absolute value |a|. Then, $$-a ≤ |a|.$$

theorem lattice_ordered_comm_group.m_pos_pos {α : Type u} [lattice α] [comm_group α] (a : α) :
1 a

Let α be a lattice ordered commutative group and let a be an element in α with positive component a⁺. Then a⁺ is positive.

theorem lattice_ordered_comm_group.m_neg_pos {α : Type u} [lattice α] [comm_group α] (a : α) :
1 a

Let α be a lattice ordered commutative group and let a be an element in α withnegative component a⁻. Then a⁻ is positive.

theorem lattice_ordered_comm_group.m_le_pos {α : Type u} [lattice α] [comm_group α] (a : α) :
a a

Let α be a lattice ordered commutative group and let a be an element in α with positive component a⁺. Then a⁺ dominates a.

theorem lattice_ordered_comm_group.m_le_neg {α : Type u} [lattice α] [comm_group α] (a : α) :

Let α be a lattice ordered commutative group and let a be an element in α with negative component a⁻. Then a⁻ dominates -a.

theorem lattice_ordered_comm_group.neg_eq_pos_inv {α : Type u} [lattice α] [comm_group α] (a : α) :

Let α be a lattice ordered commutative group and let a be an element in α. Then the negative component a⁻ of a is equal to the positive component (-a)⁺ of -a.

theorem lattice_ordered_comm_group.pos_eq_neg_inv {α : Type u} [lattice α] [comm_group α] (a : α) :

Let α be a lattice ordered commutative group and let a be an element in α. Then the positive component a⁺ of a is equal to the negative component (-a)⁻ of -a.

theorem lattice_ordered_comm_group.add_inf_eq_add_inf_add {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
c + a b = (c + a) (c + b)
theorem lattice_ordered_comm_group.mul_inf_eq_mul_inf_mul {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
c * (a b) = c * a c * b

Let α be a lattice ordered commutative group. For all elements a, b and c in α, $$c + (a ⊓ b) = (c + a) ⊓ (c + b).$$

Let α be a lattice ordered commutative group with identity 0 and let a be an element in α with negative component a⁻. Then $$a⁻ = -(a ⊓ 0).$$

theorem lattice_ordered_comm_group.pos_inv_neg {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
a = a / a

Let α be a lattice ordered commutative group and let a be an element in α with positive component a⁺ and negative component a⁻. Then a can be decomposed as the difference of a⁺ and a⁻.

@[nolint]
theorem lattice_ordered_comm_group.pos_div_neg' {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
a / a = a

Let α be a lattice ordered commutative group and let a be an element in α with positive component a⁺ and negative component a⁻. Then a⁺ and a⁻ are co-prime (and, since they are positive, disjoint).

theorem lattice_ordered_comm_group.sup_eq_mul_pos_div {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
a b = b * (a / b)

Let α be a lattice ordered commutative group, let a and b be elements in α, and let (a - b)⁺ be the positive componet of a - b. Then $$a⊔b = b + (a - b)⁺.$$

theorem lattice_ordered_comm_group.inf_eq_div_pos_div {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
a b = a / (a / b)

Let α be a lattice ordered commutative group, let a and b be elements in α, and let (a - b)⁺ be the positive componet of a - b. Then $$a⊓b = a - (a - b)⁺.$$

Let α be a lattice ordered commutative group and let a and b be elements in α with positive components a⁺ and b⁺ and negative components a⁻ and b⁻ respectively. Then b dominates a if and only if b⁺ dominates a⁺ and a⁻ dominates b⁻.

theorem lattice_ordered_comm_group.pos_mul_neg {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
|a| = a * a

Let α be a lattice ordered commutative group and let a be an element in α with absolute value |a|, positive component a⁺ and negative component a⁻. Then |a| decomposes as the sum of a⁺ and a⁻.

theorem lattice_ordered_comm_group.sup_div_inf_eq_abs_div {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
(a b) / (a b) = |b / a|

Let α be a lattice ordered commutative group, let a and b be elements in α and let |b - a| be the absolute value of b - a. Then, $$a ⊔ b - (a ⊓ b) = |b - a|.$$

theorem lattice_ordered_comm_group.sup_sq_eq_mul_mul_abs_div {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
(a b) ^ 2 = (a * b) * |b / a|

Let α be a lattice ordered commutative group, let a and b be elements in α and let |b - a| be the absolute value of b - a. Then, $$2•(a ⊔ b) = a + b + |b - a|.$$

theorem lattice_ordered_comm_group.sup_sq_eq_add_add_abs_sub {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
2 (a b) = a + b + |b - a|
theorem lattice_ordered_comm_group.two_inf_eq_mul_div_abs_div {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
(a b) ^ 2 = a * b / |b / a|

Let α be a lattice ordered commutative group, let a and b be elements in α and let |b-a| be the absolute value of b-a. Then, $$2•(a ⊓ b) = a + b - |b - a|.$$

theorem lattice_ordered_comm_group.abs_div_sup_mul_abs_div_inf {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
|(a c) / (b c)| * |a c / (b c)| = |a / b|

Let α be a lattice ordered commutative group and let a, b and c be elements in α. Let |a ⊔ c - (b ⊔ c)|, |a ⊓ c - b ⊓ c| and |a - b| denote the absolute values of a ⊔ c - (b ⊔ c), a ⊓ c - b ⊓ c and a - b respectively. Then, $$|a ⊔ c - (b ⊔ c)| + |a ⊓ c-b ⊓ c| = |a - b|.$$

theorem lattice_ordered_comm_group.abs_sub_sup_add_abs_sub_inf {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
|a c - (b c)| + |a c - b c| = |a - b|
theorem lattice_ordered_comm_group.pos_pos_id {α : Type u} [lattice α] [add_comm_group α] (a : α) (h : 0 a) :
theorem lattice_ordered_comm_group.m_pos_pos_id {α : Type u} [lattice α] [comm_group α] (a : α) (h : 1 a) :
a = a

Let α be a lattice ordered commutative group and let a be a positive element in α. Then a is equal to its positive component a⁺.

theorem lattice_ordered_comm_group.abs_pos_eq {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a : α) (h : 0 a) :
|a| = a
theorem lattice_ordered_comm_group.mabs_pos_eq {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) (h : 1 a) :
|a| = a

Let α be a lattice ordered commutative group and let a be a positive element in α. Then a is equal to its absolute value |a|.

theorem lattice_ordered_comm_group.mabs_pos {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
1 |a|

Let α be a lattice ordered commutative group and let a be an element in α. Then the absolute value |a| of a is positive.

Let α be a lattice ordered commutative group. The unary operation of taking the absolute value is idempotent.

theorem lattice_ordered_comm_group.m_Birkhoff_inequalities {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
|(a c) / (b c)| |a c / (b c)| |a / b|

Let α be a lattice ordered commutative group and let a, b and c be elements in α. Let |a ⊔ c - (b ⊔ c)|, |a ⊓ c - b ⊓ c| and |a - b| denote the absolute values of a ⊔ c - (b ⊔ c), a ⊓ c - b ⊓ c anda - b respectively. Then |a - b| dominates |a ⊔ c - (b ⊔ c)| and |a ⊓ c - b ⊓ c|.

theorem lattice_ordered_comm_group.Birkhoff_inequalities {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
|a c - (b c)| |a c - b c| |a - b|
theorem lattice_ordered_comm_group.mabs_triangle {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
|a * b| |a| * |b|

Let α be a lattice ordered commutative group. Then the absolute value satisfies the triangle inequality.