Sublattices of vector lattices

A vector sublattice of a vector lattice is a linear subspace closed under the lattice operations. Since all lattice operations are expressible in terms of each other, it suffices that the subspace be closed under any one operation — for example, ⊔ or |·|. The key characterisation proved here is that closure under absolute value is equivalent to the sublattice property. The file also constructs generated sublattices, describes them in terms of sup- and inf-closures, and records the induced normed vector lattice structure on closed sublattices.

Sup- and inf-closure of a pointed cone

In a vector lattice, the sup-closure and inf-closure of a pointed cone C ⊆ X are again pointed cones.

theorem PointedCone.add_mem_supClosure_of_addClosed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {s : Set X} (hadd : ∀ ⦃a : X⦄, a ∈ s → ∀ ⦃b : X⦄, b ∈ s → a + b ∈ s) {x y : X} (hx : x ∈ _root_.supClosure s) (hy : y ∈ _root_.supClosure s) : x + y ∈ _root_.supClosure s

If s is closed under addition, so is its sup-closure.

theorem PointedCone.smul_mem_supClosure_of_smulClosed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s : Set X} (hsmul : ∀ ⦃a : ℝ⦄, 0 ≤ a → ∀ ⦃x : X⦄, x ∈ s → a • x ∈ s) {a : ℝ} (ha : 0 ≤ a) {x : X} (hx : x ∈ _root_.supClosure s) : a • x ∈ _root_.supClosure s

If s is closed under non-negative scaling, so is its sup-closure.

theorem PointedCone.add_mem_infClosure_of_addClosed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {s : Set X} (hadd : ∀ ⦃a : X⦄, a ∈ s → ∀ ⦃b : X⦄, b ∈ s → a + b ∈ s) {x y : X} (hx : x ∈ _root_.infClosure s) (hy : y ∈ _root_.infClosure s) : x + y ∈ _root_.infClosure s

If s is closed under addition, so is its inf-closure.

theorem PointedCone.smul_mem_infClosure_of_smulClosed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s : Set X} (hsmul : ∀ ⦃a : ℝ⦄, 0 ≤ a → ∀ ⦃x : X⦄, x ∈ s → a • x ∈ s) {a : ℝ} (ha : 0 ≤ a) {x : X} (hx : x ∈ _root_.infClosure s) : a • x ∈ _root_.infClosure s

If s is closed under non-negative scaling, so is its inf-closure.

def PointedCone.supClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (C : PointedCone ℝ X) : PointedCone ℝ X

The sup-closure of a pointed cone is a pointed cone.

Equations

• C.supClosure = { carrier := supClosure ↑C, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem PointedCone.coe_supClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (C : PointedCone ℝ X) : ↑C.supClosure = _root_.supClosure ↑C

def PointedCone.infClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (C : PointedCone ℝ X) : PointedCone ℝ X

The inf-closure of a pointed cone is a pointed cone.

Equations

• C.infClosure = { carrier := infClosure ↑C, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem PointedCone.coe_infClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (C : PointedCone ℝ X) : ↑C.infClosure = _root_.infClosure ↑C

structure VectorSublattice (X : Type u_2) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] extends Submodule ℝ X : Type u_2

A VectorSublattice of a vector lattice X is a linear subspace closed under ⊔. This is the bundled version: it extends Submodule ℝ X with lattice closure.

• carrier : Set X
• add_mem' {a b : X} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : ℝ) {x : X} : x ∈ self.carrier → c • x ∈ self.carrier
• sup_mem' {x y : X} : x ∈ self.carrier → y ∈ self.carrier → x ⊔ y ∈ self.carrier

@[instance_reducible]

instance VectorSublattice.instSetLike {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : SetLike (VectorSublattice X) X

Equations

• VectorSublattice.instSetLike = { coe := fun (Y : VectorSublattice X) => Y.carrier, coe_injective := ⋯ }

theorem VectorSublattice.sup_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) {x y : X} (hx : x ∈ Y) (hy : y ∈ Y) : x ⊔ y ∈ Y

A vector sublattice is closed under ⊔.

theorem VectorSublattice.inf_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) {x y : X} (hx : x ∈ Y) (hy : y ∈ Y) : x ⊓ y ∈ Y

A vector sublattice is closed under ⊓.

theorem VectorSublattice.posPart_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) {x : X} (hx : x ∈ Y) : x⁺ ∈ Y

A vector sublattice is closed under the positive part.

theorem VectorSublattice.negPart_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) {x : X} (hx : x ∈ Y) : x⁻ ∈ Y

A vector sublattice is closed under the negative part.

theorem VectorSublattice.abs_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) {x : X} (hx : x ∈ Y) : |x| ∈ Y

A vector sublattice is closed under absolute value.

theorem VectorSublattice.isSublattice {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : IsSublattice ↑Y

The underlying set of a vector sublattice is an IsSublattice.

Construction from absolute-value closure

def VectorSublattice.ofAbsClosed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (M : Submodule ℝ X) (h : ∀ x ∈ M, |x| ∈ M) : VectorSublattice X

Build a VectorSublattice from a submodule closed under |·|.

Equations

• VectorSublattice.ofAbsClosed M h = { toSubmodule := M, sup_mem' := ⋯ }

theorem VectorSublattice.abs_mem_iff_sup_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (M : Submodule ℝ X) : (∀ x ∈ M, |x| ∈ M) ↔ ∀ (x y : X), x ∈ M → y ∈ M → x ⊔ y ∈ M

A submodule is a vector sublattice iff it is closed under absolute value.

Coercion to submodule

theorem VectorSublattice.toSubmodule_injective {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Function.Injective toSubmodule

The coercion to Submodule ℝ X is injective.

@[simp]

theorem VectorSublattice.coe_toSubmodule {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : ↑Y.toSubmodule = ↑Y

A vector sublattice and its underlying submodule have the same carrier.

Coercion to pointed cone

Every vector sublattice, being a linear subspace, is in particular a pointed convex cone.

@[instance_reducible]

instance VectorSublattice.instCoeHeadPointedConeReal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : CoeHead (VectorSublattice X) (PointedCone ℝ X)

Every vector sublattice is (canonically) a pointed cone.

Equations

• VectorSublattice.instCoeHeadPointedConeReal = { coe := fun (Y : VectorSublattice X) => let __AddSubmonoid := Y.toAddSubmonoid; { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } }

theorem VectorSublattice.coe_toPointedCone {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : ↑(let __AddSubmonoid := Y.toAddSubmonoid; { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }) = ↑Y

Lattice structure on the underlying subtype

A vector sublattice Y inherits a lattice and vector-lattice structure from the ambient space, with ⊔ and ⊓ computed pointwise.

@[instance_reducible]

noncomputable instance VectorSublattice.instLatticeSubtype {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : Lattice ↥Y.toSubmodule

The lattice structure on the underlying subtype of a vector sublattice.

Equations

• Y.instLatticeSubtype = Subtype.lattice ⋯ ⋯

instance VectorSublattice.instIsOrderedAddMonoidSubtype {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : IsOrderedAddMonoid ↥Y.toSubmodule

The subtype of a vector sublattice is an ordered additive monoid.

instance VectorSublattice.instPosSMulMonoSubtype {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : PosSMulMono ℝ ↥Y.toSubmodule

Scalar multiplication by non-negative reals is monotone on the subtype of a vector sublattice.

@[instance_reducible]

instance VectorSublattice.instVectorLatticeSubtype {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : VectorLattice ↥Y.toSubmodule

The subtype of a vector sublattice is itself a vector lattice.

Equations

• Y.instVectorLatticeSubtype = { toModule := Y.module, toPosSMulMono := ⋯ }

Lattice structure on VectorSublattice X

The collection of vector sublattices of X is ordered by inclusion. It contains the whole space ⊤ = X and the zero subspace ⊥ = {0}, and is closed under arbitrary intersections.

@[instance_reducible]

instance VectorSublattice.instPartialOrder {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : PartialOrder (VectorSublattice X)

Equations

• VectorSublattice.instPartialOrder = PartialOrder.lift (fun (Y : VectorSublattice X) => ↑Y) ⋯

@[instance_reducible]

instance VectorSublattice.instTop {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Top (VectorSublattice X)

The whole space X is a vector sublattice.

Equations

• VectorSublattice.instTop = { top := let __Submodule := ⊤; { toSubmodule := __Submodule, sup_mem' := ⋯ } }

@[simp]

theorem VectorSublattice.mem_top {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x : X} : x ∈ ⊤

Every element belongs to ⊤.

@[instance_reducible]

instance VectorSublattice.instBot {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Bot (VectorSublattice X)

The zero subspace {0} is a vector sublattice.

Equations

• VectorSublattice.instBot = { bot := let __Submodule := ⊥; { toSubmodule := __Submodule, sup_mem' := ⋯ } }

@[simp]

theorem VectorSublattice.mem_bot {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x : X} : x ∈ ⊥ ↔ x = 0

An element of ⊥ is zero.

@[instance_reducible]

instance VectorSublattice.instInfSet {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : InfSet (VectorSublattice X)

Arbitrary intersections of vector sublattices are vector sublattices.

Equations

• One or more equations did not get rendered due to their size.

The vector sublattice generated by a set

The vector sublattice generated by a set s ⊆ X is by definition the smallest vector sublattice of X containing s, obtained as the infimum of all vector sublattices containing s.

def VectorSublattice.generated {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (s : Set X) : VectorSublattice X

The vector sublattice generated by a set s: the smallest vector sublattice of X containing s.

Equations

• VectorSublattice.generated s = sInf {Y : VectorSublattice X | s ⊆ ↑Y}

theorem VectorSublattice.subset_generated {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (s : Set X) : s ⊆ ↑(generated s)

The generating set is contained in the vector sublattice it generates.

theorem VectorSublattice.generated_le {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s : Set X} {Y : VectorSublattice X} (h : s ⊆ ↑Y) : generated s ≤ Y

The vector sublattice generated by s is contained in every vector sublattice containing s.

theorem VectorSublattice.generated_submodule_eq_supClosure_infClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (M : Submodule ℝ X) : ↑(generated ↑M) = supClosure (infClosure ↑M)

The vector sublattice generated by a linear subspace M coincides with the sup-closure of the inf-closure of M.

theorem VectorSublattice.generated_submodule_eq_infClosure_supClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (M : Submodule ℝ X) : ↑(generated ↑M) = infClosure (supClosure ↑M)

The vector sublattice generated by a linear subspace M coincides with the inf-closure of the sup-closure of M.

theorem VectorSublattice.generated_pointedCone_eq_sub_supClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (C : PointedCone ℝ X) : ↑(generated ↑C) = supClosure ↑C - supClosure ↑C

The vector sublattice generated by a pointed cone C coincides with the difference set of the sup-closure of C with itself.

theorem VectorSublattice.generated_pointedCone_eq_sub_infClosure {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (C : PointedCone ℝ X) : ↑(generated ↑C) = infClosure ↑C - infClosure ↑C

The vector sublattice generated by a pointed cone C coincides with the difference set of the inf-closure of C with itself.

theorem VectorSublattice.generated_eq_span_of_pairwise_vlDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {A : Set X} (hA : A.Pairwise IsVLDisjoint) (hA_nn : ∀ a ∈ A, 0 ≤ a) : (generated A).toSubmodule = Submodule.span ℝ A

The vector sublattice generated by a set of pairwise lattice-disjoint, non-negative elements coincides with its linear span.

theorem LLexpr.generated_range_eq_combinations {n : ℕ} {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) : ↑(VectorSublattice.generated (Set.range x)) = combinations x

The sublattice generated by the image of a tuple x : Fin n → X coincides with the set of lattice-linear combinations of x.

theorem LLexpr.generated_eq_iUnion_combinations {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (s : Set X) : ↑(VectorSublattice.generated s) = ⋃ (n : ℕ), ⋃ (x : Fin n → ↑s), combinations (Subtype.val ∘ x)

The sublattice generated by a set s coincides with the union, over all natural numbers n and all n-tuples x with values in s, of the sets of lattice-linear combinations of x.

Normed and Banach lattice structure on sublattices

@[instance_reducible]

instance VectorSublattice.instNormedVectorLatticeSubtype {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (Y : VectorSublattice X) : NormedVectorLattice ↥Y.toSubmodule

A vector sublattice of a normed vector lattice is itself a normed vector lattice under the induced norm and lattice operations.

Equations

• Y.instNormedVectorLatticeSubtype = { toVectorLattice := Y.instVectorLatticeSubtype, toHasSolidNorm := ⋯, toNormSMulClass := ⋯ }

noncomputable def VectorSublattice.topologicalClosure {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (Y : VectorSublattice X) : VectorSublattice X

The closure of a vector sublattice in a normed vector lattice is again a vector sublattice.

Equations

• Y.topologicalClosure = { toSubmodule := Y.topologicalClosure, sup_mem' := ⋯ }

@[reducible]

noncomputable def VectorSublattice.banachLatticeSubtype {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (Y : VectorSublattice X) [CompleteSpace X] (hclosed : IsClosed ↑Y) : BanachLattice ↥Y.toSubmodule

A norm-closed vector sublattice of a Banach lattice is itself a Banach lattice under the induced structures.

Equations

• Y.banachLatticeSubtype hclosed = { toNormedVectorLattice := Y.instNormedVectorLatticeSubtype, toCompleteSpace := ⋯ }

theorem VectorSublattice.separableSpace_topologicalClosure_generated_of_countable {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {A : Set X} (hA : A.Countable) : TopologicalSpace.SeparableSpace ↥(generated A).topologicalClosure.toSubmodule

The closed vector sublattice generated by a countable subset of a normed vector lattice is separable.