feat(analysis/normed_space/M_structure): Define L-projections, show t…

…hey form a Boolean algebra (#12173)

A continuous projection P on a normed space X is said to be an L-projection if, for all `x` in `X`,
```
∥x∥ = ∥P x∥ + ∥(1-P) x∥.
```
The range of an L-projection is said to be an L-summand of X.

A continuous 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 range of an M-projection is said to be an M-summand of X.

The L-projections and M-projections form Boolean algebras. 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 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`.

This initial PR limits itself to showing that the L-projections form a Boolean algebra. The approach followed is based on that used in `measure_theory.measurable_space`. The equivalent result for M-projections can be established by a similar argument or by a duality result (to be established). However, I thought it best to seek feedback before proceeding further.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

docs/references.bib

@@ -18,6 +18,23 @@ @Article{         ahrens2017
   doi           = {10.23638/LMCS-15(1:20)2019}
 }
 
+@Article{         alfseneffros1972,
+  author        = {Erik M. {Alfsen} and Edward G. {Effros}},
+  title         = {{Structure in real Banach spaces. I and II}},
+  fjournal      = {{Annals of Mathematics. Second Series}},
+  journal       = {{Ann. Math. (2)}},
+  issn          = {0003-486X},
+  volume        = {96},
+  pages         = {98--173},
+  year          = {1972},
+  publisher     = {Princeton University, Mathematics Department, Princeton,
+                  NJ},
+  language      = {English},
+  doi           = {10.2307/1970895},
+  msc2010       = {46L05 46B10 46K05 46E15 46B99 46A40},
+  zbl           = {0248.46019}
+}
+
 @Book{            aluffi2016,
   title         = {Algebra: Chapter 0},
   author        = {Aluffi, Paolo},
@@ -95,6 +112,20 @@ @Book{            beals2004
   year          = {2004}
 }
 
+@Book{            behrends1979,
+  author        = {Ehrhard {Behrends}},
+  title         = {{M-structure and the Banach-Stone theorem}},
+  fjournal      = {{Lecture Notes in Mathematics}},
+  journal       = {{Lect. Notes Math.}},
+  issn          = {0075-8434},
+  volume        = {736},
+  year          = {1979},
+  publisher     = {Springer, Cham},
+  language      = {English},
+  msc2010       = {46B20 46-02 46E40 46A40},
+  zbl           = {0436.46013}
+}
+
 @Article{         bernstein1912,
   author        = {Bernstein, S.},
   year          = {1912},
@@ -822,6 +853,23 @@ @Book{            hardy2008introduction
   publisher     = {Oxford University Press}
 }
 
+@Book{            harmandwernerwerner1993,
+  author        = {Peter {Harmand} and Dirk {Werner} and Wend {Werner}},
+  title         = {{\(M\)-ideals in Banach spaces and Banach algebras}},
+  fjournal      = {{Lecture Notes in Mathematics}},
+  journal       = {{Lect. Notes Math.}},
+  issn          = {0075-8434},
+  volume        = {1547},
+  isbn          = {3-540-56814-X},
+  pages         = {viii + 387},
+  year          = {1993},
+  publisher     = {Berlin: Springer-Verlag},
+  language      = {English},
+  doi           = {10.1007/BFb0084355},
+  msc2010       = {46B20 46B25 46B22 46-02 46B28},
+  zbl           = {0789.46011}
+}
+
 @Article{         Haze09,
   title         = {Witt vectors. Part 1},
   isbn          = {9780444532572},

src/algebra/ring/idempotents.lean

@@ -43,57 +43,35 @@ lemma eq {p : M} (h : is_idempotent_elem p) : p * p = p := h
 
 lemma mul_of_commute {p q : S} (h : commute p q) (h₁ : is_idempotent_elem p)
   (h₂ : is_idempotent_elem q) : is_idempotent_elem (p * q)  :=
-  by rw [is_idempotent_elem, mul_assoc, ← mul_assoc q, ←h.eq, mul_assoc p, h₂.eq, ← mul_assoc,
-    h₁.eq]
+by rw [is_idempotent_elem, mul_assoc, ← mul_assoc q, ← h.eq, mul_assoc p, h₂.eq, ← mul_assoc, h₁.eq]
 
 lemma zero : is_idempotent_elem (0 : M₀) := mul_zero _
 
 lemma one : is_idempotent_elem (1 : M₁) := mul_one _
 
 lemma one_sub {p : R} (h : is_idempotent_elem p) : is_idempotent_elem (1 - p) :=
-begin
-  rw is_idempotent_elem at h,
-  rw [is_idempotent_elem, mul_sub_left_distrib, mul_one, sub_mul, one_mul, h, sub_self, sub_zero],
-end
+by rw [is_idempotent_elem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
 
 @[simp] lemma one_sub_iff {p : R} : is_idempotent_elem (1 - p) ↔ is_idempotent_elem p :=
 ⟨ λ h, sub_sub_cancel 1 p ▸ h.one_sub, is_idempotent_elem.one_sub ⟩
 
 lemma pow {p : N} (n : ℕ) (h : is_idempotent_elem p) : is_idempotent_elem (p ^ n) :=
-begin
-  induction n with n ih,
-  { rw pow_zero, apply one, },
-  { unfold is_idempotent_elem,
-    rw [pow_succ, ← mul_assoc, ← pow_mul_comm', mul_assoc (p^n), h.eq, pow_mul_comm', mul_assoc,
-      ih.eq], }
-end
+nat.rec_on n ((pow_zero p).symm ▸ one) (λ n ih, show p ^ n.succ * p ^ n.succ = p ^ n.succ,
+  by { nth_rewrite 2 ←h.eq, rw [←sq, ←sq, ←pow_mul, ←pow_mul'] })
 
 lemma pow_succ_eq {p : N} (n : ℕ) (h : is_idempotent_elem p) : p ^ (n + 1) = p :=
-begin
-  induction n with n ih,
-  { rw [nat.zero_add, pow_one], },
-  { rw [pow_succ, ih, h.eq], }
-end
+nat.rec_on n ((nat.zero_add 1).symm ▸ pow_one p) (λ n ih, by rw [pow_succ, ih, h.eq])
 
 @[simp] lemma iff_eq_one {p : G} : is_idempotent_elem p ↔ p = 1 :=
-begin
-  split,
-  { intro h,
-    rw ← mul_left_inv p,
-    nth_rewrite_rhs 1 ← h.eq,
-    rw [← mul_assoc, mul_left_inv, one_mul] },
-  { intro h, rw h, apply one, }
-end
+iff.intro (λ h, mul_left_cancel ((mul_one p).symm ▸ h.eq : p * p = p * 1)) (λ h, h.symm ▸ one)
 
 @[simp] lemma iff_eq_zero_or_one {p : G₀}  : is_idempotent_elem p ↔ p = 0 ∨ p = 1 :=
 begin
-  refine ⟨λ h, or_iff_not_imp_left.mpr (λ hp, _), _⟩,
-  { rw ← mul_inv_cancel hp,
-    nth_rewrite_rhs 0 ← h.eq,
-    rw [mul_assoc, mul_inv_cancel hp, mul_one] },
-   { rintro (h₁ | h₂),
-    { rw h₁, exact zero, },
-    { rw h₂, exact one, } }
+  refine iff.intro
+    (λ h, or_iff_not_imp_left.mpr (λ hp, _))
+    (λ h, h.elim (λ hp, hp.symm ▸ zero) (λ hp, hp.symm ▸ one)),
+  lift p to G₀ˣ using is_unit.mk0 _ hp,
+  exact_mod_cast iff_eq_one.mp (by exact_mod_cast h.eq),
 end
 
 /-! ### Instances on `subtype is_idempotent_elem` -/