English
There is a bijection between idempotent endomorphisms f with range p and linear maps E → p that restrict to the identity on p.
Русский
Существует биекция между идемпотентными эндоморфизмами f с образцом p и линейными отображениями E → p, которые ограничиваются тождественным отображением на p.
LaTeX
$$$\{ f \in \mathrm{End}_R(E) \mid f^2=f,\ \operatorname{range}(f)=p \} \simeq \{ g: E \to p \mid g|_p = \mathrm{id}_p \}.$$$
Lean4
/-- The idempotent endomorphisms of a module with range equal to a submodule are in 1-1
correspondence with linear maps to the submodule that restrict to the identity on the submodule. -/
@[simps]
def isIdempotentElemEquiv :
{ f : Module.End R E // IsIdempotentElem f ∧ range f = p } ≃ { f : E →ₗ[R] p // ∀ x : p, f x = x }
where
toFun
f :=
⟨f.1.codRestrict _ fun x ↦ by simp_rw [← f.2.2]; exact mem_range_self f.1 x, fun ⟨x, hx⟩ ↦
Subtype.ext <| by
obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
exact DFunLike.congr_fun f.2.1 x⟩
invFun
f :=
⟨p.subtype ∘ₗ f.1, LinearMap.ext fun x ↦ by simp [f.2],
le_antisymm ((range_comp_le_range _ _).trans_eq p.range_subtype) fun x hx ↦ ⟨x, Subtype.ext_iff.1 <| f.2 ⟨x, hx⟩⟩⟩
