M-structure

A projection P on a normed space X is said to be an L-projection (IsLprojection) if, for all x in X, $\Vert x\Vert =\Vert Px\Vert +\Vert (1-P)x\Vert$.

A projection P on a normed space X is said to be an M-projection if, for all x in X, $\Vert x\Vert =max(\Vert Px\Vert ,\Vert (1-P)x\Vert )$.

The L-projections on X form a Boolean algebra (IsLprojection.Subtype.BooleanAlgebra).

TODO (Motivational background)

The M-projections on a normed space form a Boolean algebra.

The range of an L-projection on a normed space X is said to be an L-summand of X. The range of an M-projection is said to be an M-summand of X.

When X is a Banach space, the Boolean algebra of L-projections is complete. Let X be a normed space with dual X^*. A closed subspace M of X is said to be an M-ideal if the topological annihilator M^∘ is an L-summand of X^*.

M-ideal, M-summands and L-summands were introduced by Alfsen and Effros in [alfseneffros1972] to study the structure of general Banach spaces. When A is a JB*-triple, the M-ideals of A are exactly the norm-closed ideals of A. When A is a JBW*-triple with predual X, the M-summands of A are exactly the weak*-closed ideals, and their pre-duals can be identified with the L-summands of X. In the special case when A is a C*-algebra, the M-ideals are exactly the norm-closed two-sided ideals of A, when A is also a W*-algebra the M-summands are exactly the weak*-closed two-sided ideals of A.

Implementation notes

The approach to showing that the L-projections form a Boolean algebra is inspired by MeasureTheory.MeasurableSpace.

Instead of using P : X →L[𝕜] X to represent projections, we use an arbitrary ring M with a faithful action on X. ContinuousLinearMap.apply_module can be used to recover the X →L[𝕜] X special case.

References

• [Behrends, M-structure and the Banach-Stone Theorem][behrends1979]
• [Harmand, Werner, Werner, M-ideals in Banach spaces and Banach algebras][harmandwernerwerner1993]

Tags

M-summand, M-projection, L-summand, L-projection, M-ideal, M-structure

structure IsLprojection (X : Type u_1) [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] (P : M) : Prop

A projection on a normed space X is said to be an L-projection if, for all x in X, $\Vert x\Vert =\Vert Px\Vert +\Vert (1-P)x\Vert$.

Note that we write P • x instead of P x for reasons described in the module docstring.

• proj : IsIdempotentElem P
• Lnorm : ∀ (x : X), ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖

theorem IsLprojection.proj {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : M} (self : IsLprojection X P) : IsIdempotentElem P

theorem IsLprojection.Lnorm {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : M} (self : IsLprojection X P) (x : X) : ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖

structure IsMprojection (X : Type u_1) [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] (P : M) : Prop

A projection on a normed space X is said to be an M-projection if, for all x in X, $\Vert x\Vert =max(\Vert Px\Vert ,\Vert (1-P)x\Vert )$.

Note that we write P • x instead of P x for reasons described in the module docstring.

• proj : IsIdempotentElem P
• Mnorm : ∀ (x : X), ‖x‖ = max ‖P • x‖ ‖(1 - P) • x‖

theorem IsMprojection.proj {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : M} (self : IsMprojection X P) : IsIdempotentElem P

theorem IsMprojection.Mnorm {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : M} (self : IsMprojection X P) (x : X) : ‖x‖ = max ‖P • x‖ ‖(1 - P) • x‖

theorem IsLprojection.Lcomplement {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : M} (h : IsLprojection X P) : IsLprojection X (1 - P)

theorem IsLprojection.Lcomplement_iff {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] (P : M) : IsLprojection X P ↔ IsLprojection X (1 - P)

theorem IsLprojection.commute {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] {P : M} {Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) : Commute P Q

theorem IsLprojection.mul {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] {P : M} {Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) : IsLprojection X (P * Q)

theorem IsLprojection.join {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] {P : M} {Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) : IsLprojection X (P + Q - P * Q)

instance IsLprojection.Subtype.hasCompl {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] : HasCompl { f : M // IsLprojection X f }

Equations

• IsLprojection.Subtype.hasCompl = { compl := fun (P : { f : M // IsLprojection X f }) => ⟨1 - ↑P, ⋯⟩ }

@[simp]

theorem IsLprojection.coe_compl {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] (P : { P : M // IsLprojection X P }) : ↑Pᶜ = 1 - ↑P

instance IsLprojection.Subtype.inf {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : Inf { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.inf = { inf := fun (P Q : { P : M // IsLprojection X P }) => ⟨↑P * ↑Q, ⋯⟩ }

@[simp]

theorem IsLprojection.coe_inf {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] (P : { P : M // IsLprojection X P }) (Q : { P : M // IsLprojection X P }) : ↑(P ⊓ Q) = ↑P * ↑Q

instance IsLprojection.Subtype.sup {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : Sup { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.sup = { sup := fun (P Q : { P : M // IsLprojection X P }) => ⟨↑P + ↑Q - ↑P * ↑Q, ⋯⟩ }

@[simp]

theorem IsLprojection.coe_sup {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] (P : { P : M // IsLprojection X P }) (Q : { P : M // IsLprojection X P }) : ↑(P ⊔ Q) = ↑P + ↑Q - ↑P * ↑Q

instance IsLprojection.Subtype.sdiff {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : SDiff { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.sdiff = { sdiff := fun (P Q : { P : M // IsLprojection X P }) => ⟨↑P * (1 - ↑Q), ⋯⟩ }

@[simp]

theorem IsLprojection.coe_sdiff {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] (P : { P : M // IsLprojection X P }) (Q : { P : M // IsLprojection X P }) : ↑(P \ Q) = ↑P * (1 - ↑Q)

instance IsLprojection.Subtype.partialOrder {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : PartialOrder { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.partialOrder = PartialOrder.mk ⋯

theorem IsLprojection.le_def {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] (P : { P : M // IsLprojection X P }) (Q : { P : M // IsLprojection X P }) : P ≤ Q ↔ ↑P = ↑(P ⊓ Q)

instance IsLprojection.Subtype.zero {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] : Zero { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.zero = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem IsLprojection.coe_zero {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] : ↑0 = 0

instance IsLprojection.Subtype.one {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] : One { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.one = { one := ⟨1, ⋯⟩ }

@[simp]

theorem IsLprojection.coe_one {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] : ↑1 = 1

instance IsLprojection.Subtype.boundedOrder {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : BoundedOrder { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.boundedOrder = BoundedOrder.mk

@[simp]

theorem IsLprojection.coe_bot {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : ↑⊥ = 0

@[simp]

theorem IsLprojection.coe_top {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : ↑⊤ = 1

theorem IsLprojection.compl_mul {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : { P : M // IsLprojection X P }} {Q : M} : ↑Pᶜ * Q = Q - ↑P * Q

theorem IsLprojection.mul_compl_self {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] {P : { P : M // IsLprojection X P }} : ↑P * ↑Pᶜ = 0

theorem IsLprojection.distrib_lattice_lemma {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] {P : { P : M // IsLprojection X P }} {Q : { P : M // IsLprojection X P }} {R : { P : M // IsLprojection X P }} : (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

instance IsLprojection.instLatticeSubtypeOfFaithfulSMul {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : Lattice { P : M // IsLprojection X P }

Equations

• IsLprojection.instLatticeSubtypeOfFaithfulSMul = Lattice.mk ⋯ ⋯ ⋯

instance IsLprojection.Subtype.distribLattice {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : DistribLattice { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.distribLattice = DistribLattice.mk ⋯

instance IsLprojection.Subtype.BooleanAlgebra {X : Type u_1} [NormedAddCommGroup X] {M : Type u_2} [Ring M] [Module M X] [FaithfulSMul M X] : BooleanAlgebra { P : M // IsLprojection X P }

Equations

• IsLprojection.Subtype.BooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯