mathlib documentation

algebra.order.lattice_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 {α : 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 {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
c * (a b) = c * a c * b
theorem add_inf {α : 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_inf {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
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 : α) :
theorem inv_inf_eq_sup_inv {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (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
@[protected, instance]

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

Equations
@[protected, instance]

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
theorem lattice_ordered_comm_group.pos_part_def {α : Type u} [lattice α] [add_comm_group α] (a : α) :
a = a 0
theorem lattice_ordered_comm_group.m_pos_part_def {α : Type u} [lattice α] [comm_group α] (a : α) :
a = a 1
@[protected, instance]

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
@[protected, instance]

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

Equations
theorem lattice_ordered_comm_group.m_neg_part_def {α : Type u} [lattice α] [comm_group α] (a : α) :
theorem lattice_ordered_comm_group.neg_part_def {α : Type u} [lattice α] [add_comm_group α] (a : α) :
a = -a 0
@[simp]
theorem lattice_ordered_comm_group.pos_one {α : Type u} [lattice α] [comm_group α] :
1 = 1
@[simp]
theorem lattice_ordered_comm_group.pos_zero {α : Type u} [lattice α] [add_comm_group α] :
0 = 0
@[simp]
theorem lattice_ordered_comm_group.neg_zero {α : Type u} [lattice α] [add_comm_group α] :
0 = 0
@[simp]
theorem lattice_ordered_comm_group.neg_one {α : Type u} [lattice α] [comm_group α] :
1 = 1
theorem lattice_ordered_comm_group.le_mabs {α : Type u} [lattice α] [comm_group α] (a : α) :
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 : α) :
theorem lattice_ordered_comm_group.one_le_pos {α : Type u} [lattice α] [comm_group α] (a : α) :
1 a
theorem lattice_ordered_comm_group.pos_nonneg {α : Type u} [lattice α] [add_comm_group α] (a : α) :
0 a
theorem lattice_ordered_comm_group.neg_nonneg {α : Type u} [lattice α] [add_comm_group α] (a : α) :
0 a
theorem lattice_ordered_comm_group.one_le_neg {α : Type u} [lattice α] [comm_group α] (a : α) :
1 a
theorem lattice_ordered_comm_group.pos_le_one_iff {α : Type u} [lattice α] [comm_group α] {a : α} :
a 1 a 1
theorem lattice_ordered_comm_group.pos_nonpos_iff {α : Type u} [lattice α] [add_comm_group α] {a : α} :
a 0 a 0
theorem lattice_ordered_comm_group.neg_nonpos_iff {α : Type u} [lattice α] [add_comm_group α] {a : α} :
a 0 -a 0
theorem lattice_ordered_comm_group.neg_le_one_iff {α : Type u} [lattice α] [comm_group α] {a : α} :
theorem lattice_ordered_comm_group.pos_eq_zero_iff {α : Type u} [lattice α] [add_comm_group α] {a : α} :
a = 0 a 0
theorem lattice_ordered_comm_group.pos_eq_one_iff {α : Type u} [lattice α] [comm_group α] {a : α} :
a = 1 a 1
theorem lattice_ordered_comm_group.neg_eq_one_iff' {α : Type u} [lattice α] [comm_group α] {a : α} :
a = 1 a⁻¹ 1
theorem lattice_ordered_comm_group.neg_eq_zero_iff' {α : Type u} [lattice α] [add_comm_group α] {a : α} :
a = 0 -a 0
theorem lattice_ordered_comm_group.le_pos {α : Type u} [lattice α] [add_comm_group α] (a : α) :
a a
theorem lattice_ordered_comm_group.m_le_pos {α : Type u} [lattice α] [comm_group α] (a : α) :
a a
theorem lattice_ordered_comm_group.neg_le_neg {α : Type u} [lattice α] [add_comm_group α] (a : α) :
theorem lattice_ordered_comm_group.inv_le_neg {α : Type u} [lattice α] [comm_group α] (a : α) :
theorem lattice_ordered_comm_group.neg_eq_pos_inv {α : Type u} [lattice α] [comm_group α] (a : α) :
theorem lattice_ordered_comm_group.neg_eq_pos_neg {α : Type u} [lattice α] [add_comm_group α] (a : α) :
a = (-a)
theorem lattice_ordered_comm_group.pos_eq_neg_neg {α : Type u} [lattice α] [add_comm_group α] (a : α) :
a = (-a)
theorem lattice_ordered_comm_group.pos_eq_neg_inv {α : Type u} [lattice α] [comm_group α] (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
@[simp]
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
@[simp]
theorem lattice_ordered_comm_group.sup_eq_add_pos_sub {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
a b = b + (a - b)
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)
theorem lattice_ordered_comm_group.inf_eq_sub_pos_sub {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
a b = a - (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)
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|
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|
theorem lattice_ordered_comm_group.inf_sq_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|
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|
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_of_nonneg {α : Type u} [lattice α] [add_comm_group α] (a : α) (h : 0 a) :
a = a

If a is positive, then it is equal to its positive component a⁺.

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

If a is positive, then it is equal to its positive component a⁺.

theorem lattice_ordered_comm_group.pos_eq_self_of_one_lt_pos {α : Type u_1} [linear_order α] [comm_group α] {x : α} (hx : 1 < x) :
x = x
theorem lattice_ordered_comm_group.pos_eq_self_of_pos_pos {α : Type u_1} [linear_order α] [add_comm_group α] {x : α} (hx : 0 < x) :
x = x
theorem lattice_ordered_comm_group.pos_of_nonpos {α : Type u} [lattice α] [add_comm_group α] (a : α) (h : a 0) :
a = 0
theorem lattice_ordered_comm_group.pos_of_le_one {α : Type u} [lattice α] [comm_group α] (a : α) (h : a 1) :
a = 1
theorem lattice_ordered_comm_group.neg_of_one_le_inv {α : Type u} [lattice α] [comm_group α] (a : α) (h : 1 a⁻¹) :
theorem lattice_ordered_comm_group.neg_of_inv_nonneg {α : Type u} [lattice α] [add_comm_group α] (a : α) (h : 0 -a) :
a = -a
theorem lattice_ordered_comm_group.neg_of_inv_le_one {α : Type u} [lattice α] [comm_group α] (a : α) (h : a⁻¹ 1) :
a = 1
theorem lattice_ordered_comm_group.neg_of_neg_nonpos {α : Type u} [lattice α] [add_comm_group α] (a : α) (h : -a 0) :
a = 0
theorem lattice_ordered_comm_group.neg_of_nonpos {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a : α) (h : a 0) :
a = -a
theorem lattice_ordered_comm_group.neg_of_le_one {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) (h : a 1) :
theorem lattice_ordered_comm_group.neg_of_one_le {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) (h : 1 a) :
a = 1
theorem lattice_ordered_comm_group.neg_of_nonneg {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a : α) (h : 0 a) :
a = 0
theorem lattice_ordered_comm_group.mabs_of_one_le {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) (h : 1 a) :
|a| = a
theorem lattice_ordered_comm_group.abs_of_nonneg {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a : α) (h : 0 a) :
|a| = a
@[simp]
theorem lattice_ordered_comm_group.mabs_mabs {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a : α) :

The unary operation of taking the absolute value is idempotent.

@[simp]

The unary operation of taking the absolute value is idempotent.

theorem lattice_ordered_comm_group.mabs_sup_div_sup_le_mabs {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
|(a c) / (b c)| |a / b|
theorem lattice_ordered_comm_group.mabs_inf_div_inf_le_mabs {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
|(a c) / (b c)| |a / b|
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|
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_mul_le {α : Type u} [lattice α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
|a * b| |a| * |b|

The absolute value satisfies the triangle inequality.

theorem lattice_ordered_comm_group.abs_add_le {α : Type u} [lattice α] [add_comm_group α] [covariant_class α α has_add.add has_le.le] (a b : α) :
|a + b| |a| + |b|

The absolute value satisfies the triangle inequality.

theorem lattice_ordered_comm_group.abs_neg_comm {α : Type u} [lattice α] [add_comm_group α] (a b : α) :
|a - b| = |b - a|
theorem lattice_ordered_comm_group.abs_inv_comm {α : Type u} [lattice α] [comm_group α] (a b : α) :
|a / b| = |b / a|