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 [AE72] 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
- Harmand, Werner, Werner, M-ideals in Banach spaces and Banach algebras
Tags #
M-summand, M-projection, L-summand, L-projection, M-ideal, M-structure
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.
- proj : IsIdempotentElem P
Instances For
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.
- proj : IsIdempotentElem P
Instances For
Equations
- IsLprojection.Subtype.hasCompl = { compl := fun (P : { f : M // IsLprojection X f }) => โจ1 - โP, โฏโฉ }
Equations
- IsLprojection.Subtype.inf = { inf := fun (P Q : { P : M // IsLprojection X P }) => โจโP * โQ, โฏโฉ }
Equations
- IsLprojection.Subtype.sup = { sup := fun (P Q : { P : M // IsLprojection X P }) => โจโP + โQ - โP * โQ, โฏโฉ }
Equations
- IsLprojection.Subtype.sdiff = { sdiff := fun (P Q : { P : M // IsLprojection X P }) => โจโP * (1 - โQ), โฏโฉ }
Equations
- IsLprojection.Subtype.partialOrder = PartialOrder.mk โฏ
Equations
- IsLprojection.Subtype.zero = { zero := โจ0, โฏโฉ }
Equations
- IsLprojection.Subtype.one = { one := โจ1, โฏโฉ }
Equations
- IsLprojection.Subtype.boundedOrder = BoundedOrder.mk
Equations
- IsLprojection.instLatticeSubtypeOfFaithfulSMul = Lattice.mk โฏ โฏ โฏ
Equations
- IsLprojection.Subtype.distribLattice = DistribLattice.mk โฏ
Equations
- IsLprojection.Subtype.BooleanAlgebra = BooleanAlgebra.mk โฏ โฏ โฏ โฏ โฏ โฏ