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.

Main statements

• pos_div_neg: Every element a of a lattice ordered group has a decomposition a⁺-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 (stated for a commutative group).

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 element a of a lattice ordered group
• a⁻ = (-a) ⊔ 0: The negative component of an element a of a lattice ordered group
• |a|ₘ = a⊔(-a): The absolute value of an element a of a lattice ordered group

Implementation notes

A lattice ordered group is a type α satisfying:

• [Lattice α]
• [CommGroup α]
• [CovariantClass α α (*) (≤)]
• [CovariantClass α α (swap (· * ·)) (· ≤ ·)]

The remainder of the 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, ordered, group

class PosPart (α : Type u_1) : Type u_1

The positive part of an element admitting a decomposition into positive and negative parts.

• pos : α → α

  The positive part function.

class NegPart (α : Type u_1) : Type u_1

The negative part of an element admitting a decomposition into positive and negative parts.

• neg : α → α

  The negative part function.

def «term_⁺» : Lean.TrailingParserDescr

The positive part function.

Equations

• «term_⁺» = Lean.ParserDescr.trailingNode `term_⁺ 1024 1024 (Lean.ParserDescr.symbol "⁺")

def «term_⁻» : Lean.TrailingParserDescr

The negative part function.

Equations

• «term_⁻» = Lean.ParserDescr.trailingNode `term_⁻ 1024 1024 (Lean.ParserDescr.symbol "⁻")

instance LatticeOrderedGroup.hasZeroLatticeHasPosPart {α : Type u} [Lattice α] [AddGroup α] : PosPart α

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

• LatticeOrderedGroup.hasZeroLatticeHasPosPart = { pos := fun (a : α) => a ⊔ 0 }

instance LatticeOrderedGroup.hasOneLatticeHasPosPart {α : Type u} [Lattice α] [Group α] : PosPart α

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

• LatticeOrderedGroup.hasOneLatticeHasPosPart = { pos := fun (a : α) => a ⊔ 1 }

theorem LatticeOrderedGroup.pos_part_def {α : Type u} [Lattice α] [AddGroup α] (a : α) : a⁺ = a ⊔ 0

theorem LatticeOrderedGroup.m_pos_part_def {α : Type u} [Lattice α] [Group α] (a : α) : a⁺ = a ⊔ 1

instance LatticeOrderedGroup.hasZeroLatticeHasNegPart {α : Type u} [Lattice α] [AddGroup α] : NegPart α

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

Equations

• LatticeOrderedGroup.hasZeroLatticeHasNegPart = { neg := fun (a : α) => -a ⊔ 0 }

instance LatticeOrderedGroup.hasOneLatticeHasNegPart {α : Type u} [Lattice α] [Group α] : NegPart α

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

Equations

• LatticeOrderedGroup.hasOneLatticeHasNegPart = { neg := fun (a : α) => a⁻¹ ⊔ 1 }

theorem LatticeOrderedGroup.neg_part_def {α : Type u} [Lattice α] [AddGroup α] (a : α) : a⁻ = -a ⊔ 0

theorem LatticeOrderedGroup.m_neg_part_def {α : Type u} [Lattice α] [Group α] (a : α) : a⁻ = a⁻¹ ⊔ 1

@[simp]

theorem LatticeOrderedGroup.pos_zero {α : Type u} [Lattice α] [AddGroup α] : 0⁺ = 0

@[simp]

theorem LatticeOrderedGroup.pos_one {α : Type u} [Lattice α] [Group α] : 1⁺ = 1

@[simp]

theorem LatticeOrderedGroup.neg_zero {α : Type u} [Lattice α] [AddGroup α] : 0⁻ = 0

@[simp]

theorem LatticeOrderedGroup.neg_one {α : Type u} [Lattice α] [Group α] : 1⁻ = 1

theorem LatticeOrderedGroup.neg_eq_neg_inf_zero {α : Type u} [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 : α) : a⁻ = -(a ⊓ 0)

theorem LatticeOrderedGroup.neg_eq_inv_inf_one {α : Type u} [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 : α) : a⁻ = (a ⊓ 1)⁻¹

theorem LatticeOrderedGroup.pos_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) : 0 ≤ a⁺

theorem LatticeOrderedGroup.one_le_pos {α : Type u} [Lattice α] [Group α] (a : α) : 1 ≤ a⁺

theorem LatticeOrderedGroup.neg_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) : 0 ≤ a⁻

theorem LatticeOrderedGroup.one_le_neg {α : Type u} [Lattice α] [Group α] (a : α) : 1 ≤ a⁻

theorem LatticeOrderedGroup.pos_nonpos_iff {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁺ ≤ 0 ↔ a ≤ 0

theorem LatticeOrderedGroup.pos_le_one_iff {α : Type u} [Lattice α] [Group α] {a : α} : a⁺ ≤ 1 ↔ a ≤ 1

theorem LatticeOrderedGroup.neg_nonpos_iff {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁻ ≤ 0 ↔ -a ≤ 0

theorem LatticeOrderedGroup.neg_le_one_iff {α : Type u} [Lattice α] [Group α] {a : α} : a⁻ ≤ 1 ↔ a⁻¹ ≤ 1

theorem LatticeOrderedGroup.pos_eq_zero_iff {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁺ = 0 ↔ a ≤ 0

theorem LatticeOrderedGroup.pos_eq_one_iff {α : Type u} [Lattice α] [Group α] {a : α} : a⁺ = 1 ↔ a ≤ 1

theorem LatticeOrderedGroup.neg_eq_zero_iff' {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁻ = 0 ↔ -a ≤ 0

theorem LatticeOrderedGroup.neg_eq_one_iff' {α : Type u} [Lattice α] [Group α] {a : α} : a⁻ = 1 ↔ a⁻¹ ≤ 1

theorem LatticeOrderedGroup.neg_eq_zero_iff {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α HAdd.hAdd LE.le] {a : α} : a⁻ = 0 ↔ 0 ≤ a

theorem LatticeOrderedGroup.neg_eq_one_iff {α : Type u} [Lattice α] [Group α] [CovariantClass α α HMul.hMul LE.le] {a : α} : a⁻ = 1 ↔ 1 ≤ a

theorem LatticeOrderedGroup.le_pos {α : Type u} [Lattice α] [AddGroup α] (a : α) : a ≤ a⁺

theorem LatticeOrderedGroup.m_le_pos {α : Type u} [Lattice α] [Group α] (a : α) : a ≤ a⁺

theorem LatticeOrderedGroup.neg_le_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) : -a ≤ a⁻

theorem LatticeOrderedGroup.inv_le_neg {α : Type u} [Lattice α] [Group α] (a : α) : a⁻¹ ≤ a⁻

theorem LatticeOrderedGroup.neg_eq_pos_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) : a⁻ = (-a)⁺

theorem LatticeOrderedGroup.neg_eq_pos_inv {α : Type u} [Lattice α] [Group α] (a : α) : a⁻ = a⁻¹⁺

theorem LatticeOrderedGroup.pos_eq_neg_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) : a⁺ = (-a)⁻

theorem LatticeOrderedGroup.pos_eq_neg_inv {α : Type u} [Lattice α] [Group α] (a : α) : a⁺ = a⁻¹⁻

@[simp]

theorem LatticeOrderedGroup.pos_sub_neg {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : a⁺ - a⁻ = a

@[simp]

theorem LatticeOrderedGroup.pos_div_neg {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : a⁺ / a⁻ = a

theorem LatticeOrderedGroup.pos_of_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : 0 ≤ a) : a⁺ = a

If a is positive, then it is equal to its positive component a⁺.

theorem LatticeOrderedGroup.pos_of_one_le {α : Type u} [Lattice α] [Group α] (a : α) (h : 1 ≤ a) : a⁺ = a

If a is positive, then it is equal to its positive component a⁺.

theorem LatticeOrderedGroup.pos_of_nonpos {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : a ≤ 0) : a⁺ = 0

theorem LatticeOrderedGroup.pos_of_le_one {α : Type u} [Lattice α] [Group α] (a : α) (h : a ≤ 1) : a⁺ = 1

theorem LatticeOrderedGroup.neg_of_inv_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : 0 ≤ -a) : a⁻ = -a

theorem LatticeOrderedGroup.neg_of_one_le_inv {α : Type u} [Lattice α] [Group α] (a : α) (h : 1 ≤ a⁻¹) : a⁻ = a⁻¹

theorem LatticeOrderedGroup.neg_of_neg_nonpos {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : -a ≤ 0) : a⁻ = 0

theorem LatticeOrderedGroup.neg_of_inv_le_one {α : Type u} [Lattice α] [Group α] (a : α) (h : a⁻¹ ≤ 1) : a⁻ = 1

theorem LatticeOrderedGroup.neg_of_nonpos {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : a ≤ 0) : a⁻ = -a

theorem LatticeOrderedGroup.neg_of_le_one {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : a ≤ 1) : a⁻ = a⁻¹

theorem LatticeOrderedGroup.pos_eq_self_of_pos_pos {α : Type u_1} [LinearOrder α] [AddCommGroup α] {x : α} (hx : 0 < x⁺) : x⁺ = x

theorem LatticeOrderedGroup.pos_eq_self_of_one_lt_pos {α : Type u_1} [LinearOrder α] [CommGroup α] {x : α} (hx : 1 < x⁺) : x⁺ = x

theorem LatticeOrderedGroup.neg_of_nonneg {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : 0 ≤ a) : a⁻ = 0

theorem LatticeOrderedGroup.neg_of_one_le {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : 1 ≤ a) : a⁻ = 1

theorem LatticeOrderedGroup.pos_add_neg {α : Type u} [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 : α) : |a| = a⁺ + a⁻

theorem LatticeOrderedGroup.pos_mul_neg {α : Type u} [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 : α) : mabs a = a⁺ * a⁻

theorem LatticeOrderedGroup.pos_abs {α : Type u} [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 : α) : |a|⁺ = |a|

theorem LatticeOrderedGroup.m_pos_abs {α : Type u} [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 : α) : (mabs a)⁺ = mabs a

theorem LatticeOrderedGroup.neg_abs {α : Type u} [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 : α) : |a|⁻ = 0

theorem LatticeOrderedGroup.m_neg_abs {α : Type u} [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 : α) : (mabs a)⁻ = 1

theorem LatticeOrderedGroup.pos_inf_neg_eq_zero {α : Type u} [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 : α) : a⁺ ⊓ a⁻ = 0

theorem LatticeOrderedGroup.pos_inf_neg_eq_one {α : Type u} [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 : α) : a⁺ ⊓ a⁻ = 1

theorem LatticeOrderedCommGroup.sup_eq_add_pos_sub {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ⊔ b = b + (a - b)⁺

theorem LatticeOrderedCommGroup.sup_eq_mul_pos_div {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ⊔ b = b * (a / b)⁺

theorem LatticeOrderedCommGroup.inf_eq_sub_pos_sub {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ⊓ b = a - (a - b)⁺

theorem LatticeOrderedCommGroup.inf_eq_div_pos_div {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ⊓ b = a / (a / b)⁺

theorem LatticeOrderedCommGroup.le_iff_pos_le_neg_ge {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻

theorem LatticeOrderedCommGroup.m_le_iff_pos_le_neg_ge {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻

def LatticeOrderedAddCommGroup.IsSolid {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) : Prop

A subset s ⊆ β, with β an AddCommGroup with a Lattice structure, is solid if for all x ∈ s and all y ∈ β such that |y| ≤ |x|, then y ∈ s.

Equations

• LatticeOrderedAddCommGroup.IsSolid s = ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, |y| ≤ |x| → y ∈ s

def LatticeOrderedAddCommGroup.solidClosure {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) : Set β

The solid closure of a subset s is the smallest superset of s that is solid.

Equations

• LatticeOrderedAddCommGroup.solidClosure s = {y : β | ∃ x ∈ s, |y| ≤ |x|}

theorem LatticeOrderedAddCommGroup.isSolid_solidClosure {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) : LatticeOrderedAddCommGroup.IsSolid (LatticeOrderedAddCommGroup.solidClosure s)

theorem LatticeOrderedAddCommGroup.solidClosure_min {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) (t : Set β) (h1 : s ⊆ t) (h2 : LatticeOrderedAddCommGroup.IsSolid t) : LatticeOrderedAddCommGroup.solidClosure s ⊆ t