isProj_range_iff_isIdempotentElem

English

For a linear map f: M → M over S, IsProj (range f) f holds if and only if f is idempotent.

Русский

Для линейного отображения f: M → M над S верно: IsProj (range f) f тогда и только тогда, когда f идемпотентно (f^2=f).

LaTeX

$$$\IsProj(\operatorname{range}f)\ f \iff \IsIdempotentElem f.$$$

Lean4

theorem isProj_range_iff_isIdempotentElem (f : M →ₗ[S] M) : IsProj (range f) f ↔ IsIdempotentElem f :=
  by
  refine
    ⟨fun ⟨h1, h2⟩ => ?_, fun hf =>
      ⟨fun x => mem_range_self f x, fun x ⟨y, hy⟩ => by rw [← hy, ← Module.End.mul_apply, hf.eq]⟩⟩
  ext x
  exact h2 (f x) (h1 x)

Похожие утверждения