Partially defined linear operators over topological vector spaces

We define basic notions of partially defined linear operators, which we call unbounded operators for short. In this file we prove all elementary properties of unbounded operators that do not assume that the underlying spaces are normed.

Main definitions

• LinearPMap.IsClosed: An unbounded operator is closed iff its graph is closed.
• LinearPMap.IsClosable: An unbounded operator is closable iff the closure of its graph is a graph.
• LinearPMap.closure: For a closable unbounded operator f : LinearPMap R E F the closure is the smallest closed extension of f. If f is not closable, then f.closure is defined as f.
• LinearPMap.HasCore: a submodule contained in the domain is a core if restricting to the core does not lose information about the unbounded operator.

Main statements

• LinearPMap.closable_iff_exists_closed_extension: an unbounded operator is closable iff it has a closed extension.
• LinearPMap.closable.exists_unique: there exists a unique closure
• LinearPMap.closureHasCore: the domain of f is a core of its closure

References

• [J. Weidmann, Linear Operators in Hilbert Spaces][weidmann_linear]

Tags

Unbounded operators, closed operators

Closed and closable operators

def LinearPMap.IsClosed {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] (f : E →ₗ.[R] F) : Prop

An unbounded operator is closed iff its graph is closed.

Equations

• LinearPMap.IsClosed f = IsClosed ↑(LinearPMap.graph f)

def LinearPMap.IsClosable {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] (f : E →ₗ.[R] F) : Prop

An unbounded operator is closable iff the closure of its graph is a graph.

Equations

• LinearPMap.IsClosable f = ∃ (f' : E →ₗ.[R] F), Submodule.topologicalClosure (LinearPMap.graph f) = LinearPMap.graph f'

theorem LinearPMap.IsClosed.isClosable {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearPMap.IsClosed f) : LinearPMap.IsClosable f

A closed operator is trivially closable.

theorem LinearPMap.IsClosable.leIsClosable {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (hf : LinearPMap.IsClosable f) (hfg : g ≤ f) : LinearPMap.IsClosable g

If g has a closable extension f, then g itself is closable.

theorem LinearPMap.IsClosable.existsUnique {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearPMap.IsClosable f) : ∃! (f' : E →ₗ.[R] F), Submodule.topologicalClosure (LinearPMap.graph f) = LinearPMap.graph f'

The closure is unique.

noncomputable def LinearPMap.closure {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] (f : E →ₗ.[R] F) : E →ₗ.[R] F

If f is closable, then f.closure is the closure. Otherwise it is defined as f.closure = f.

Equations

• LinearPMap.closure f = if hf : LinearPMap.IsClosable f then Exists.choose hf else f

theorem LinearPMap.closure_def {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearPMap.IsClosable f) : LinearPMap.closure f = Exists.choose hf

theorem LinearPMap.closure_def' {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : ¬LinearPMap.IsClosable f) : LinearPMap.closure f = f

theorem LinearPMap.IsClosable.graph_closure_eq_closure_graph {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearPMap.IsClosable f) : Submodule.topologicalClosure (LinearPMap.graph f) = LinearPMap.graph (LinearPMap.closure f)

The closure (as a submodule) of the graph is equal to the graph of the closure (as a LinearPMap).

theorem LinearPMap.le_closure {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] (f : E →ₗ.[R] F) : f ≤ LinearPMap.closure f

A LinearPMap is contained in its closure.

theorem LinearPMap.IsClosable.closure_mono {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} {g : E →ₗ.[R] F} (hg : LinearPMap.IsClosable g) (h : f ≤ g) : LinearPMap.closure f ≤ LinearPMap.closure g

theorem LinearPMap.IsClosable.closure_isClosed {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearPMap.IsClosable f) : LinearPMap.IsClosed (LinearPMap.closure f)

If f is closable, then the closure is closed.

theorem LinearPMap.IsClosable.closureIsClosable {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearPMap.IsClosable f) : LinearPMap.IsClosable (LinearPMap.closure f)

If f is closable, then the closure is closable.

theorem LinearPMap.isClosable_iff_exists_closed_extension {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} : LinearPMap.IsClosable f ↔ ∃ (g : E →ₗ.[R] F) (_ : LinearPMap.IsClosed g), f ≤ g

The core of a linear operator

structure LinearPMap.HasCore {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] (f : E →ₗ.[R] F) (S : Submodule R E) : Prop

A submodule S is a core of f if the closure of the restriction of f to S is again f.

• le_domain : S ≤ f.domain
• closure_eq : LinearPMap.closure (LinearPMap.domRestrict f S) = f

theorem LinearPMap.hasCore_def {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} {S : Submodule R E} (h : LinearPMap.HasCore f S) : LinearPMap.closure (LinearPMap.domRestrict f S) = f

theorem LinearPMap.closureHasCore {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] (f : E →ₗ.[R] F) : LinearPMap.HasCore (LinearPMap.closure f) f.domain

For every unbounded operator f the submodule f.domain is a core of its closure.

Note that we don't require that f is closable, due to the definition of the closure.

Topological properties of the inverse

theorem LinearPMap.closure_inverse_graph {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) (hf' : LinearPMap.IsClosable f) (hcf : LinearMap.ker (LinearPMap.closure f).toFun = ⊥) : LinearPMap.graph (LinearPMap.inverse (LinearPMap.closure f)) = Submodule.topologicalClosure (LinearPMap.graph (LinearPMap.inverse f))

If f is invertible and closable as well as its closure being invertible, then the graph of the inverse of the closure is given by the closure of the graph of the inverse.

theorem LinearPMap.inverse_isClosable_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) (hf' : LinearPMap.IsClosable f) : LinearPMap.IsClosable (LinearPMap.inverse f) ↔ LinearMap.ker (LinearPMap.closure f).toFun = ⊥

Assuming that f is invertible and closable, then the closure is invertible if and only if the inverse of f is closable.

theorem LinearPMap.inverse_closure {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) (hf' : LinearPMap.IsClosable f) (hcf : LinearMap.ker (LinearPMap.closure f).toFun = ⊥) : LinearPMap.closure (LinearPMap.inverse f) = LinearPMap.inverse (LinearPMap.closure f)

If f is invertible and closable, then taking the closure and the inverse commute.