M-structure #
A projection P on a normed space X is said to be an L-projection (is_Lprojection
) 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 (is_Lprojection.subtype.boolean_algebra
).
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
measure_theory.measurable_space
.
Instead of using P : X βL[π] X
to represent projections, we use an arbitrary ring M
with a
faithful action on X
. continuous_linear_map.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 : is_idempotent_elem P
- Mnorm : β (x : X), βxβ = linear_order.max βP β’ xβ β(1 - P) β’ xβ
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.
Equations
- is_Lprojection.subtype.has_compl = {compl := Ξ» (P : {f // is_Lprojection X f}), β¨1 - βP, _β©}
Equations
- is_Lprojection.subtype.has_inf = {inf := Ξ» (P Q : {P // is_Lprojection X P}), β¨βP * βQ, _β©}
Equations
- is_Lprojection.subtype.has_sdiff = {sdiff := Ξ» (P Q : {P // is_Lprojection X P}), β¨βP * (1 - βQ), _β©}
Equations
- is_Lprojection.subtype.partial_order = {le := Ξ» (P Q : {P // is_Lprojection X P}), βP = β(P β Q), lt := preorder.lt._default (Ξ» (P Q : {P // is_Lprojection X P}), βP = β(P β Q)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
- is_Lprojection.subtype.has_zero = {zero := β¨0, _β©}
Equations
- is_Lprojection.subtype.has_one = {one := β¨1, _β©}
Equations
- is_Lprojection.subtype.distrib_lattice = {sup := has_sup.sup is_Lprojection.subtype.has_sup, le := partial_order.le is_Lprojection.subtype.partial_order, lt := partial_order.lt is_Lprojection.subtype.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf is_Lprojection.subtype.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
Equations
- is_Lprojection.subtype.boolean_algebra = {sup := distrib_lattice.sup is_Lprojection.subtype.distrib_lattice, le := distrib_lattice.le is_Lprojection.subtype.distrib_lattice, lt := distrib_lattice.lt is_Lprojection.subtype.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf is_Lprojection.subtype.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := has_compl.compl is_Lprojection.subtype.has_compl, sdiff := has_sdiff.sdiff is_Lprojection.subtype.has_sdiff, himp := Ξ» (x y : {P // is_Lprojection X P}), distrib_lattice.sup y xαΆ, top := bounded_order.top is_Lprojection.subtype.bounded_order, bot := bounded_order.bot is_Lprojection.subtype.bounded_order, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}