English
If P and Q are L-projections on X and the scalar action is faithful, then P and Q commute: PQ = QP.
Русский
Если P и Q — L-проекции на X и действие скаляров безошибочно выпукло, то P и Q коммутируют: PQ = QP.
LaTeX
$$If $P,Q$ are L-projections on $X$ with faithful scalar action, then $PQ=QP$.$$
Lean4
theorem commute [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) : Commute P Q :=
by
have PR_eq_RPR : ∀ R : M, IsLprojection X R → P * R = R * P * R := fun R h₃ => by
refine
@eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
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), 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
rw [ge_iff_le]
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_iff_le] at e1
nth_rewrite 2 [← 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_iff_right₀ (show (0 : ℝ) < 2 by simp)] at e1
have QP_eq_QPQ : Q * P = Q * P * Q :=
by
have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
calc
P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
_ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
rwa [eq_sub_iff_add_eq, add_eq_left, sub_eq_zero] at e1
change P * Q = Q * P
rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
