Lattice-ordered groups and vector lattices

This file develops the basic order-theoretic algebra of lattice-ordered groups and vector lattices. The first part works in the general setting of an additive commutative group with a compatible lattice order (IsOrderedAddMonoid): it establishes properties of x⁺, x⁻, and |x|, together with order-theoretic suprema and infima lemmas. The second part adds a real scalar multiplication (VectorLattice) and proves that positive scalars distribute over ⊔ and ⊓, culminating in abs_smul'. The Archimedean case is treated at the end.

class VectorLattice (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] extends Module ℝ X, PosSMulMono ℝ X : Type u_1

A real vector lattice is a real module whose scalar multiplication is monotone for non-negative scalars and is compatible with the lattice-ordered additive structure.

• smul : ℝ → X → X
• mul_smul (x y : ℝ) (b : X) : (x * y) • b = x • y • b
• one_smul (b : X) : 1 • b = b
• smul_zero (a : ℝ) : a • 0 = 0
• smul_add (a : ℝ) (x y : X) : a • (x + y) = a • x + a • y
• add_smul (r s : ℝ) (x : X) : (r + s) • x = r • x + s • x
• zero_smul (x : X) : 0 • x = 0
• smul_le_smul_of_nonneg_left ⦃a : ℝ⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : X⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂

@[instance_reducible]

noncomputable instance instVectorLatticeReal : VectorLattice ℝ

The real numbers form a vector lattice over themselves.

Equations

• instVectorLatticeReal = { toModule := Semiring.toModule, toPosSMulMono := instVectorLatticeReal._proof_1 }

theorem abs_eq_zero_iff_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : |x| = 0 ↔ x = 0

An element of a lattice-ordered group is zero iff its absolute value is zero. Extends Mathlib.Algebra.Order.Module.Basic.abs_eq_zero to the non-total-order setting.

theorem uniqueness_posPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) {u v : X} (hdif : x = u - v) (udisv : u ⊓ v = 0) : u = x⁺

If x = u - v with u ⊓ v = 0, then u is the positive part of x.

theorem sup_eq_add_posPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y : X) : x ⊔ y = x + (y - x)⁺

x ⊔ y = x + (y - x)⁺.

theorem inf_eq_sub_posPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y : X) : x ⊓ y = x - (x - y)⁺

x ⊓ y = x - (x - y)⁺.

theorem sub_inf_eq_posPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y : X) : x - x ⊓ y = (x - y)⁺

x - x ⊓ y = (x - y)⁺.

theorem posPart_add_le {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y : X) : (x + y)⁺ ≤ x⁺ + y⁺

The positive part is subadditive: (x + y)⁺ ≤ x⁺ + y⁺.

theorem posPart_le_abs {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : x⁺ ≤ |x|

The positive part is bounded by the modulus.

theorem negPart_le_abs {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : x⁻ ≤ |x|

The negative part is bounded by the modulus.

theorem inf_le_inf_add_inf_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x a b : X) (hx : 0 ≤ x) (ha : 0 ≤ a) (hb : 0 ≤ b) : x ⊓ (a + b) ≤ x ⊓ a + x ⊓ b

For non-negative x, a, b: x ⊓ (a + b) ≤ x ⊓ a + x ⊓ b.

theorem isLUB_const_add {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A : Set X} {a : X} (x : X) (h : IsLUB A a) : IsLUB ((fun (z : X) => x + z) '' A) (x + a)

Translation preserves suprema: x + sup A = sup(x + A).

theorem isGLB_const_add {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A : Set X} {a : X} (x : X) (h : IsGLB A a) : IsGLB ((fun (z : X) => x + z) '' A) (x + a)

Translation preserves infima: x + inf A = inf(x + A).

theorem isLUB_inf_const {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A : Set X} {a : X} (x : X) (h : IsLUB A a) : IsLUB ((fun (z : X) => x ⊓ z) '' A) (x ⊓ a)

Meet distributes over arbitrary suprema: x ⊓ sup A = sup {x ⊓ a : a ∈ A}.

theorem isGLB_sup_const {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A : Set X} {a : X} (x : X) (h : IsGLB A a) : IsGLB ((fun (z : X) => x ⊔ z) '' A) (x ⊔ a)

Join distributes over arbitrary infima: x ⊔ inf A = inf {x ⊔ a : a ∈ A}.

theorem isGLB_add_sets {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A B : Set X} {a b : X} (hA : IsGLB A a) (hB : IsGLB B b) : IsGLB ((fun (p : X × X) => p.1 + p.2) '' A ×ˢ B) (a + b)

inf(A + B) = inf A + inf B.

theorem isGLB_sup_sets {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A B : Set X} {a b : X} (hA : IsGLB A a) (hB : IsGLB B b) : IsGLB ((fun (p : X × X) => p.1 ⊔ p.2) '' A ×ˢ B) (a ⊔ b)

inf(A ∨ B) = inf A ∨ inf B, where A ∨ B = {p ⊔ q : p ∈ A, q ∈ B}.

theorem isGLB_union {X : Type u_1} [Lattice X] {A B : Set X} {a b : X} (hA : IsGLB A a) (hB : IsGLB B b) : IsGLB (A ∪ B) (a ⊓ b)

inf(A ∪ B) = (inf A) ⊓ (inf B).

theorem nonneg_smul_sup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x y : X) (a : ℝ) (nonneg : a ≥ 0) : a • (x ⊔ y) = a • x ⊔ a • y

A non-negative scalar distributes over ⊔.

theorem posPart_smul_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {a : ℝ} (ha : 0 ≤ a) (x : X) : (a • x)⁺ = a • x⁺

A non-negative scalar commutes with the positive part.

theorem isLUB_smul_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {A : Set X} {a : X} {lam : ℝ} (hlam : 0 ≤ lam) (h : IsLUB A a) : IsLUB ((fun (z : X) => lam • z) '' A) (lam • a)

A non-negative scalar distributes over suprema: λ • sup A = sup (λ • A).

theorem isGLB_smul_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {A : Set X} {a : X} {lam : ℝ} (hlam : 0 ≤ lam) (h : IsGLB A a) : IsGLB ((fun (z : X) => lam • z) '' A) (lam • a)

A non-negative scalar distributes over infima: λ • inf A = inf (λ • A).

theorem nonneg_smul_inf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x y : X) (a : ℝ) (nonneg : a ≥ 0) : a • (x ⊓ y) = a • x ⊓ a • y

A non-negative scalar distributes over ⊓.

theorem sup_smul_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : X) (a b : ℝ) (h : 0 ≤ x) : max a b • x = a • x ⊔ b • x

Scalar sup distributes over a non-negative element.

theorem inf_smul_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : X) (a b : ℝ) (h : 0 ≤ x) : min a b • x = a • x ⊓ b • x

Scalar inf distributes over a non-negative element.

theorem abs_smul' {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : X) (a : ℝ) : |a • x| = |a| • |x|

|a • x| = |a| • |x| in a vector lattice. Extends the Mathlib result of the same name from total orders to lattice orders.

class IsVLArchimedean (X : Type u_2) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] : Prop

A lattice-ordered group is Archimedean (in the vector-lattice sense) when the only non-negative element all of whose multiples are bounded is zero: 0 ≤ x and ∀ n, n • x ≤ y imply x = 0. This is the standard Archimedean property for partially ordered groups; it is weaker than Mathlib's Archimedean class, which is stated for linearly ordered monoids.

• le_zero_of_forall_nsmul_le {x y : X} : (∀ (n : ℕ), n • x ≤ y) → x ≤ 0

theorem isVLArchimedean_of_eq_zero_of_nonneg_of_forall_nsmul_le {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (H : ∀ {x y : X}, 0 ≤ x → (∀ (n : ℕ), n • x ≤ y) → x = 0) : IsVLArchimedean X

Constructor from the non-negative formulation of the Archimedean property.

theorem isVLArchimedean_iff_le_zero_of_forall_nsmul_le {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] : IsVLArchimedean X ↔ ∀ {x y : X}, (∀ (n : ℕ), n • x ≤ y) → x ≤ 0

In a vector lattice, being Archimedean is equivalent to the condition that n • x ≤ y for all n : ℕ implies x ≤ 0.

theorem IsVLArchimedean.eq_zero_of_nonneg_of_forall_nsmul_le {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [IsVLArchimedean X] {x y : X} (hx : 0 ≤ x) (h : ∀ (n : ℕ), n • x ≤ y) : x = 0

Non-negative form of the Archimedean property.

theorem isVLArchimedean_iff_isGLB_inv_smul {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : IsVLArchimedean X ↔ ∀ (u : X), 0 ≤ u → IsGLB {v : X | ∃ (n : ℕ), 0 < n ∧ v = (↑n)⁻¹ • u} 0

A vector lattice is Archimedean iff for every positive u, the infimum of (1/n) • u over n ≥ 1 equals 0.

theorem infinitesimal_eq_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [IsVLArchimedean X] {x y : X} (h : ∀ (n : ℕ), n • |x| ≤ y) : x = 0

An element whose absolute-value multiples are bounded must be zero.

theorem exists_not_nonneg_not_nonpos_of_one_lt_rank {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [IsVLArchimedean X] (h : 1 < Module.rank ℝ X) : ∃ (x : X), ¬0 ≤ x ∧ ¬x ≤ 0

If X is an Archimedean vector lattice with more than one dimension, then there exists a vector in X which is neither positive nor negative.