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} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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_sub {α : Type u_1} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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_sub {α : Type u_1} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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} [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 : α) (b : α) : -(a ⊔ b) = -a ⊓ -b

theorem inv_sup {α : 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 : α) (b : α) : (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹

theorem neg_inf {α : 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 : α) (b : α) : -(a ⊓ b) = -a ⊔ -b

theorem inv_inf {α : 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 : α) (b : α) : (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹

theorem sub_sup {α : 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 : α) (b : α) (c : α) : c - a ⊔ b = (c - a) ⊓ (c - b)

theorem div_sup {α : 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 : α) (b : α) (c : α) : c / (a ⊔ b) = c / a ⊓ c / b

theorem sub_inf {α : 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 : α) (b : α) (c : α) : c - a ⊓ b = (c - a) ⊔ (c - b)

theorem div_inf {α : 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 : α) (b : α) (c : α) : c / (a ⊓ b) = c / a ⊔ c / b

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 : α) : a ⊓ b + a ⊔ b = a + b

theorem inf_mul_sup {α : Type u_1} [Lattice α] [CommGroup α] [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) [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : DistribLattice α

Every lattice ordered commutative additive group is a distributive lattice

Equations

• AddCommGroup.toDistribLattice α = DistribLattice.mk ⋯

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 : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ 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] : DistribLattice α

Every lattice ordered commutative group is a distributive lattice.

Equations

• CommGroup.toDistribLattice α = DistribLattice.mk ⋯