English
If T is a unit (invertible) and f is idempotent, then f commutes with T if and only if T preserves both the image and the kernel of f.
Русский
Если T — инвертируемый оператор и f идемпотентен, тогда f коммутирует с T тогда и только тогда, когда T сохраняет и образ, и ядро f.
LaTeX
$$$ \text{Commute}(f,T) \iff (\operatorname{Im}(f)).map(T) = \operatorname{Im}(f) \wedge (\ker f).map(T) = \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 (hT : IsUnit T) (hf : IsIdempotentElem f) :
Commute f T ↔ (range f).map T = range f ∧ (ker f).map T = ker f :=
by
lift T to GeneralLinearGroup R E using hT
have {a : E ≃ₗ[R] E} {b : Submodule R E} : b ≤ b.map a.toLinearMap ↔ b ≤ b.map a := by rfl
simp_rw [← GeneralLinearGroup.generalLinearEquiv_to_linearMap, le_antisymm_iff, ←
Module.End.mem_invtSubmodule_iff_map_le, this, ← Module.End.mem_invtSubmodule_symm_iff_le_map,
and_and_and_comm (c := (ker f ∈ _)), ← hf.commute_iff, GeneralLinearGroup.generalLinearEquiv_to_linearMap,
iff_self_and]
exact Commute.units_inv_right
