refactor(analysis/normed_space/M_structure): generalize to arbitrary faithful actions (#14222)

This follows up from a comment in review of #12173

The motivation here is to allow `X →L[𝕜] X`, `X →+ X`, and other weaker or stronger endomorphisms to also be used

This also tides up a few proof names and some poorly-rendering LaTeX

Author: eric-wieser

src/analysis/normed_space/M_structure.lean

@@ -10,19 +10,14 @@ import tactic.noncomm_ring
 /-!
 # M-structure
 
-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∥.
-$$
+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 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∥).
-$$
+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.
+The L-projections on `X` form a Boolean algebra (`is_Lprojection.subtype.boolean_algebra`).
 
 ## TODO (Motivational background)
 
@@ -48,6 +43,10 @@ two-sided ideals of `A`.
 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][behrends1979]
@@ -59,62 +58,66 @@ M-summand, M-projection, L-summand, L-projection, M-ideal, M-structure
 
 -/
 
-variables {X : Type*} [normed_group X]
-
-variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 X]
-
+variables (X : Type*) [normed_group X]
+variables {M : Type} [ring M] [module M X]
 /--
 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∥.
-$$
+$\|x\| = \|P x\| + \|(1 - P) x\|$.
+
+Note that we write `P • x` instead of `P x` for reasons described in the module docstring.
 -/
-structure is_Lprojection (P : X →L[𝕜] X) : Prop :=
+structure is_Lprojection (P : M) : Prop :=
 (proj : is_idempotent_elem P)
-(Lnorm : ∀ (x : X), ∥x∥ = ∥P x∥ + ∥(1 - P) x∥)
+(Lnorm : ∀ (x : X), ∥x∥ = ∥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∥).
-$$
+$\|x\| = max(\|P x\|,\|(1 - P) x\|)$.
+
+Note that we write `P • x` instead of `P x` for reasons described in the module docstring.
 -/
-structure is_Mprojection (P : X →L[𝕜] X) : Prop :=
+structure is_Mprojection (P : M) : Prop :=
 (proj : is_idempotent_elem P)
-(Mnorm : ∀ (x : X), ∥x∥ = (max ∥P x∥  ∥(1 - P) x∥))
+(Mnorm : ∀ (x : X), ∥x∥ = (max ∥P • x∥ ∥(1 - P) • x∥))
+
+variables {X}
 
 namespace is_Lprojection
 
-lemma Lcomplement {P : X →L[𝕜] X} (h: is_Lprojection P) :  is_Lprojection (1 - P) :=
+lemma Lcomplement {P : M} (h: is_Lprojection X P) : is_Lprojection X (1 - P) :=
 ⟨h.proj.one_sub, λ x, by { rw [add_comm, sub_sub_cancel], exact h.Lnorm x }⟩
 
-lemma Lcomplement_iff (P : X →L[𝕜] X) : is_Lprojection P ↔ is_Lprojection (1 - P) :=
+lemma Lcomplement_iff (P : M) : is_Lprojection X P ↔ is_Lprojection X (1 - P) :=
 ⟨Lcomplement, λ h, sub_sub_cancel 1 P ▸ h.Lcomplement⟩
 
-lemma commute {P Q : X →L[𝕜] X} (h₁ : is_Lprojection P) (h₂ : is_Lprojection Q) : commute P Q :=
+lemma commute [has_faithful_scalar M X] {P Q : M} (h₁ : is_Lprojection X P)
+  (h₂ : is_Lprojection X Q) : commute P Q :=
 begin
-  have PR_eq_RPR : ∀ R : (X →L[𝕜] X), is_Lprojection R →  (P * R = R * P * R) :=λ R h₃,
+  have PR_eq_RPR : ∀ R : M, is_Lprojection X R → P * R = R * P * R := λ R h₃,
   begin
-    ext,
+    refine @eq_of_smul_eq_smul _ X _ _ _ _ (λ x, _),
     rw ← norm_sub_eq_zero_iff,
-    have e1 : ∥R x∥ ≥ ∥R x∥ + 2 • ∥ (P * R) x - (R * P * R) x∥ :=
-    calc ∥R x∥ = ∥R (P (R x))∥ + ∥(1 - R) (P (R x))∥ + (∥(R * R) x - R (P (R x))∥
-      + ∥(1 - R) ((1 - P) (R x))∥) :
-      by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) (R x)), continuous_linear_map.sub_apply 1 P,
-        continuous_linear_map.one_apply, map_sub, continuous_linear_map.coe_mul]
-    ... = ∥R (P (R x))∥ + ∥(1 - R) (P (R x))∥ + (∥R x - R (P (R x))∥
-      + ∥((1 - R) * R) x - (1 - R) (P (R x))∥) : by rw [h₃.proj.eq,
-        continuous_linear_map.sub_apply 1 P, continuous_linear_map.one_apply,
-        map_sub,continuous_linear_map.coe_mul]
-    ... = ∥R (P (R x))∥ + ∥(1 - R) (P (R x))∥ + (∥R x - R (P (R x))∥ + ∥(1 - R) (P (R x))∥) :
-      by rw [sub_mul, h₃.proj.eq, one_mul, sub_self, continuous_linear_map.zero_apply, zero_sub,
+    have e1 : ∥R • x∥ ≥ ∥R • x∥ + 2 • ∥ (P * R) • x - (R * P * R) • x∥ :=
+    calc ∥R • x∥ = ∥R • (P • (R • x))∥ + ∥(1 - R) • (P • (R • x))∥ +
+                   (∥(R * R) • x - R • (P • (R • x))∥ + ∥(1 - R) • ((1 - P) • (R • x))∥) :
+      by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • (R • x)), sub_smul 1 P,
+        one_smul, smul_sub, mul_smul]
+    ... = ∥R • (P • (R • x))∥ + ∥(1 - R) • (P • (R • x))∥ + (∥R • x - R • (P • (R • x))∥
+      + ∥((1 - R) * R) • x - (1 - R) • (P • (R • x))∥) : by rw [h₃.proj.eq,
+        sub_smul 1 P, one_smul, smul_sub, mul_smul]
+    ... = ∥R • (P • (R • x))∥ + ∥(1 - R) • (P • (R • x))∥ +
+          (∥R • x - R • (P • (R • x))∥ + ∥(1 - R) • (P • (R • x))∥) :
+      by rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub,
         norm_neg]
-    ... = ∥R (P (R x))∥ + ∥R x - R (P (R x))∥ + 2•∥(1 - R) (P (R x))∥  : by abel
-    ... ≥ ∥R x∥ + 2 • ∥ (P * R) x - (R * P * R) x∥ :
-      by exact add_le_add_right (norm_le_insert' (R x) (R (P (R x)))) (2•∥(1 - R) (P (R x))∥),
+    ... = ∥R • (P • (R • x))∥ + ∥R • x - R • (P • (R • x))∥ + 2•∥(1 - R) • (P • (R • x))∥ : by abel
+    ... ≥ ∥R • x∥ + 2 • ∥ (P * R) • x - (R * P * R) • x∥ : by
+      { rw ge,
+        have := add_le_add_right
+          (norm_le_insert' (R • x) (R • (P • (R • x)))) (2•∥(1 - R) • (P • (R • x))∥),
+        simpa only [mul_smul, sub_smul, one_smul] using this },
     rw ge at e1,
-    nth_rewrite_rhs 0 ← add_zero (∥R x∥) at e1,
-    rw [add_le_add_iff_left, two_smul,  ← two_mul]  at e1,
+    nth_rewrite_rhs 0 ← add_zero (∥R • x∥) at e1,
+    rw [add_le_add_iff_left, two_smul, ← two_mul] at e1,
     rw le_antisymm_iff,
     refine ⟨_, norm_nonneg _⟩,
     rwa [←mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2, by norm_num)] at e1
@@ -127,109 +130,112 @@ begin
   show P * Q = Q * P, by rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
 end
 
-lemma mul {P Q : X →L[𝕜] X} (h₁ : is_Lprojection P) (h₂ : is_Lprojection Q) :
-  is_Lprojection (P * Q) :=
+lemma mul [has_faithful_scalar M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :
+  is_Lprojection X (P * Q) :=
 begin
   refine ⟨is_idempotent_elem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, _⟩,
   intro x,
   refine le_antisymm _ _,
-  { calc ∥ x ∥ = ∥(P * Q) x + (x - (P * Q) x)∥ : by rw add_sub_cancel'_right ((P * Q) x) x
-    ... ≤ ∥(P * Q) x∥ + ∥ x - (P * Q) x ∥ : by apply norm_add_le
-    ... = ∥(P * Q) x∥ + ∥(1 - P * Q) x∥ : by rw [continuous_linear_map.sub_apply,
-      continuous_linear_map.one_apply] },
-  { calc ∥x∥ = ∥P (Q x)∥ + (∥Q x - P (Q x)∥ + ∥x - Q x∥) : by rw [h₂.Lnorm x, h₁.Lnorm (Q x),
-      continuous_linear_map.sub_apply, continuous_linear_map.one_apply,
-      continuous_linear_map.sub_apply, continuous_linear_map.one_apply, add_assoc]
-    ... ≥ ∥P (Q x)∥ + ∥(Q x - P (Q x)) + (x - Q x)∥ :
-      (add_le_add_iff_left (∥P(Q x)∥)).mpr (norm_add_le (Q x - P (Q x)) (x - Q x))
-    ... = ∥(P * Q) x∥ + ∥(1 - P * Q) x∥ : by rw [sub_add_sub_cancel',
-      continuous_linear_map.sub_apply, continuous_linear_map.one_apply,
-      continuous_linear_map.coe_mul] }
+  { calc ∥ x ∥ = ∥(P * Q) • x + (x - (P * Q) • x)∥ : by rw add_sub_cancel'_right ((P * Q) • x) x
+    ... ≤ ∥(P * Q) • x∥ + ∥ x - (P * Q) • x ∥ : by apply norm_add_le
+    ... = ∥(P * Q) • x∥ + ∥(1 - P * Q) • x∥ : by rw [sub_smul,
+      one_smul] },
+  { calc ∥x∥ = ∥P • (Q • x)∥ + (∥Q • x - P • (Q • x)∥ + ∥x - Q • x∥) : by
+      rw [h₂.Lnorm x, h₁.Lnorm (Q • x),
+          sub_smul, one_smul,
+          sub_smul, one_smul, add_assoc]
+    ... ≥ ∥P • (Q • x)∥ + ∥(Q • x - P • (Q • x)) + (x - Q • x)∥ :
+      (add_le_add_iff_left (∥P • (Q • x)∥)).mpr (norm_add_le (Q • x - P • (Q • x)) (x - Q • x))
+    ... = ∥(P * Q) • x∥ + ∥(1 - P * Q) • x∥ : by rw [sub_add_sub_cancel',
+      sub_smul, one_smul,
+      mul_smul] }
 end
 
-lemma join {P Q : X →L[𝕜] X} (h₁ : is_Lprojection P) (h₂ : is_Lprojection Q) :
-  is_Lprojection (P + Q - P * Q) :=
+lemma join [has_faithful_scalar M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :
+  is_Lprojection X (P + Q - P * Q) :=
 begin
   convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1,
   noncomm_ring,
 end
 
-instance : has_compl { f : X →L[𝕜] X // is_Lprojection f } :=
+instance : has_compl { f : M // is_Lprojection X f } :=
 ⟨λ P, ⟨1 - P, P.prop.Lcomplement⟩⟩
 
-@[simp] lemma coe_compl (P : {P : X →L[𝕜] X // is_Lprojection P}) :
-  ↑(Pᶜ) = (1 : X →L[𝕜] X) - ↑P := rfl
+@[simp] lemma coe_compl (P : {P : M // is_Lprojection X P}) :
+  ↑(Pᶜ) = (1 : M) - ↑P := rfl
 
-instance : has_inf {P : X →L[𝕜] X // is_Lprojection P} :=
+instance [has_faithful_scalar M X] : has_inf {P : M // is_Lprojection X P} :=
 ⟨λ P Q, ⟨P * Q, P.prop.mul Q.prop⟩ ⟩
 
-@[simp] lemma coe_inf (P Q : {P : X →L[𝕜] X // is_Lprojection P}) :
-  ↑(P ⊓ Q) = ((↑P : (X →L[𝕜] X)) * ↑Q) := rfl
+@[simp] lemma coe_inf [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+  ↑(P ⊓ Q) = ((↑P : (M)) * ↑Q) := rfl
 
-instance : has_sup {P : X →L[𝕜] X // is_Lprojection P} :=
+instance [has_faithful_scalar M X] : has_sup {P : M // is_Lprojection X P} :=
 ⟨λ P Q, ⟨P + Q - P * Q, P.prop.join Q.prop⟩ ⟩
 
-@[simp] lemma coe_sup (P Q : {P : X →L[𝕜] X // is_Lprojection P}) :
-  ↑(P ⊔ Q) = ((↑P : X →L[𝕜] X) + ↑Q - ↑P * ↑Q) := rfl
+@[simp] lemma coe_sup [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+  ↑(P ⊔ Q) = ((↑P : M) + ↑Q - ↑P * ↑Q) := rfl
 
-instance : has_sdiff {P : X →L[𝕜] X // is_Lprojection P} :=
+instance [has_faithful_scalar M X] : has_sdiff {P : M // is_Lprojection X P} :=
 ⟨λ P Q, ⟨P * (1 - Q), by exact P.prop.mul Q.prop.Lcomplement ⟩⟩
 
-@[simp] lemma coe_sdiff (P Q : {P : X →L[𝕜] X // is_Lprojection P}) :
-  ↑(P \ Q) = (↑P : X →L[𝕜] X) * (1 - ↑Q) := rfl
+@[simp] lemma coe_sdiff [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+  ↑(P \ Q) = (↑P : M) * (1 - ↑Q) := rfl
 
-instance : partial_order {P : X →L[𝕜] X // is_Lprojection P} :=
-{ le := λ P Q, (↑P : X →L[𝕜] X) = ↑(P ⊓ Q),
+instance [has_faithful_scalar M X] : partial_order {P : M // is_Lprojection X P} :=
+{ le := λ P Q, (↑P : M) = ↑(P ⊓ Q),
   le_refl := λ P, by simpa only [coe_inf, ←sq] using (P.prop.proj.eq).symm,
   le_trans := λ P Q R h₁ h₂, by { simp only [coe_inf] at ⊢ h₁ h₂, rw [h₁, mul_assoc, ←h₂] },
   le_antisymm := λ P Q h₁ h₂, subtype.eq (by convert (P.prop.commute Q.prop).eq) }
 
-lemma le_def (P Q : {P : X →L[𝕜] X // is_Lprojection P}) : P ≤ Q ↔ (P : X →L[𝕜] X) = ↑(P ⊓ Q) :=
+lemma le_def [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+  P ≤ Q ↔ (P : M) = ↑(P ⊓ Q) :=
 iff.rfl
 
-instance : has_zero {P : X →L[𝕜] X // is_Lprojection P}  :=
+instance : has_zero {P : M // is_Lprojection X P} :=
 ⟨⟨0, ⟨by rw [is_idempotent_elem, zero_mul],
-     λ x, by simp only [continuous_linear_map.zero_apply, norm_zero, sub_zero,
-                        continuous_linear_map.one_apply, zero_add]⟩⟩⟩
+     λ x, by simp only [zero_smul, norm_zero, sub_zero,
+                        one_smul, zero_add]⟩⟩⟩
 
-@[simp] lemma coe_zero : ↑(0 : {P : X →L[𝕜] X // is_Lprojection P}) = (0 : X →L[𝕜] X) :=
+@[simp] lemma coe_zero : ↑(0 : {P : M // is_Lprojection X P}) = (0 : M) :=
 rfl
 
-instance : has_one {P : X →L[𝕜] X // is_Lprojection P}  :=
-⟨⟨1, sub_zero (1 : X →L[𝕜] X) ▸ (0 : {P : X →L[𝕜] X // is_Lprojection P}).prop.Lcomplement⟩⟩
+instance : has_one {P : M // is_Lprojection X P} :=
+⟨⟨1, sub_zero (1 : M) ▸ (0 : {P : M // is_Lprojection X P}).prop.Lcomplement⟩⟩
 
-@[simp] lemma coe_one : ↑(1 : {P : X →L[𝕜] X // is_Lprojection P}) = (1 : X →L[𝕜] X) :=
+@[simp] lemma coe_one : ↑(1 : {P : M // is_Lprojection X P}) = (1 : M) :=
 rfl
 
-instance : bounded_order {P : X →L[𝕜] X // is_Lprojection P} :=
+instance [has_faithful_scalar M X] : bounded_order {P : M // is_Lprojection X P} :=
 { top := 1,
-  le_top := λ P, (by rw mul_one : (↑P : X  →L[𝕜] X) = ↑P * 1),
+  le_top := λ P, (mul_one (P : M)).symm,
   bot := 0,
-  bot_le := λ P, show 0 ≤ P, from zero_mul P, }
+  bot_le := λ P, (zero_mul (P : M)).symm, }
 
-@[simp] lemma coe_bot : ↑(bounded_order.bot : {P : X →L[𝕜] X // is_Lprojection P}) = (0 : X →L[𝕜] X)
-  := rfl
+@[simp] lemma coe_bot [has_faithful_scalar M X] :
+  ↑(bounded_order.bot : {P : M // is_Lprojection X P}) = (0 : M) := rfl
 
-@[simp] lemma coe_top : ↑(bounded_order.top : {P : X →L[𝕜] X // is_Lprojection P}) = (1 : X →L[𝕜] X)
-  := rfl
+@[simp] lemma coe_top [has_faithful_scalar M X] :
+  ↑(bounded_order.top : {P : M // is_Lprojection X P}) = (1 : M) := rfl
 
-lemma compl_mul_left {P : {P : X →L[𝕜] X // is_Lprojection P}} {Q : X →L[𝕜] X} :
-  Q - ↑P * Q = ↑Pᶜ * Q := by rw [coe_compl, sub_mul, one_mul]
+lemma compl_mul {P : {P : M // is_Lprojection X P}} {Q : M} :
+  ↑Pᶜ * Q = Q - ↑P * Q := by rw [coe_compl, sub_mul, one_mul]
 
-lemma compl_orthog {P : {P : X →L[𝕜] X // is_Lprojection P}} :
-  (↑P : X →L[𝕜] X) * (↑Pᶜ) = 0 :=
+lemma mul_compl_self {P : {P : M // is_Lprojection X P}} :
+  (↑P : M) * (↑Pᶜ) = 0 :=
 by rw [coe_compl, mul_sub, mul_one, P.prop.proj.eq, sub_self]
 
-lemma distrib_lattice_lemma {P Q R : {P : X →L[𝕜] X // is_Lprojection P}} :
-  ((↑P : X →L[𝕜] X) + ↑Pᶜ * R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = (↑P + ↑Q * ↑R * ↑Pᶜ) :=
-by rw [add_mul, mul_add, mul_add, mul_assoc ↑Pᶜ ↑R (↑Q * ↑R * ↑Pᶜ), ← mul_assoc ↑R (↑Q * ↑R)  ↑Pᶜ,
+lemma distrib_lattice_lemma [has_faithful_scalar M X] {P Q R : {P : M // is_Lprojection X P}} :
+  ((↑P : M) + ↑Pᶜ * R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = (↑P + ↑Q * ↑R * ↑Pᶜ) :=
+by rw [add_mul, mul_add, mul_add, mul_assoc ↑Pᶜ ↑R (↑Q * ↑R * ↑Pᶜ), ← mul_assoc ↑R (↑Q * ↑R) ↑Pᶜ,
     ← coe_inf Q, (Pᶜ.prop.commute R.prop).eq, ((Q ⊓ R).prop.commute Pᶜ.prop).eq,
     (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q, mul_assoc ↑Q, ← mul_assoc, mul_assoc ↑R,
-    (Pᶜ.prop.commute P.prop).eq, compl_orthog, zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc,
+    (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero, zero_add, add_zero,
+    ← mul_assoc,
     P.prop.proj.eq, R.prop.proj.eq, ← coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute Pᶜ.prop).eq,
     ← mul_assoc, Pᶜ.prop.proj.eq]
 
-instance : distrib_lattice {P : X →L[𝕜] X // is_Lprojection P} :=
+instance [has_faithful_scalar M X] : distrib_lattice {P : M // is_Lprojection X P} :=
 { le_sup_left := λ P Q, by rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc,
     P.prop.proj.eq, sub_self, add_zero],
   le_sup_right := λ P Q,
@@ -257,35 +263,33 @@ instance : distrib_lattice {P : X →L[𝕜] X // is_Lprojection P} :=
   begin
     have e₁: ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ :=
     by rw [coe_inf, coe_sup, coe_sup,
-      ← add_sub, ← add_sub, compl_mul_left, compl_mul_left, add_mul, mul_add,
+      ← add_sub, ← add_sub, ←compl_mul, ←compl_mul, add_mul, mul_add,
       (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc ↑Q, (Pᶜ.prop.commute P.prop).eq,
-      compl_orthog, zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc ↑Q,
+      mul_compl_self, zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc ↑Q,
       P.prop.proj.eq, Pᶜ.prop.proj.eq, mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc],
     have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ := by rw [coe_inf, coe_sup,
-      coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, compl_mul_left, compl_mul_left,
-      compl_mul_left, (Pᶜ.prop.commute (Q⊓R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma,
+      coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ←compl_mul, ←compl_mul,
+      ←compl_mul, (Pᶜ.prop.commute (Q⊓R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma,
       (Q.prop.commute R.prop).eq, distrib_lattice_lemma],
     rw [le_def, e₁, coe_inf, e₂],
   end,
   .. is_Lprojection.subtype.has_inf,
   .. is_Lprojection.subtype.has_sup,
   .. is_Lprojection.subtype.partial_order }
 
-instance : boolean_algebra {P : X →L[𝕜] X // is_Lprojection P} :=
-{ sup_inf_sdiff := λ P Q,
-  subtype.ext (by rw [coe_sup, coe_inf, coe_sdiff, mul_assoc, ← mul_assoc ↑Q,
-    (Q.prop.commute P.prop).eq, mul_assoc ↑P ↑Q, ← coe_compl, compl_orthog, mul_zero, mul_zero,
-    sub_zero, ← mul_add, coe_compl, add_sub_cancel'_right, mul_one]),
-  inf_inf_sdiff := λ P Q,
-    subtype.ext (by rw [coe_inf, coe_inf, coe_sdiff, coe_bot, mul_assoc, ← mul_assoc ↑Q,
-    (Q.prop.commute P.prop).eq, ← coe_compl, mul_assoc, compl_orthog, mul_zero, mul_zero]),
+instance [has_faithful_scalar M X] : boolean_algebra {P : M // is_Lprojection X P} :=
+{ sup_inf_sdiff := λ P Q, subtype.ext $
+    by rw [coe_sup, coe_inf, coe_sdiff, mul_assoc, ← mul_assoc ↑Q,
+    (Q.prop.commute P.prop).eq, mul_assoc ↑P ↑Q, ← coe_compl, mul_compl_self, mul_zero, mul_zero,
+    sub_zero, ← mul_add, coe_compl, add_sub_cancel'_right, mul_one],
+  inf_inf_sdiff := λ P Q, subtype.ext $
+    by rw [coe_inf, coe_inf, coe_sdiff, coe_bot, mul_assoc, ← mul_assoc ↑Q,
+      (Q.prop.commute P.prop).eq, ← coe_compl, mul_assoc, mul_compl_self, mul_zero, mul_zero],
   inf_compl_le_bot := λ P,
-    (subtype.ext (by rw [coe_inf, coe_compl, coe_bot, ← coe_compl, compl_orthog])).le,
+    (subtype.ext (by rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self])).le,
   top_le_sup_compl := λ P, (subtype.ext(by rw [coe_top, coe_sup, coe_compl,
-    add_sub_cancel'_right, ← coe_compl, compl_orthog, sub_zero])).le,
-  sdiff_eq := λ P Q,
-  subtype.ext
-  (by rw [coe_sdiff, ← coe_compl, coe_inf]),
+    add_sub_cancel'_right, ← coe_compl, mul_compl_self, sub_zero])).le,
+  sdiff_eq := λ P Q, subtype.ext $ by rw [coe_sdiff, ← coe_compl, coe_inf],
   .. is_Lprojection.subtype.has_compl,
   .. is_Lprojection.subtype.has_sdiff,
   .. is_Lprojection.subtype.bounded_order,