Restriction of scalars for partial linear maps

A partial linear map A : E →ₗ.[R] F over a ring R is in particular linear over any ring S acting compatibly through R, with the same domain and the same values. This file records that restriction, LinearPMap.restrictScalars S A, the partial-map analogue of Submodule.restrictScalars and LinearMap.restrictScalars. Its purpose is to let operator properties defined over a smaller scalar ring be applied to operators over a larger one; the motivating case is S = ℝ, R = ℂ, where the real-Banach-first semigroup development of Tau Ceti (dissipativity, generation of C₀-semigroups) is applied to operators on a complex Hilbert space. Since domain and action are preserved, membership and evaluation transport back and forth without change, and negation commutes with the restriction.

Main declarations

• LinearPMap.restrictScalars: the restriction of a partial linear map to a smaller scalar ring.
• LinearPMap.mem_restrictScalars_domain and LinearPMap.restrictScalars_apply: domain membership and evaluation agree with those of the original map.
• LinearPMap.restrictScalars_neg and LinearPMap.restrictScalars_smul: restriction of scalars commutes with negation and with scalar multiplication of the map.
• LinearPMap.restrictScalars_injective: a map is determined by its restriction.
• LinearPMap.restrictScalars_graph and LinearPMap.congr_fun_restrictScalars: the graph is the restriction of scalars of the graph, and a map equal to a restriction takes the restricted map's values.

def LinearPMap.restrictScalars (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) : E →ₗ.[S] F

A partial linear map over R, regarded as a partial linear map over the smaller scalar ring S, with the same domain and values.

Equations

• LinearPMap.restrictScalars S A = { domain := Submodule.restrictScalars S A.domain, toFun := ↑S A.toFun }

@[simp]

theorem LinearPMap.restrictScalars_domain (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) : (restrictScalars S A).domain = Submodule.restrictScalars S A.domain

theorem LinearPMap.mem_restrictScalars_domain (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) {x : E} : x ∈ (restrictScalars S A).domain ↔ x ∈ A.domain

Membership in the domain of the restriction is membership in the domain of A. This is what simp proves from restrictScalars_domain, packaged for use in proof terms.

@[simp]

theorem LinearPMap.restrictScalars_apply (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) (x : ↥(restrictScalars S A).domain) : ↑(restrictScalars S A) x = ↑A ⟨↑x, ⋯⟩

The restriction takes the values of A.

@[simp]

theorem LinearPMap.restrictScalars_neg (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) : restrictScalars S (-A) = -restrictScalars S A

Restriction of scalars commutes with negation.

@[simp]

theorem LinearPMap.restrictScalars_smul (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] [SMulCommClass S M F] (a : M) (A : E →ₗ.[R] F) : restrictScalars S (a • A) = a • restrictScalars S A

Restriction of scalars commutes with scalar multiplication of the map.

theorem LinearPMap.restrictScalars_injective (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] : Function.Injective (restrictScalars S)

Restriction of scalars is injective: a partial linear map is determined by its restriction.

@[simp]

theorem LinearPMap.restrictScalars_graph (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) : (restrictScalars S A).graph = Submodule.restrictScalars S A.graph

The graph of the restriction of scalars is the restriction of scalars of the graph.

theorem LinearPMap.restrictScalars_coe_graph (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] (A : E →ₗ.[R] F) : ↑(restrictScalars S A).graph = ↑A.graph

Restricting scalars does not change the graph, as a set.

theorem LinearPMap.congr_fun_restrictScalars (S : Type u_1) {R : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [Module S E] [Module S F] [SMul S R] [IsScalarTower S R E] [IsScalarTower S R F] {B : E →ₗ.[S] F} {A : E →ₗ.[R] F} (h : B = restrictScalars S A) {x : E} (hx : x ∈ B.domain) (hxA : x ∈ A.domain) : ↑B ⟨x, hx⟩ = ↑A ⟨x, hxA⟩

A partial linear map equal to a restriction of scalars takes the values of the restricted map.