# Documentation

Mathlib.Analysis.NormedSpace.MStructure

# 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.

• [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