Restriction of scalars for continuous linear maps

In this file, we define and study ContinuousLinearMap.restrictScalars, which reinterprets a continuous R-linear map as a continuous S-linear map, for suitable R and S. This is the continuous version of LinearMap.restrictScalars.

def ContinuousLinearMap.restrictScalars {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} (R : Type u_4) [Semiring A] [Semiring R] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂) : M₁ →L[R] M₂

If A is an R-algebra, then a continuous A-linear map can be interpreted as a continuous R-linear map. We assume LinearMap.CompatibleSMul M₁ M₂ R A to match assumptions of LinearMap.map_smul_of_tower.

Equations

• ContinuousLinearMap.restrictScalars R f = { toLinearMap := ↑R ↑f, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_restrictScalars {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [Semiring A] [Semiring R] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂) : ↑(restrictScalars R f) = ↑R ↑f

@[simp]

theorem ContinuousLinearMap.coe_restrictScalars' {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [Semiring A] [Semiring R] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂) : ⇑(restrictScalars R f) = ⇑f

@[simp]

theorem ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [Semiring A] [Semiring R] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂) : ↑(restrictScalars R f) = ↑f

@[simp]

theorem ContinuousLinearMap.restrictScalars_zero {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [Semiring A] [Semiring R] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] : restrictScalars R 0 = 0

@[simp]

theorem ContinuousLinearMap.restrictScalars_add {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [Semiring A] [Semiring R] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] [ContinuousAdd M₂] (f g : M₁ →L[A] M₂) : restrictScalars R (f + g) = restrictScalars R f + restrictScalars R g

@[simp]

theorem ContinuousLinearMap.restrictScalars_smul {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} {S : Type u_5} [Semiring A] [Semiring R] [Semiring S] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] (c : S) (f : M₁ →L[A] M₂) : restrictScalars R (c • f) = c • restrictScalars R f

def ContinuousLinearMap.restrictScalarsₗ (A : Type u_1) (M₁ : Type u_2) (M₂ : Type u_3) (R : Type u_4) (S : Type u_5) [Semiring A] [Semiring R] [Semiring S] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] [ContinuousAdd M₂] : (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂

ContinuousLinearMap.restrictScalars as a LinearMap. See also ContinuousLinearMap.restrictScalarsL.

Equations

• ContinuousLinearMap.restrictScalarsₗ A M₁ M₂ R S = { toFun := ContinuousLinearMap.restrictScalars R, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsₗ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} {S : Type u_5} [Semiring A] [Semiring R] [Semiring S] [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] [ContinuousAdd M₂] : ⇑(restrictScalarsₗ A M₁ M₂ R S) = restrictScalars R

@[simp]

theorem ContinuousLinearMap.restrictScalars_sub {A : Type u_1} {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Ring A] [Ring R] [AddCommGroup M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommGroup M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] [IsTopologicalAddGroup M₂] (f g : M₁ →L[A] M₂) : restrictScalars R (f - g) = restrictScalars R f - restrictScalars R g

@[simp]

theorem ContinuousLinearMap.restrictScalars_neg {A : Type u_1} {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Ring A] [Ring R] [AddCommGroup M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] [AddCommGroup M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] [LinearMap.CompatibleSMul M₁ M₂ R A] [IsTopologicalAddGroup M₂] (f : M₁ →L[A] M₂) : restrictScalars R (-f) = -restrictScalars R f