Intertwining linear maps

A linear map T : E →ₗ[R] F between topological modules, possibly discontinuous, is intertwined by continuous linear maps Q on F and P on E up to a continuous error when Q ∘ T - T ∘ P is continuous. This file shows that such intertwining pairs are closed under taking products. Exact intertwiners also intertwine the spectral operators 1 - a • u and their powers. Polynomial evaluation with zero constant coefficient commutes with extending an endomorphism along a continuous linear retract; no complement is needed.

Main results

• LinearMap.continuous_comp_sub_comp_of_continuous_sub: products of maps intertwining T up to continuous errors again intertwine T up to a continuous error.
• ContinuousLinearMap.aeval_comp_comp_of_retract: polynomial evaluation with zero constant coefficient commutes with extension along a retract.

theorem Function.Semiconj.one_sub_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [TopologicalSpace N] [AddCommGroup N] [Module R N] [IsTopologicalAddGroup N] [ContinuousConstSMul R N] {f : M →ₗ[R] N} {u : M →L[R] M} {v : N →L[R] N} (hf : Semiconj ⇑f ⇑u ⇑v) (a : R) : Semiconj ⇑f ⇑(1 - a • u) ⇑(1 - a • v)

A linear intertwiner also intertwines the associated spectral operators.

theorem Function.Semiconj.one_sub_smul_pow {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [TopologicalSpace N] [AddCommGroup N] [Module R N] [IsTopologicalAddGroup N] [ContinuousConstSMul R N] {f : M →ₗ[R] N} {u : M →L[R] M} {v : N →L[R] N} (hf : Semiconj ⇑f ⇑u ⇑v) (a : R) (n : ℕ) : Semiconj ⇑f ⇑((1 - a • u) ^ n) ⇑((1 - a • v) ^ n)

A linear intertwiner intertwines every power of the associated spectral operators.

theorem LinearMap.continuous_comp_sub_comp_of_continuous_sub {R : Type u_1} {E : Type u_2} {F : Type u_3} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] (T : E →ₗ[R] F) (P : ℕ → E →L[R] E) (Q : ℕ → F →L[R] F) (hPQ : ∀ (n : ℕ), Continuous ⇑(↑(Q n) ∘ₗ T - T ∘ₗ ↑(P n))) {U : ℕ → E →L[R] E} (hU0 : U 0 = ContinuousLinearMap.id R E) (hU : ∀ (n : ℕ), U (n + 1) = U n ∘SL P n) {V : ℕ → F →L[R] F} (hV0 : V 0 = ContinuousLinearMap.id R F) (hV : ∀ (n : ℕ), V (n + 1) = V n ∘SL Q n) (n : ℕ) : Continuous ⇑(↑(V n) ∘ₗ T - T ∘ₗ ↑(U n))

If continuous linear maps Q n on F intertwine T with continuous linear maps P n on E up to continuous errors Q n ∘ T - T ∘ P n, then so do the products V n = Q 0 ∘ ⋯ ∘ Q (n - 1) and U n = P 0 ∘ ⋯ ∘ P (n - 1).

@[simp]

theorem ContinuousLinearMap.toLinearMap_aeval {R : Type u_1} {M : Type u_2} [CommSemiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (u : M →L[R] M) (p : Polynomial R) : ↑((Polynomial.aeval u) p) = (Polynomial.aeval ↑u) p

Forgetting continuity commutes with polynomial evaluation.

theorem ContinuousLinearMap.aeval_comp_comp_of_retract {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] [TopologicalSpace N] [AddCommGroup N] [Module R N] [IsTopologicalAddGroup N] [ContinuousConstSMul R N] {i : M →L[R] N} {r : N →L[R] M} (hri : r ∘SL i = ContinuousLinearMap.id R M) (u : M →L[R] M) {B : Polynomial R} (hB0 : B.coeff 0 = 0) : (Polynomial.aeval (i ∘SL u ∘SL r)) B = i ∘SL (Polynomial.aeval u) B ∘SL r

Extending an endomorphism along a retract commutes with evaluating a polynomial whose constant coefficient is zero. The condition ensures that the polynomial also vanishes on the kernel of the retraction.