BanLat/Operators/Hom.lean
All source files · Download exact source
SHA-256: 1a38127619695e2862fb93408bc24272d19a02f72a09783daf32e81b922e2595
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Operators.Positive6import BanLat.Substructures.Sublattice7import BanLat.LLexpr8import Mathlib.Analysis.Normed.Operator.LinearIsometry910/-!11# Morphisms of vector lattices1213This file defines `VecLatHom`, the type of vector lattice homomorphisms — maps that are14simultaneously real-linear and lattice homomorphisms — together with the15proposition-valued predicate `IsVecLatHom` characterising such maps. Key results include16the characterisation of vector lattice homomorphisms by their behaviour on absolute17values (`VecLatHom.ofAbs`) and the fact that every vector lattice homomorphism is monotone.1819The second section develops `VecLatEquiv`, the type of vector lattice isomorphisms. It20packages `Positive.extensionEquiv`, which extends an additive bijection between positive21cones to a vector lattice isomorphism, and `toContinuousLinearEquiv`, which turns a22vector lattice isomorphism between Banach lattices into a continuous linear equivalence.2324The final section introduces `BanachLatEquiv`, the type of Banach lattice isometries:25real linear isometric equivalences that also preserve `⊔` and `⊓`.26-/2728/-! ## Vector lattice homomorphisms -/2930/-- A vector lattice homomorphism from `X` to `Y`: a real-linear map that also preserves31`⊔` and `⊓`. -/32structure VecLatHom (X : Type*) (Y : Type*) [AddCommGroup X] [AddCommGroup Y]33 [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]34 [VectorLattice X] [VectorLattice Y] extends X →ₗ[ℝ] Y, LatticeHom X Y3536attribute [inherit_doc LatticeHom] VecLatHom.toLatticeHom3738variable {X : Type*} {Y : Type*} [AddCommGroup X] [AddCommGroup Y]39 [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]40 [VectorLattice X] [VectorLattice Y]4142/-- Predicate form of `VecLatHom`: a map is a vector lattice homomorphism if it is linear43and preserves `⊔` and `⊓`. -/44structure IsVecLatHom (f : X → Y) extends IsLinearMap ℝ f where45 map_sup' : ∀ x y : X, f (x ⊔ y) = (f x) ⊔ (f y)46 map_inf' : ∀ x y : X, f (x ⊓ y) = (f x) ⊓ (f y)4748namespace VecLatHom4950/-- The canonical `FunLike` instance, making `VecLatHom X Y` a type of functions `X → Y`. -/51instance instFunLike : FunLike (VecLatHom X Y) X Y where52 coe f := f.toFun53 coe_injective f g h := by54 dsimp at h55 cases f56 cases g57 congr58 exact LinearMap.ext_iff.mpr (congrFun h)5960/-- Every `VecLatHom` satisfies the `IsVecLatHom` predicate. -/61theorem isVecLatHom (f : VecLatHom X Y) : IsVecLatHom f where62 map_add := f.toLinearMap.map_add63 map_smul := f.toLinearMap.map_smul64 map_sup' := f.toLatticeHom.map_sup'65 map_inf' := f.toLatticeHom.map_inf'6667/-- Construct a `VecLatHom` from a proof that a function satisfies `IsVecLatHom`. -/68def ofIsVecLatHom (f : X → Y) (h : IsVecLatHom f) : VecLatHom X Y where69 toFun := f70 map_add' := h.map_add71 map_smul' := h.map_smul72 map_sup' := h.map_sup'73 map_inf' := h.map_inf'7475/-- `VecLatHom X Y` is a `LatticeHomClass`. -/76instance instLatticeHomClass : LatticeHomClass (VecLatHom X Y) X Y where77 map_inf := by78 intro f a b79 exact f.toLatticeHom.map_inf' a b80 map_sup := by81 intro f a b82 exact f.toLatticeHom.map_sup' a b8384/-- `VecLatHom X Y` is a `LinearMapClass`. -/85instance instLinearMapClass : LinearMapClass (VecLatHom X Y) ℝ X Y where86 map_add := by87 intro f a b88 exact f.toLinearMap.map_add a b89 map_smulₛₗ := by90 intro f c x91 simp only [RingHom.id_apply]92 exact f.toLinearMap.map_smul c x9394/-- The underlying function of a `VecLatHom` equals its coercion to `X → Y`. -/95theorem toFun_eq_coe {f : VecLatHom X Y} : f.toFun = (f : X → Y) := rfl9697/-- A vector lattice homomorphism preserves absolute values. -/98theorem map_abs (f : VecLatHom X Y) (x : X) : f |x| = |f x| := by99 rw [abs, abs, map_sup, map_neg]100101/-- Every vector lattice homomorphism is monotone. -/102theorem monotone (f : VecLatHom X Y) : Monotone f := by103 intro x y hxy104 have : x ⊔ y = y := by simp [hxy]105 rw [← sup_eq_right, ← map_sup f x y, this]106107/-- A vector lattice homomorphism maps nonneg elements to nonneg elements. -/108theorem map_nonneg (f : VecLatHom X Y) {x : X} (hx : 0 ≤ x) : 0 ≤ f x := by109 have h := f.monotone hx; rwa [map_zero] at h110111/-- An injective vector lattice homomorphism reflects the order: if `f a ≤ f b` then112`a ≤ b`. Together with `monotone`, an injective vector lattice homomorphism is an order113embedding. -/114theorem le_of_map_le (f : VecLatHom X Y) (hf : Function.Injective f) {a b : X}115 (hab : f a ≤ f b) : a ≤ b :=116 sup_eq_right.mp (hf (by rw [map_sup f a b]; exact sup_eq_right.mpr hab))117118/-- A vector lattice homomorphism preserves positive parts: `f x⁺ = (f x)⁺`. -/119theorem map_posPart (f : VecLatHom X Y) (x : X) : f x⁺ = (f x)⁺ := by120 rw [posPart_def, map_sup, map_zero, posPart_def]121122/-- A vector lattice homomorphism preserves negative parts: `f x⁻ = (f x)⁻`. -/123theorem map_negPart (f : VecLatHom X Y) (x : X) : f x⁻ = (f x)⁻ := by124 rw [negPart_def, map_sup, map_neg, map_zero, negPart_def]125126/-- A vector lattice homomorphism preserves disjointness: `x ⊓ y = 0 → f x ⊓ f y = 0`. -/127theorem map_disjoint (f : VecLatHom X Y) {x y : X} (h : x ⊓ y = 0) : f x ⊓ f y = 0 := by128 rw [← map_inf, h, map_zero]129130/-- The identity vector lattice homomorphism. -/131def id : VecLatHom X X :=132 { LinearMap.id with133 map_sup' := fun _ _ => rfl134 map_inf' := fun _ _ => rfl }135136/-- Construct a `VecLatHom` from a linear map that preserves absolute values. -/137def ofAbs (f : X →ₗ[ℝ] Y) (abs : ∀ x : X, f |x| = |f x|) : VecLatHom X Y :=138 { f with139 map_sup' := fun a b => by140 change f (a ⊔ b) = f a ⊔ f b141 rw [sup_eq_half_smul_add_add_abs_sub' ℝ, map_smul, map_add, map_add,142 abs (b - a), map_sub, ← sup_eq_half_smul_add_add_abs_sub' ℝ]143 map_inf' := fun a b => by144 change f (a ⊓ b) = f a ⊓ f b145 rw [inf_eq_half_smul_add_sub_abs_sub' ℝ, map_smul, map_sub, map_add,146 abs (b - a), map_sub, ← inf_eq_half_smul_add_sub_abs_sub' ℝ] }147148/-- Composition of two vector lattice homomorphisms. -/149def comp {Z : Type*} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z]150 [VectorLattice Z] (g : VecLatHom Y Z) (f : VecLatHom X Y) :151 VecLatHom X Z :=152 {LinearMap.comp g.toLinearMap f.toLinearMap with153 map_sup' := by154 intro x y155 simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp,156 Function.comp_apply]157 change g ( f (x ⊔ y) ) = (g (f x)) ⊔ (g (f y))158 simp only [map_sup]159 map_inf' := by160 intro x y161 simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp,162 Function.comp_apply]163 change g ( f (x ⊓ y) ) = (g (f x)) ⊓ (g (f y))164 simp only [map_inf]165 }166167/-- Evaluation of a composed `VecLatHom`. -/168theorem comp_apply {Z : Type*} [AddCommGroup Z] [Lattice Z]169 [IsOrderedAddMonoid Z] [VectorLattice Z] (g : VecLatHom Y Z)170 (f : VecLatHom X Y) (x : X) : g.comp f x = g (f x) := by171 rw [comp]172 change (LinearMap.comp g.toLinearMap f.toLinearMap) x = g (f x)173 simp174 rfl175176/-- The inverse of a bijective vector lattice homomorphism is again a vector lattice177homomorphism. -/178noncomputable def symm (f : VecLatHom X Y) (h : Function.Bijective f) : VecLatHom Y X :=179 {(LinearEquiv.ofBijective f.toLinearMap h).symm with180 map_sup' := by181 intro a b182 change183 (LinearEquiv.ofBijective f.toLinearMap h).symm (a ⊔ b) =184 (LinearEquiv.ofBijective f.toLinearMap h).symm a ⊔185 (LinearEquiv.ofBijective f.toLinearMap h).symm b186 rw [LinearEquiv.symm_apply_eq]187 change188 a ⊔ b = f ( (LinearEquiv.ofBijective f.toLinearMap h).symm a ⊔189 (LinearEquiv.ofBijective f.toLinearMap h).symm b)190 rw [map_sup]191 change192 a ⊔ b = LinearEquiv.ofBijective f.toLinearMap h193 ((LinearEquiv.ofBijective f.toLinearMap h).symm a) ⊔194 LinearEquiv.ofBijective f.toLinearMap h195 ((LinearEquiv.ofBijective f.toLinearMap h).symm b)196 rw [LinearEquiv.apply_symm_apply, LinearEquiv.apply_symm_apply]197 map_inf' := by198 intro a b199 change200 (LinearEquiv.ofBijective f.toLinearMap h).symm (a ⊓ b) =201 (LinearEquiv.ofBijective f.toLinearMap h).symm a ⊓202 (LinearEquiv.ofBijective f.toLinearMap h).symm b203 rw [LinearEquiv.symm_apply_eq]204 change205 a ⊓ b = f ( (LinearEquiv.ofBijective f.toLinearMap h).symm a ⊓206 (LinearEquiv.ofBijective f.toLinearMap h).symm b)207 rw [map_inf]208 change209 a ⊓ b = LinearEquiv.ofBijective f.toLinearMap h210 ((LinearEquiv.ofBijective f.toLinearMap h).symm a) ⊓211 LinearEquiv.ofBijective f.toLinearMap h212 ((LinearEquiv.ofBijective f.toLinearMap h).symm b)213 rw [LinearEquiv.apply_symm_apply, LinearEquiv.apply_symm_apply]214 }215216/-- The inverse bijection from `symm`: `(f.symm h) y = x ↔ y = f x`. -/217theorem symm_apply (f : VecLatHom X Y) (h : Function.Bijective f)218 (x : X) (y : Y) : (f.symm h) y = x ↔ y = f x := by219 let lineq := LinearEquiv.ofBijective f.toLinearMap h220 change lineq.symm y = x ↔ y = f x221 apply LinearEquiv.symm_apply_eq222223end VecLatHom224225namespace LLexpr226227variable {n : ℕ}228229/-- A vector lattice homomorphism commutes with evaluation of lattice-linear expressions. -/230theorem map_eval {Y Z : Type*}231 [AddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice Y]232 [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z]233 (T : VecLatHom Y Z) (y : Fin n → Y) (e : LLexpr n) :234 T (eval y e) = eval (fun i => T (y i)) e := by235 induction e with236 | zero => simp [eval]237 | var i => simp [eval]238 | add e₁ e₂ h₁ h₂ => simp [eval, h₁, h₂]239 | smul r e h => simp [eval, h]240 | sup e₁ e₂ h₁ h₂ => simp [eval, h₁, h₂, map_sup]241 | inf e₁ e₂ h₁ h₂ => simp [eval, h₁, h₂, map_inf]242243end LLexpr244245namespace IsVecLatHom246247/-- Bundle an `IsVecLatHom` proof into a `VecLatHom`. -/248def mk' (f : X → Y) (vlh : IsVecLatHom f) : VecLatHom X Y where249 toFun := f250 map_add' := vlh.map_add251 map_smul' := vlh.map_smul252 map_sup' := vlh.map_sup'253 map_inf' := vlh.map_inf'254255/-- Evaluation of `mk'` agrees with the underlying function. -/256@[simp]257theorem mk'_apply {f : X → Y} (vlh : IsVecLatHom f) (x : X) :258 mk' f vlh x = f x := rfl259260/-- A linear map that preserves absolute values satisfies `IsVecLatHom`. -/261theorem of_abs {f : X → Y} (lin : IsLinearMap ℝ f) (abs : ∀ x : X, f |x|262 = |f x|) : IsVecLatHom f :=263 VecLatHom.isVecLatHom (VecLatHom.ofAbs (IsLinearMap.mk' f lin) abs)264265/-- A positive linear map that preserves disjointness is a vector lattice homomorphism. -/266theorem of_disjoint {f : X → Y} (lin : IsLinearMap ℝ f)267 (_pos : ∀ x : X, 0 ≤ x → 0 ≤ f x)268 (disj : ∀ x y : X, x ⊓ y = 0 → f x ⊓ f y = 0) : IsVecLatHom f := by269 have fNeg : ∀ x : X, f (-x) = -f x := fun x => by270 have h := lin.map_smul (-1 : ℝ) x; rwa [neg_one_smul, neg_one_smul] at h271 have fSub : ∀ x y : X, f (x - y) = f x - f y := fun x y => by272 rw [sub_eq_add_neg, lin.map_add, fNeg, ← sub_eq_add_neg]273 have fPosPart : ∀ c : X, f c⁺ = (f c)⁺ := fun c =>274 uniqueness_posPart (f c) (by rw [← fSub, posPart_sub_negPart])275 (disj c⁺ c⁻ (posPart_inf_negPart_eq_zero c))276 have fSup : ∀ a b : X, f (a ⊔ b) = f a ⊔ f b := fun a b => by277 rw [sup_eq_add_posPart_sub, lin.map_add, fPosPart, fSub, ← sup_eq_add_posPart_sub]278 exact { lin with279 map_sup' := fSup280 map_inf' := fun a b => by281 have h := fSup (-a) (-b)282 rw [← neg_inf] at h283 rw [fNeg, fNeg a, fNeg b, ← neg_inf] at h284 exact neg_inj.mp h }285286end IsVecLatHom287288/-! ## Vector lattice isomorphisms -/289290/-- A vector lattice isomorphism: a real-linear equivalence that also preserves `⊔` and `⊓`. -/291structure VecLatEquiv (X : Type*) (Y : Type*) [AddCommGroup X] [AddCommGroup Y]292 [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]293 [VectorLattice X] [VectorLattice Y] extends X ≃ₗ[ℝ] Y, LatticeHom X Y294295attribute [inherit_doc LatticeHom] VecLatEquiv.toLatticeHom296297namespace VecLatEquiv298299/-- The canonical `FunLike` instance, making `VecLatEquiv X Y` a type of functions `X → Y`. -/300instance instFunLike : FunLike (VecLatEquiv X Y) X Y where301 coe e := e.toFun302 coe_injective := by303 intro f g h304 cases f; cases g305 congr 1306 exact LinearEquiv.ext (congrFun h)307308/-- Coerce a `VecLatEquiv` to a `VecLatHom`. -/309def toVecLatHom (e : VecLatEquiv X Y) : VecLatHom X Y :=310 { e.toLinearMap with311 map_sup' := e.map_sup'312 map_inf' := e.map_inf' }313314/-- The identity vector lattice isomorphism. -/315def refl : VecLatEquiv X X :=316 { LinearEquiv.refl ℝ X with317 map_sup' := fun _ _ => rfl318 map_inf' := fun _ _ => rfl }319320/-- The inverse of a vector lattice isomorphism. -/321def symm (e : VecLatEquiv X Y) : VecLatEquiv Y X :=322 { e.toLinearEquiv.symm with323 map_sup' := fun a b => by324 have h := e.map_sup' (e.toLinearEquiv.symm a) (e.toLinearEquiv.symm b)325 simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,326 LinearEquiv.apply_symm_apply] at h327 change e.toLinearEquiv.symm (a ⊔ b) = e.toLinearEquiv.symm a ⊔ e.toLinearEquiv.symm b328 exact e.toLinearEquiv.injective (by rw [LinearEquiv.apply_symm_apply]; exact h.symm)329 map_inf' := fun a b => by330 have h := e.map_inf' (e.toLinearEquiv.symm a) (e.toLinearEquiv.symm b)331 simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,332 LinearEquiv.apply_symm_apply] at h333 change e.toLinearEquiv.symm (a ⊓ b) = e.toLinearEquiv.symm a ⊓ e.toLinearEquiv.symm b334 exact e.toLinearEquiv.injective (by rw [LinearEquiv.apply_symm_apply]; exact h.symm) }335336/-- Composition of vector lattice isomorphisms. -/337def trans {Z : Type*} [AddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z] [VectorLattice Z]338 (e₁ : VecLatEquiv X Y) (e₂ : VecLatEquiv Y Z) : VecLatEquiv X Z :=339 { e₁.toLinearEquiv.trans e₂.toLinearEquiv with340 map_sup' := fun a b => by341 change e₂.toFun (e₁.toFun (a ⊔ b)) = e₂.toFun (e₁.toFun a) ⊔ e₂.toFun (e₁.toFun b)342 rw [e₁.map_sup', e₂.map_sup']343 map_inf' := fun a b => by344 change e₂.toFun (e₁.toFun (a ⊓ b)) = e₂.toFun (e₁.toFun a) ⊓ e₂.toFun (e₁.toFun b)345 rw [e₁.map_inf', e₂.map_inf'] }346347end VecLatEquiv348349/-! ### Extension from the positive cone -/350351namespace Positive352353variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y]354 [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]355 [IsVLArchimedean Y] {τ : X → Y}356 (hτ_nn : ∀ x, 0 ≤ x → 0 ≤ τ x)357 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)358359/-- An additive bijection between positive cones extends to a vector lattice360isomorphism when the codomain is Archimedean. -/361noncomputable def extensionEquiv362 (hτ_inj : ∀ x y, 0 ≤ x → 0 ≤ y → τ x = τ y → x = y)363 (hτ_surj : ∀ y, 0 ≤ y → ∃ x, 0 ≤ x ∧ τ x = y) :364 VecLatEquiv X Y := by365 set T := extension hτ_nn hτ_add366 have hT_inj : Function.Injective T := by367 intro a b hab368 have h : T (a - b) = 0 := by369 rw [map_sub]; exact sub_eq_zero.mpr hab370 rw [extension_apply] at h371 have heq : (a - b)⁺ = (a - b)⁻ :=372 hτ_inj _ _ (posPart_nonneg _) (negPart_nonneg _) (sub_eq_zero.mp h)373 have hsub := posPart_sub_negPart (a - b)374 rw [heq, sub_self] at hsub375 exact sub_eq_zero.mp hsub.symm376 have hT_surj : Function.Surjective T := by377 intro y378 obtain ⟨a, ha, haτ⟩ := hτ_surj y⁺ (posPart_nonneg y)379 obtain ⟨b, hb, hbτ⟩ := hτ_surj y⁻ (negPart_nonneg y)380 exact ⟨a - b, by381 rw [map_sub, extension_nonneg hτ_nn hτ_add ha,382 extension_nonneg hτ_nn hτ_add hb, haτ, hbτ,383 posPart_sub_negPart]⟩384 -- T is order-reflecting: 0 ≤ Tx → 0 ≤ x385 have hT_bipos : ∀ x, 0 ≤ T x → 0 ≤ x := by386 intro x hTx387 rw [extension_apply] at hTx388 have hτle : τ x⁻ ≤ τ x⁺ := sub_nonneg.mp hTx389 obtain ⟨c, hc, hcτ⟩ := hτ_surj _ hTx390 have hsum : τ (x⁻ + c) = τ x⁺ := by391 rw [hτ_add _ _ (negPart_nonneg _) hc, hcτ, add_sub_cancel]392 have heq : x⁻ + c = x⁺ :=393 hτ_inj _ _ (add_nonneg (negPart_nonneg _) hc) (posPart_nonneg _) hsum394 have hle : x⁻ ≤ x⁺ := heq ▸ le_add_of_nonneg_right hc395 have : x⁻ = 0 := (inf_eq_left.mpr hle).symm.trans396 ((inf_comm x⁻ x⁺).trans (posPart_inf_negPart_eq_zero x))397 rw [← posPart_sub_negPart x, this, sub_zero]398 exact posPart_nonneg _399 -- T⁻¹ is monotone (from bipositivity + positivity)400 have hT_inv_mono : ∀ a b, T a ≤ T b → a ≤ b := by401 intro a b hab402 have : 0 ≤ T (b - a) := by rw [map_sub]; exact sub_nonneg.mpr hab403 exact sub_nonneg.mp (hT_bipos _ this)404 have hT_mono : Monotone T := monotone_iff.mpr (extension_positive hτ_nn hτ_add)405 -- T preserves ⊔406 have hT_sup : ∀ a b, T (a ⊔ b) = T a ⊔ T b := by407 intro a b408 apply le_antisymm409 · obtain ⟨c, hc⟩ := hT_surj (T a ⊔ T b)410 have hca : a ≤ c := hT_inv_mono _ _ (hc ▸ le_sup_left)411 have hcb : b ≤ c := hT_inv_mono _ _ (hc ▸ le_sup_right)412 rw [← hc]; exact hT_mono (sup_le hca hcb)413 · exact sup_le (hT_mono le_sup_left) (hT_mono le_sup_right)414 -- T preserves ⊓415 have hT_inf : ∀ a b, T (a ⊓ b) = T a ⊓ T b := by416 intro a b417 apply le_antisymm418 · exact le_inf (hT_mono inf_le_left) (hT_mono inf_le_right)419 · obtain ⟨c, hc⟩ := hT_surj (T a ⊓ T b)420 have hca : c ≤ a := hT_inv_mono _ _ (hc ▸ inf_le_left)421 have hcb : c ≤ b := hT_inv_mono _ _ (hc ▸ inf_le_right)422 rw [← hc]; exact hT_mono (le_inf hca hcb)423 exact424 { (LinearEquiv.ofBijective T ⟨hT_inj, hT_surj⟩) with425 map_sup' := hT_sup426 map_inf' := hT_inf }427428end Positive429430/-! ### Continuous linear equivalence between Banach lattices -/431432namespace VecLatEquiv433434variable {X Y : Type*} [NormedAddCommGroup X] [NormedAddCommGroup Y]435 [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]436 [BanachLattice X] [BanachLattice Y]437438/-- A vector lattice isomorphism between Banach lattices extends to a continuous linear439equivalence. -/440noncomputable def toContinuousLinearEquiv (e : VecLatEquiv X Y) : X ≃L[ℝ] Y :=441 ContinuousLinearEquiv.mk e.toLinearEquiv442 (Positive.continuous (Positive.monotone_iff.mp e.toVecLatHom.monotone))443 (Positive.continuous (Positive.monotone_iff.mp e.symm.toVecLatHom.monotone))444445end VecLatEquiv446447/-- A Banach lattice contains a lattice copy of another Banach lattice if it has a448closed vector sublattice that is vector-lattice isomorphic to it. -/449def ContainsLatticeCopy (X Y : Type*)450 [NormedAddCommGroup X] [NormedAddCommGroup Y]451 [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]452 [BanachLattice X] [BanachLattice Y] : Prop :=453 ∃ Z : VectorSublattice X,454 IsClosed (Z : Set X) ∧ Nonempty (VecLatEquiv Y ↥Z.toSubmodule)455456/-! ## Banach lattice isometries -/457458/-- A **Banach lattice isometry** between two Banach lattices: a real linear459isometric equivalence that also preserves the lattice operations `⊔` and `⊓`.460Such a map is automatically an order isomorphism. -/461structure BanachLatEquiv (X Y : Type*)462 [NormedAddCommGroup X] [NormedAddCommGroup Y]463 [Lattice X] [Lattice Y]464 [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]465 [BanachLattice X] [BanachLattice Y]466 extends X ≃ₗᵢ[ℝ] Y, LatticeHom X Y467468attribute [inherit_doc LatticeHom] BanachLatEquiv.toLatticeHom469470namespace BanachLatEquiv471472variable {X Y : Type*}473 [NormedAddCommGroup X] [NormedAddCommGroup Y]474 [Lattice X] [Lattice Y]475 [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]476 [BanachLattice X] [BanachLattice Y]477478/-- The canonical `FunLike` instance, making `BanachLatEquiv X Y` a type of479functions `X → Y`. -/480instance instFunLike : FunLike (BanachLatEquiv X Y) X Y where481 coe e := e.toFun482 coe_injective := by483 intro f g h484 cases f; cases g485 congr 1486 exact LinearIsometryEquiv.toLinearEquiv_injective487 (LinearEquiv.toEquiv_injective (Equiv.coe_inj.mp h))488489/-- Coerce a `BanachLatEquiv` to a continuous linear equivalence. -/490noncomputable def toContinuousLinearEquiv (e : BanachLatEquiv X Y) : X ≃L[ℝ] Y :=491 e.toLinearIsometryEquiv.toContinuousLinearEquiv492493/-- Coerce a `BanachLatEquiv` to a `VecLatEquiv`. -/494def toVecLatEquiv (e : BanachLatEquiv X Y) : VecLatEquiv X Y :=495 { e.toLinearIsometryEquiv.toLinearEquiv with496 map_sup' := e.map_sup'497 map_inf' := e.map_inf' }498499/-- The inverse of a Banach lattice isometry. -/500def symm (e : BanachLatEquiv X Y) : BanachLatEquiv Y X where501 toLinearIsometryEquiv := e.toLinearIsometryEquiv.symm502 map_sup' := e.toVecLatEquiv.symm.map_sup'503 map_inf' := e.toVecLatEquiv.symm.map_inf'504505/-- The identity Banach lattice isometry. -/506def refl (X : Type*) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]507 [BanachLattice X] : BanachLatEquiv X X where508 toLinearIsometryEquiv := LinearIsometryEquiv.refl ℝ X509 map_sup' := fun _ _ => rfl510 map_inf' := fun _ _ => rfl511512/-- The composition of two Banach lattice isometries. -/513def trans {Z : Type*} [NormedAddCommGroup Z] [Lattice Z] [IsOrderedAddMonoid Z]514 [BanachLattice Z] (e₁ : BanachLatEquiv X Y) (e₂ : BanachLatEquiv Y Z) :515 BanachLatEquiv X Z where516 toLinearIsometryEquiv := e₁.toLinearIsometryEquiv.trans e₂.toLinearIsometryEquiv517 map_sup' := (e₁.toVecLatEquiv.trans e₂.toVecLatEquiv).map_sup'518 map_inf' := (e₁.toVecLatEquiv.trans e₂.toVecLatEquiv).map_inf'519520end BanachLatEquiv521522/-! ## Inclusion into the completion -/523524section Completion525526open UniformSpace527528variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]529 [NormedVectorLattice X]530531/-- The canonical inclusion of a normed vector lattice into its completion, as a vector532lattice homomorphism. -/533noncomputable def toCompletionVecLatHom : VecLatHom X (Completion X) where534 toFun := ((↑) : X → Completion X)535 map_add' := Completion.coe_add536 map_smul' := Completion.coe_smul537 map_sup' := coe_sup_completion538 map_inf' := coe_inf_completion539540@[simp]541theorem coe_toCompletionVecLatHom :542 ⇑(toCompletionVecLatHom : VecLatHom X (Completion X)) = ((↑) : X → Completion X) :=543 rfl544545/-- The canonical inclusion of a normed vector lattice into its completion is an isometry;546together with `toCompletionVecLatHom` this exhibits the inclusion as a lattice isometry. -/547theorem isometry_toCompletionVecLatHom :548 Isometry (toCompletionVecLatHom : X → Completion X) := by549 rw [coe_toCompletionVecLatHom]550 exact isometry_coe_completion551552/-- A norm-preserving vector lattice homomorphism `T : X → Y` with dense range into a Banach553lattice `Y` extends to a Banach lattice isometry from the completion of `X` onto `Y`. -/554noncomputable def banachLatEquivCompletionOfDenseIsometry555 {Y : Type*} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [BanachLattice Y]556 (T : VecLatHom X Y) (hT_norm : ∀ x, ‖T x‖ = ‖x‖) (hT_dense : DenseRange ⇑T) :557 BanachLatEquiv (Completion X) Y := by558 let Tli : X →ₗᵢ[ℝ] Y := { toLinearMap := T.toLinearMap, norm_map' := hT_norm }559 have huc : UniformContinuous ⇑Tli := Tli.isometry.uniformContinuous560 let Tc : Completion X →ₗᵢ[ℝ] Y :=561 { toFun := Completion.extension Tli562 map_add' := fun z w => by563 refine Completion.induction_on₂ z w (isClosed_eq ?_ ?_) (fun x y => ?_)564 · exact Completion.continuous_extension.comp continuous_add565 · exact (Completion.continuous_extension.comp continuous_fst).add566 (Completion.continuous_extension.comp continuous_snd)567 · rw [← Completion.coe_add, Completion.extension_coe huc, Completion.extension_coe huc,568 Completion.extension_coe huc, map_add]569 map_smul' := fun r z => by570 refine Completion.induction_on z (isClosed_eq ?_ ?_) (fun x => ?_)571 · exact Completion.continuous_extension.comp (continuous_const_smul r)572 · exact (continuous_const_smul r).comp Completion.continuous_extension573 · rw [← Completion.coe_smul, Completion.extension_coe huc, Completion.extension_coe huc,574 map_smul, RingHom.id_apply]575 norm_map' := fun z => by576 refine Completion.induction_on z (isClosed_eq ?_ ?_) (fun x => ?_)577 · exact continuous_norm.comp Completion.continuous_extension578 · exact continuous_norm579 · change ‖Completion.extension (⇑Tli) (x : Completion X)‖ = ‖(x : Completion X)‖580 rw [Completion.extension_coe huc, Tli.norm_map, Completion.norm_coe] }581 have hTc_coe : ∀ a : X, Tc (a : Completion X) = T a := fun a =>582 Completion.extension_coe huc a583 have hdense : DenseRange ⇑Tc := by584 refine hT_dense.mono ?_585 rintro _ ⟨x, rfl⟩586 exact ⟨(x : Completion X), hTc_coe x⟩587 have hsurj : Function.Surjective ⇑Tc := by588 have hclosed : IsClosed (Set.range ⇑Tc) := Tc.isometry.isClosedEmbedding.isClosed_range589 rw [← Set.range_eq_univ, ← hclosed.closure_eq, hdense.closure_range]590 refine591 { toLinearIsometryEquiv := LinearIsometryEquiv.ofSurjective Tc hsurj592 map_sup' := fun z w => ?_593 map_inf' := fun z w => ?_ }594 · change Tc (z ⊔ w) = Tc z ⊔ Tc w595 refine Completion.induction_on₂ z w (isClosed_eq ?_ ?_) (fun x y => ?_)596 · exact Tc.continuous.comp ContinuousSup.continuous_sup597 · exact ContinuousSup.continuous_sup.comp598 ((Tc.continuous.comp continuous_fst).prodMk (Tc.continuous.comp continuous_snd))599 · rw [← coe_sup_completion, hTc_coe, hTc_coe, hTc_coe]600 exact T.map_sup' x y601 · change Tc (z ⊓ w) = Tc z ⊓ Tc w602 refine Completion.induction_on₂ z w (isClosed_eq ?_ ?_) (fun x y => ?_)603 · exact Tc.continuous.comp ContinuousInf.continuous_inf604 · exact ContinuousInf.continuous_inf.comp605 ((Tc.continuous.comp continuous_fst).prodMk (Tc.continuous.comp continuous_snd))606 · rw [← coe_inf_completion, hTc_coe, hTc_coe, hTc_coe]607 exact T.map_inf' x y608609end Completion610