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.
A lattice ordered group is a type α
satisfying:
Lattice α
CommGroup α
CovariantClass α α (· * ·) (· ≤ ·)
CovariantClass α α (swap (· * ·)) (· ≤ ·)
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,Fuchs) but we do not yet have the machinery to establish this in mathlib.
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, order, group
theorem
nsmul_two_semiclosed
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
{a : α}
(ha : 0 ≤ 2 • a)
:
0 ≤ a
theorem
pow_two_semiclosed
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1]
{a : α}
(ha : 1 ≤ a ^ 2)
:
1 ≤ a
theorem
inf_add_sup
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(a : α)
(b : α)
:
def
AddCommGroup.toDistribLattice
(α : Type u_3)
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
Every lattice ordered commutative additive group is a distributive lattice
Equations
Instances For
theorem
AddCommGroup.toDistribLattice.proof_1
(α : Type u_1)
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(x : α)
(y : α)
(z : α)
:
def
CommGroup.toDistribLattice
(α : Type u_3)
[Lattice α]
[CommGroup α]
[CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1]
:
Every lattice ordered commutative group is a distributive lattice.