Morphisms of vector lattices

This file defines VecLatHom, the type of vector lattice homomorphisms — maps that are simultaneously real-linear and lattice homomorphisms — together with the proposition-valued predicate IsVecLatHom characterising such maps. Key results include the characterisation of vector lattice homomorphisms by their behaviour on absolute values (VecLatHom.ofAbs) and the fact that every vector lattice homomorphism is monotone.

The second section develops VecLatEquiv, the type of vector lattice isomorphisms. It packages Positive.extensionEquiv, which extends an additive bijection between positive cones to a vector lattice isomorphism, and toContinuousLinearEquiv, which turns a vector lattice isomorphism between Banach lattices into a continuous linear equivalence.

The final section introduces BanachLatEquiv, the type of Banach lattice isometries: real linear isometric equivalences that also preserve ⊔ and ⊓.

Vector lattice homomorphisms

structure VecLatHom (X : Type u_1) (Y : Type u_2) [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] extends X →ₗ[ℝ] Y, LatticeHom X Y : Type (max u_1 u_2)

A vector lattice homomorphism from X to Y: a real-linear map that also preserves ⊔ and ⊓.

• toFun : X → Y
• map_add' (x y : X) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℝ) (x : X) : self.toFun (m • x) = (RingHom.id ℝ) m • self.toFun x
• map_sup' (a b : X) : self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
• map_inf' (a b : X) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b

structure IsVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X → Y) extends IsLinearMap ℝ f : Prop

Predicate form of VecLatHom: a map is a vector lattice homomorphism if it is linear and preserves ⊔ and ⊓.

• map_add (x y : X) : f (x + y) = f x + f y
• map_smul (c : ℝ) (x : X) : f (c • x) = c • f x
• map_sup' (x y : X) : f (x ⊔ y) = f x ⊔ f y
• map_inf' (x y : X) : f (x ⊓ y) = f x ⊓ f y

@[instance_reducible]

instance VecLatHom.instFunLike {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : FunLike (VecLatHom X Y) X Y

The canonical FunLike instance, making VecLatHom X Y a type of functions X → Y.

Equations

• VecLatHom.instFunLike = { coe := fun (f : VecLatHom X Y) => f.toFun, coe_injective := ⋯ }

theorem VecLatHom.isVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) : IsVecLatHom ⇑f

Every VecLatHom satisfies the IsVecLatHom predicate.

def VecLatHom.ofIsVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X → Y) (h : IsVecLatHom f) : VecLatHom X Y

Construct a VecLatHom from a proof that a function satisfies IsVecLatHom.

Equations

• VecLatHom.ofIsVecLatHom f h = { toFun := f, map_add' := ⋯, map_smul' := ⋯, map_sup' := ⋯, map_inf' := ⋯ }

instance VecLatHom.instLatticeHomClass {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : LatticeHomClass (VecLatHom X Y) X Y

VecLatHom X Y is a LatticeHomClass.

instance VecLatHom.instLinearMapClass {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : LinearMapClass (VecLatHom X Y) ℝ X Y

VecLatHom X Y is a LinearMapClass.

theorem VecLatHom.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : VecLatHom X Y} : f.toFun = ⇑f

The underlying function of a VecLatHom equals its coercion to X → Y.

theorem VecLatHom.map_abs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (x : X) : f |x| = |f x|

A vector lattice homomorphism preserves absolute values.

theorem VecLatHom.monotone {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) : Monotone ⇑f

Every vector lattice homomorphism is monotone.

theorem VecLatHom.map_nonneg {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) {x : X} (hx : 0 ≤ x) : 0 ≤ f x

A vector lattice homomorphism maps nonneg elements to nonneg elements.

theorem VecLatHom.le_of_map_le {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (hf : Function.Injective ⇑f) {a b : X} (hab : f a ≤ f b) : a ≤ b

An injective vector lattice homomorphism reflects the order: if f a ≤ f b then a ≤ b. Together with monotone, an injective vector lattice homomorphism is an order embedding.

theorem VecLatHom.map_posPart {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (x : X) : f x⁺ = (f x)⁺

A vector lattice homomorphism preserves positive parts: f x⁺ = (f x)⁺.

theorem VecLatHom.map_negPart {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (x : X) : f x⁻ = (f x)⁻

A vector lattice homomorphism preserves negative parts: f x⁻ = (f x)⁻.

theorem VecLatHom.map_disjoint {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) {x y : X} (h : x ⊓ y = 0) : f x ⊓ f y = 0

A vector lattice homomorphism preserves disjointness: x ⊓ y = 0 → f x ⊓ f y = 0.

def VecLatHom.id {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : VecLatHom X X

The identity vector lattice homomorphism.

Equations

• VecLatHom.id = { toLinearMap := LinearMap.id, map_sup' := ⋯, map_inf' := ⋯ }

def VecLatHom.ofAbs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X →ₗ[ℝ] Y) (abs : ∀ (x : X), f |x| = |f x|) : VecLatHom X Y

Construct a VecLatHom from a linear map that preserves absolute values.

Equations

• VecLatHom.ofAbs f abs = { toLinearMap := f, map_sup' := ⋯, map_inf' := ⋯ }

def VecLatHom.comp {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {Z : Type u_3} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z] (g : VecLatHom Y Z) (f : VecLatHom X Y) : VecLatHom X Z

Composition of two vector lattice homomorphisms.

Equations

• g.comp f = { toLinearMap := g.toLinearMap ∘ₗ f.toLinearMap, map_sup' := ⋯, map_inf' := ⋯ }

theorem VecLatHom.comp_apply {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {Z : Type u_3} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z] (g : VecLatHom Y Z) (f : VecLatHom X Y) (x : X) : (g.comp f) x = g (f x)

Evaluation of a composed VecLatHom.

noncomputable def VecLatHom.symm {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (h : Function.Bijective ⇑f) : VecLatHom Y X

The inverse of a bijective vector lattice homomorphism is again a vector lattice homomorphism.

Equations

• f.symm h = { toLinearMap := ↑(LinearEquiv.ofBijective f.toLinearMap h).symm, map_sup' := ⋯, map_inf' := ⋯ }

theorem VecLatHom.symm_apply {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : VecLatHom X Y) (h : Function.Bijective ⇑f) (x : X) (y : Y) : (f.symm h) y = x ↔ y = f x

The inverse bijection from symm: (f.symm h) y = x ↔ y = f x.

theorem LLexpr.map_eval {n : ℕ} {Y : Type u_3} {Z : Type u_4} [AddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice Y] [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z] (T : VecLatHom Y Z) (y : Fin n → Y) (e : LLexpr n) : T (eval y e) = eval (fun (i : Fin n) => T (y i)) e

A vector lattice homomorphism commutes with evaluation of lattice-linear expressions.

def IsVecLatHom.mk' {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X → Y) (vlh : IsVecLatHom f) : VecLatHom X Y

Bundle an IsVecLatHom proof into a VecLatHom.

Equations

• IsVecLatHom.mk' f vlh = VecLatHom.ofIsVecLatHom f vlh

@[simp]

theorem IsVecLatHom.mk'_apply {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X → Y} (vlh : IsVecLatHom f) (x : X) : (mk' f vlh) x = f x

Evaluation of mk' agrees with the underlying function.

theorem IsVecLatHom.of_abs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X → Y} (lin : IsLinearMap ℝ f) (abs : ∀ (x : X), f |x| = |f x|) : IsVecLatHom f

A linear map that preserves absolute values satisfies IsVecLatHom.

theorem IsVecLatHom.of_disjoint {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X → Y} (lin : IsLinearMap ℝ f) (disj : ∀ (x y : X), x ⊓ y = 0 → f x ⊓ f y = 0) : IsVecLatHom f

A linear map that preserves disjointness is a vector lattice homomorphism.

Vector lattice isomorphisms

structure VecLatEquiv (X : Type u_3) (Y : Type u_4) [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] extends X ≃ₗ[ℝ] Y, LatticeHom X Y : Type (max u_3 u_4)

A vector lattice isomorphism: a real-linear equivalence that also preserves ⊔ and ⊓.

• toFun : X → Y
• map_add' (x y : X) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' (m : ℝ) (x : X) : (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id ℝ) m • (↑self.toLinearEquiv).toFun x
• invFun : Y → X
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• map_sup' (a b : X) : (↑self.toLinearEquiv).toFun (a ⊔ b) = (↑self.toLinearEquiv).toFun a ⊔ (↑self.toLinearEquiv).toFun b
• map_inf' (a b : X) : (↑self.toLinearEquiv).toFun (a ⊓ b) = (↑self.toLinearEquiv).toFun a ⊓ (↑self.toLinearEquiv).toFun b

@[instance_reducible]

instance VecLatEquiv.instFunLike {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : FunLike (VecLatEquiv X Y) X Y

The canonical FunLike instance, making VecLatEquiv X Y a type of functions X → Y.

Equations

• VecLatEquiv.instFunLike = { coe := fun (e : VecLatEquiv X Y) => (↑e.toLinearEquiv).toFun, coe_injective := ⋯ }

def VecLatEquiv.toVecLatHom {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (e : VecLatEquiv X Y) : VecLatHom X Y

Coerce a VecLatEquiv to a VecLatHom.

Equations

• e.toVecLatHom = { toLinearMap := ↑e.toLinearEquiv, map_sup' := ⋯, map_inf' := ⋯ }

def VecLatEquiv.refl {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : VecLatEquiv X X

The identity vector lattice isomorphism.

Equations

• VecLatEquiv.refl = { toLinearEquiv := LinearEquiv.refl ℝ X, map_sup' := ⋯, map_inf' := ⋯ }

def VecLatEquiv.symm {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (e : VecLatEquiv X Y) : VecLatEquiv Y X

The inverse of a vector lattice isomorphism.

Equations

• e.symm = { toLinearEquiv := e.symm, map_sup' := ⋯, map_inf' := ⋯ }

def VecLatEquiv.trans {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {Z : Type u_3} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z] (e₁ : VecLatEquiv X Y) (e₂ : VecLatEquiv Y Z) : VecLatEquiv X Z

Composition of vector lattice isomorphisms.

Equations

• e₁.trans e₂ = { toLinearEquiv := e₁.toLinearEquiv ≪≫ₗ e₂.toLinearEquiv, map_sup' := ⋯, map_inf' := ⋯ }

Extension from the positive cone

noncomputable def Positive.extensionEquiv {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] {τ : X → Y} (hτ_nn : ∀ (x : X), 0 ≤ x → 0 ≤ τ x) (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) (hτ_inj : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ x = τ y → x = y) (hτ_surj : ∀ (y : Y), 0 ≤ y → ∃ (x : X), 0 ≤ x ∧ τ x = y) : VecLatEquiv X Y

An additive bijection between positive cones extends to a vector lattice isomorphism when the codomain is Archimedean.

Equations

• Positive.extensionEquiv hτ_nn hτ_add hτ_inj hτ_surj = { toLinearEquiv := LinearEquiv.ofBijective (Positive.extension hτ_nn hτ_add) ⋯, map_sup' := ⋯, map_inf' := ⋯ }

Continuous linear equivalence between Banach lattices

noncomputable def VecLatEquiv.toContinuousLinearEquiv {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] (e : VecLatEquiv X Y) : X ≃L[ℝ] Y

A vector lattice isomorphism between Banach lattices extends to a continuous linear equivalence.

Equations

• e.toContinuousLinearEquiv = { toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Banach lattice isometries

structure BanachLatEquiv (X : Type u_3) (Y : Type u_4) [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] extends X ≃ₗᵢ[ℝ] Y, LatticeHom X Y : Type (max u_3 u_4)

A Banach lattice isometry between two Banach lattices: a real linear isometric equivalence that also preserves the lattice operations ⊔ and ⊓. Such a map is automatically an order isomorphism.

• toFun : X → Y
• map_add' (x y : X) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' (m : ℝ) (x : X) : (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id ℝ) m • (↑self.toLinearEquiv).toFun x
• invFun : Y → X
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• norm_map' (x : X) : ‖self.toLinearEquiv x‖ = ‖x‖
• map_sup' (a b : X) : (↑self.toLinearEquiv).toFun (a ⊔ b) = (↑self.toLinearEquiv).toFun a ⊔ (↑self.toLinearEquiv).toFun b
• map_inf' (a b : X) : (↑self.toLinearEquiv).toFun (a ⊓ b) = (↑self.toLinearEquiv).toFun a ⊓ (↑self.toLinearEquiv).toFun b

@[instance_reducible]

instance BanachLatEquiv.instFunLike {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] : FunLike (BanachLatEquiv X Y) X Y

The canonical FunLike instance, making BanachLatEquiv X Y a type of functions X → Y.

Equations

• BanachLatEquiv.instFunLike = { coe := fun (e : BanachLatEquiv X Y) => (↑e.toLinearEquiv).toFun, coe_injective := ⋯ }

noncomputable def BanachLatEquiv.toContinuousLinearEquiv {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] (e : BanachLatEquiv X Y) : X ≃L[ℝ] Y

Coerce a BanachLatEquiv to a continuous linear equivalence.

Equations

• e.toContinuousLinearEquiv = ↑e.toLinearIsometryEquiv

def BanachLatEquiv.toVecLatEquiv {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] (e : BanachLatEquiv X Y) : VecLatEquiv X Y

Coerce a BanachLatEquiv to a VecLatEquiv.

Equations

• e.toVecLatEquiv = { toLinearEquiv := e.toLinearEquiv, map_sup' := ⋯, map_inf' := ⋯ }

def BanachLatEquiv.symm {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] (e : BanachLatEquiv X Y) : BanachLatEquiv Y X

The inverse of a Banach lattice isometry.

Equations

• e.symm = { toLinearIsometryEquiv := e.symm, map_sup' := ⋯, map_inf' := ⋯ }

def BanachLatEquiv.refl (X : Type u_5) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] : BanachLatEquiv X X

The identity Banach lattice isometry.

Equations

• BanachLatEquiv.refl X = { toLinearIsometryEquiv := LinearIsometryEquiv.refl ℝ X, map_sup' := ⋯, map_inf' := ⋯ }

def BanachLatEquiv.trans {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [BanachLattice Y] {Z : Type u_5} [NormedAddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [BanachLattice Z] (e₁ : BanachLatEquiv X Y) (e₂ : BanachLatEquiv Y Z) : BanachLatEquiv X Z

The composition of two Banach lattice isometries.

Equations

• e₁.trans e₂ = { toLinearIsometryEquiv := e₁.trans e₂.toLinearIsometryEquiv, map_sup' := ⋯, map_inf' := ⋯ }

Inclusion into the completion

noncomputable def toCompletionVecLatHom {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : VecLatHom X (UniformSpace.Completion X)

The canonical inclusion of a normed vector lattice into its completion, as a vector lattice homomorphism.

Equations

• toCompletionVecLatHom = { toFun := UniformSpace.Completion.coe', map_add' := ⋯, map_smul' := ⋯, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem coe_toCompletionVecLatHom {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : ⇑toCompletionVecLatHom = UniformSpace.Completion.coe'

theorem isometry_toCompletionVecLatHom {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : Isometry ⇑toCompletionVecLatHom

The canonical inclusion of a normed vector lattice into its completion is an isometry; together with toCompletionVecLatHom this exhibits the inclusion as a lattice isometry.

noncomputable def banachLatEquivCompletionOfDenseIsometry {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {Y : Type u_4} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [BanachLattice Y] (T : VecLatHom X Y) (hT_norm : ∀ (x : X), ‖T x‖ = ‖x‖) (hT_dense : DenseRange ⇑T) : BanachLatEquiv (UniformSpace.Completion X) Y

A norm-preserving vector lattice homomorphism T : X → Y with dense range into a Banach lattice Y extends to a Banach lattice isometry from the completion of X onto Y.

Equations

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