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 #
pos_div_neg
: Every elementa
of a lattice ordered commutative group has a decompositiona⁺-a⁻
into the difference of the positive and negative component.pos_inf_neg_eq_one
: The positive and negative components are coprime.abs_triangle
: The absolute value operation satisfies the triangle inequality.
It is shown that the inf and sup operations are related to the absolute value operation by a number of equations and inequalities.
Notations #
a⁺ = a ⊔ 0
: The positive component of an elementa
of a lattice ordered commutative groupa⁻ = (-a) ⊔ 0
: The negative component of an elementa
of a lattice ordered commutative group
|a| = a⊔(-a)
: The absolute value of an elementa
of a lattice ordered commutative group
Implementation notes #
A lattice ordered commutative group is a type α
satisfying:
[lattice α]
[comm_group α]
[covariant_class α α (*) (≤)]
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 #
- Birkhoff, Lattice-ordered Groups
- Bourbaki, Algebra II
- Fuchs, Partially Ordered Algebraic Systems
- Zaanen, Lectures on "Riesz Spaces"
- Banasiak, Banach Lattices in Applications
Tags #
lattice, ordered, group
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
- lattice_ordered_comm_group.has_one_lattice_has_pos_part = {pos := λ (a : α), a ⊔ 1}
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
- lattice_ordered_comm_group.has_zero_lattice_has_pos_part = {pos := λ (a : α), a ⊔ 0}
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⁻
.
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⁻
.
Every lattice ordered commutative additive group is a distributive lattice
Equations
- lattice_ordered_comm_group.lattice_ordered_add_comm_group_to_distrib_lattice α = {sup := lattice.sup s, le := lattice.le s, lt := lattice.lt s, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf s, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
Every lattice ordered commutative group is a distributive lattice
Equations
- lattice_ordered_comm_group.lattice_ordered_comm_group_to_distrib_lattice α = {sup := lattice.sup s, le := lattice.le s, lt := lattice.lt s, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf s, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
If a
is positive, then it is equal to its positive component a⁺
.
If a
is positive, then it is equal to its positive component a⁺
.
The unary operation of taking the absolute value is idempotent.
The unary operation of taking the absolute value is idempotent.
The absolute value satisfies the triangle inequality.