# M-structure #

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

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

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) {M : Type u_2} [Ring M] [Module M X] (P : M) :

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

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

Instances For
theorem IsLprojection.proj {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : M} (self : ) :
theorem IsLprojection.Lnorm {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : M} (self : ) (x : X) :
structure IsMprojection (X : Type u_1) {M : Type u_2} [Ring M] [Module M X] (P : M) :

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

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

Instances For
theorem IsMprojection.proj {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : M} (self : ) :
theorem IsMprojection.Mnorm {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : M} (self : ) (x : X) :
theorem IsLprojection.Lcomplement {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : M} (h : ) :
theorem IsLprojection.Lcomplement_iff {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] (P : M) :
theorem IsLprojection.commute {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] {P : M} {Q : M} (hโ : ) (hโ : ) :
theorem IsLprojection.mul {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] {P : M} {Q : M} (hโ : ) (hโ : ) :
theorem IsLprojection.join {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] {P : M} {Q : M} (hโ : ) (hโ : ) :
IsLprojection X (P + Q - P * Q)
instance IsLprojection.Subtype.hasCompl {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] :
HasCompl { f : M // }
Equations
• IsLprojection.Subtype.hasCompl = { compl := fun (P : { f : M // }) => โจ1 - โP, โฏโฉ }
@[simp]
theorem IsLprojection.coe_compl {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] (P : { P : M // }) :
โPแถ = 1 - โP
instance IsLprojection.Subtype.inf {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
Inf { P : M // }
Equations
• IsLprojection.Subtype.inf = { inf := fun (P Q : { P : M // }) => โจโP * โQ, โฏโฉ }
@[simp]
theorem IsLprojection.coe_inf {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] (P : { P : M // }) (Q : { P : M // }) :
โ(P โ Q) = โP * โQ
instance IsLprojection.Subtype.sup {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
Sup { P : M // }
Equations
• IsLprojection.Subtype.sup = { sup := fun (P Q : { P : M // }) => โจโP + โQ - โP * โQ, โฏโฉ }
@[simp]
theorem IsLprojection.coe_sup {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] (P : { P : M // }) (Q : { P : M // }) :
โ(P โ Q) = โP + โQ - โP * โQ
instance IsLprojection.Subtype.sdiff {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
SDiff { P : M // }
Equations
• IsLprojection.Subtype.sdiff = { sdiff := fun (P Q : { P : M // }) => โจโP * (1 - โQ), โฏโฉ }
@[simp]
theorem IsLprojection.coe_sdiff {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] (P : { P : M // }) (Q : { P : M // }) :
โ(P \ Q) = โP * (1 - โQ)
instance IsLprojection.Subtype.partialOrder {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
PartialOrder { P : M // }
Equations
• IsLprojection.Subtype.partialOrder =
theorem IsLprojection.le_def {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] (P : { P : M // }) (Q : { P : M // }) :
P โค Q โ โP = โ(P โ Q)
instance IsLprojection.Subtype.zero {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] :
Zero { P : M // }
Equations
• IsLprojection.Subtype.zero = { zero := โจ0, โฏโฉ }
@[simp]
theorem IsLprojection.coe_zero {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] :
โ0 = 0
instance IsLprojection.Subtype.one {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] :
One { P : M // }
Equations
• IsLprojection.Subtype.one = { one := โจ1, โฏโฉ }
@[simp]
theorem IsLprojection.coe_one {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] :
โ1 = 1
instance IsLprojection.Subtype.boundedOrder {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
BoundedOrder { P : M // }
Equations
• IsLprojection.Subtype.boundedOrder = BoundedOrder.mk
@[simp]
theorem IsLprojection.coe_bot {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
โโฅ = 0
@[simp]
theorem IsLprojection.coe_top {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
โโค = 1
theorem IsLprojection.compl_mul {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : { P : M // }} {Q : M} :
โPแถ * Q = Q - โP * Q
theorem IsLprojection.mul_compl_self {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] {P : { P : M // }} :
โP * โPแถ = 0
theorem IsLprojection.distrib_lattice_lemma {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] {P : { P : M // }} {Q : { P : M // }} {R : { P : M // }} :
(โP + โPแถ * โR) * (โP + โQ * โR * โPแถ) = โP + โQ * โR * โPแถ
instance IsLprojection.instLatticeSubtypeOfFaithfulSMul {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
Lattice { P : M // }
Equations
• IsLprojection.instLatticeSubtypeOfFaithfulSMul = Lattice.mk โฏ โฏ โฏ
instance IsLprojection.Subtype.distribLattice {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
DistribLattice { P : M // }
Equations
• IsLprojection.Subtype.distribLattice =
instance IsLprojection.Subtype.BooleanAlgebra {X : Type u_1} {M : Type u_2} [Ring M] [Module M X] [] :
BooleanAlgebra { P : M // }
Equations
• One or more equations did not get rendered due to their size.