English
If T is a unit operator, then for idempotent f, f commutes with T iff the images under T fix both range and ker of f.
Русский
Если T является обратимым оператором, то для идемпотентного f верно: f коммутирует с T тогда и только тогда, когда образ и ядро f фиксируются под действием T.
LaTeX
$$$\text{IsUnit}(T) \Rightarrow (\text{Commute}(f,T) \iff (\operatorname{map}_T(\operatorname{range} f) = \operatorname{range} f) \land (\operatorname{map}_T(\ker f) = \ker f))$$$
Lean4
/-- An idempotent operator `f` commutes with an unit operator `T` if and only if
`T (range f) = range f` and `T (ker f) = ker f`. -/
theorem commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T) (hf : IsIdempotentElem f) :
Commute f T ↔ (range f).map T = range f ∧ (ker f).map T = ker f :=
by
have := hT.map ContinuousLinearMap.toLinearMapRingHom
lift T to (M →L[R] M)ˣ using hT
simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using
LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap
