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.
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 α]
[CommGroup α]
[CovariantClass α α (*) (≤)]
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][birkhoff1942], [Fuchs][fuchs1963]) but we have not developed that here, since we are primarily interested in vector lattices.
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, ordered, group
Equations
- (_ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_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⁺
.
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⁺
.
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
- LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice α = DistribLattice.mk (_ : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)
Every lattice ordered commutative group is a distributive lattice
Equations
- LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice α = DistribLattice.mk (_ : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)
If a
is positive, then it is equal to its positive component a⁺
.
The unary operation of taking the absolute value is idempotent.
The absolute value satisfies the triangle inequality.