Documentation

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Idempotent continuous linear maps #

In this file, we study the idempotent elements (IsIdempotentElem) of the ring M →L[R] M of continuous endomorphisms of a topological R-module M.

Main statements #

ContinuousLinearMap.isIdempotentElem_toLinearMap_iff: T is idempotent as an element of M →L[R] M if and only if it is such as an element of M →ₗ[R] M;
ContinuousLinearMap.IsIdempotentElem.ext_iff: idempotent elements of M →L[R] M are determined by their range and kernel;
ContinuousLinearMap.IsIdempotentElem.commute_iff: a continuous linear map S commutes with an idempotent T if and only if the range and kernel of T are S-invariant;
ContinuousLinearMap.IsIdempotentElem.isCLosed_range: an idempotent continuous linear map has closed range.

Further results can be found in the Mathlib/Topology/Algebra/Module/Complement.lean module, where we show that idempotent elements of M →L[R] M are precisely the projections associated to topological complement submodules.

theorem ContinuousLinearMap.isIdempotentElem_toLinearMap_iff {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] {f : M →L[R] M} :

IsIdempotentElem ↑f ↔ IsIdempotentElem f

theorem ContinuousLinearMap.IsIdempotentElem.toLinearMap {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] {f : M →L[R] M} :

IsIdempotentElem f → IsIdempotentElem ↑f

Alias of the reverse direction of ContinuousLinearMap.isIdempotentElem_toLinearMap_iff.

theorem ContinuousLinearMap.IsIdempotentElem.ext_iff {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : M →L[R] M} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :

p = q ↔ (↑p).range = (↑q).range ∧ (↑p).ker = (↑q).ker

Idempotent operators are equal iff their range and kernels are.

theorem ContinuousLinearMap.IsIdempotentElem.ext {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : M →L[R] M} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :

(↑p).range = (↑q).range ∧ (↑p).ker = (↑q).ker → p = q

Alias of the reverse direction of ContinuousLinearMap.IsIdempotentElem.ext_iff.

Idempotent operators are equal iff their range and kernels are.

theorem ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

(↑f).range ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = T ∘SL f

range f is invariant under T if and only if f ∘L T ∘L f = T ∘L f, for idempotent f.

theorem ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

f ∘SL T ∘SL f = T ∘SL f → (↑f).range ∈ Module.End.invtSubmodule ↑T

Alias of the reverse direction of ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff.

range f is invariant under T if and only if f ∘L T ∘L f = T ∘L f, for idempotent f.

theorem ContinuousLinearMap.IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

(↑f).range ∈ Module.End.invtSubmodule ↑T → f ∘SL T ∘SL f = T ∘SL f

Alias of the forward direction of ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff.

range f is invariant under T if and only if f ∘L T ∘L f = T ∘L f, for idempotent f.

theorem ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

(↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = f ∘SL T

ker f is invariant under T if and only if f ∘L T ∘L f = f ∘L T, for idempotent f.

theorem ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

f ∘SL T ∘SL f = f ∘SL T → (↑f).ker ∈ Module.End.invtSubmodule ↑T

Alias of the reverse direction of ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff.

ker f is invariant under T if and only if f ∘L T ∘L f = f ∘L T, for idempotent f.

theorem ContinuousLinearMap.IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

(↑f).ker ∈ Module.End.invtSubmodule ↑T → f ∘SL T ∘SL f = f ∘SL T

Alias of the forward direction of ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff.

ker f is invariant under T if and only if f ∘L T ∘L f = f ∘L T, for idempotent f.

theorem ContinuousLinearMap.IsIdempotentElem.commute_iff {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {f T : M →L[R] M} (hf : IsIdempotentElem f) :

Commute f T ↔ (↑f).range ∈ Module.End.invtSubmodule ↑T ∧ (↑f).ker ∈ Module.End.invtSubmodule ↑T

An idempotent operator f commutes with T if and only if both range f and ker f are invariant under T.

theorem ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] {f T : M →L[R] M} (hT : IsUnit T) (hf : IsIdempotentElem f) :

Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker

An idempotent operator f commutes with a unit operator T if and only if T (range f) = range f and T (ker f) = ker f.

@[deprecated LinearMap.IsIdempotentElem.range_eq_ker (since := "2025-12-27")]

theorem ContinuousLinearMap.IsIdempotentElem.range_eq_ker {S : Type u_5} [Semiring S] {E : Type u_7} [AddCommGroup E] [Module S E] {p : E →ₗ[S] E} (hp : IsIdempotentElem p) :

p.range = (LinearMap.id - p).ker

Alias of LinearMap.IsIdempotentElem.range_eq_ker.

@[deprecated LinearMap.IsIdempotentElem.ker_eq_range (since := "2025-12-27")]

theorem ContinuousLinearMap.IsIdempotentElem.ker_eq_range {S : Type u_5} [Semiring S] {E : Type u_7} [AddCommGroup E] [Module S E] {p : E →ₗ[S] E} (hp : IsIdempotentElem p) :

p.ker = (LinearMap.id - p).range

Alias of LinearMap.IsIdempotentElem.ker_eq_range.

theorem ContinuousLinearMap.IsIdempotentElem.isClosed_range {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] [T1Space M] {p : M →L[R] M} (hp : IsIdempotentElem p) :

IsClosed ↑(↑p).range