isProj_iff_isIdempotentElem — Mathlib

English

A linear map f is a projection onto some submodule if and only if f is idempotent.

Русский

Линейное отображение является проекцией на какое‑то подмножество тогда и только тогда, когда оно идемпотентно.

LaTeX

$$$(\exists p, \IsProj p f) \iff \IsIdempotentElem f.$$$

Lean4

theorem isProj_iff_isIdempotentElem (f : M →ₗ[S] M) : (∃ p : Submodule S M, IsProj p f) ↔ IsIdempotentElem f :=
  by
  refine ⟨fun ⟨p, hp⟩ => ?_, fun h => ⟨_, IsIdempotentElem.isProj_range _ h⟩⟩
  ext x
  exact hp.map_id (f x) (hp.map_mem x)

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