# 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.

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][birkhoff1942],[Fuchs][fuchs1963]) but we do not yet have the machinery to establish this in mathlib.

## 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, order, group

theorem add_sup {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c + a b = (c + a) (c + b)
theorem mul_sup {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c * (a b) = c * a c * b
theorem sup_add {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b + c = (a + c) (b + c)
theorem sup_mul {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) * c = a * c b * c
theorem add_inf {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c + a b = (c + a) (c + b)
theorem mul_inf {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c * (a b) = c * a c * b
theorem inf_add {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b + c = (a + c) (b + c)
theorem inf_mul {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) * c = a * c b * c
theorem neg_sup {α : Type u_1} [] [] [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 : α) (b : α) :
-(a b) = -a -b
theorem inv_sup {α : Type u_1} [] [] [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 : α) (b : α) :
theorem neg_inf {α : Type u_1} [] [] [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 : α) (b : α) :
-(a b) = -a -b
theorem inv_inf {α : Type u_1} [] [] [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 : α) (b : α) :
theorem sub_sup {α : Type u_1} [] [] [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 : α) (b : α) (c : α) :
c - a b = (c - a) (c - b)
theorem div_sup {α : Type u_1} [] [] [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 : α) (b : α) (c : α) :
c / (a b) = c / a c / b
theorem sup_sub {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b - c = (a - c) (b - c)
theorem sup_div {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) / c = a / c b / c
theorem sub_inf {α : Type u_1} [] [] [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 : α) (b : α) (c : α) :
c - a b = (c - a) (c - b)
theorem div_inf {α : Type u_1} [] [] [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 : α) (b : α) (c : α) :
c / (a b) = c / a c / b
theorem inf_sub {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b - c = (a - c) (b - c)
theorem inf_div {α : Type u_1} [] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) / c = a / c b / c
theorem nsmul_two_semiclosed {α : Type u_1} [] [] [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} [] [] [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} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a b + a b = a + b
theorem inf_mul_sup {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
(a b) * (a b) = a * b
def AddCommGroup.toDistribLattice (α : Type u_3) [] [] [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) [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (x : α) (y : α) (z : α) :
(x y) (x z) x y z
def CommGroup.toDistribLattice (α : Type u_3) [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :

Every lattice ordered commutative group is a distributive lattice.

Equations
Instances For