range_mem_invtSubmodule_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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