English
An idempotent operator f commutes with T iff both range f and ker f are invariant under T.
Русский
Идемпотентный оператор f коммутирует с T тогда и только тогда, когда и образ, и ядро f инвариантны относительно T.
LaTeX
$$$\text{IsIdempotentElem}(f) \Rightarrow \text{Commute}(f,T) \iff (\operatorname{range} f \in \mathrm{invtSubmodule}(T) \land \ker f \in \mathrm{invtSubmodule}(T))$$$
Lean4
/-- An idempotent operator `f` commutes with `T` if and only if
both `range f` and `ker f` are invariant under `T`. -/
theorem commute_iff {f T : M →L[R] M} (hf : IsIdempotentElem f) :
Commute f T ↔ (LinearMap.range f ∈ Module.End.invtSubmodule T ∧ LinearMap.ker f ∈ Module.End.invtSubmodule T) := by
simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← coe_comp] using
LinearMap.IsIdempotentElem.commute_iff (T := T) hf.toLinearMap
