ker_mem_invtSubmodule_iff — Mathlib

English

For idempotent f, ker f is invariant under T iff f ∘L T ∘L f = f ∘L T.

Русский

Для идемпотентного f, ядро f инвариантно относительно T тогда и только тогда, когда f ∘ L T ∘ L f = f ∘ L T.

LaTeX

$$$\text{IsIdempotentElem}(f) \Rightarrow (\ker f \in \mathrm{End}_{R}(M)\,\text{invtSubmodule } T) \iff f \circ_L T \circ_L f = f \circ_L T$$$

Lean4

/-- `ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`,
for idempotent `f`. -/
theorem ker_mem_invtSubmodule_iff {f T : M →L[R] M} (hf : IsIdempotentElem f) :
    LinearMap.ker f ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = f ∘L T := by
  simpa [← ContinuousLinearMap.coe_comp] using
    LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap

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