LinearPMap.IsClosable.graph_closure_eq_closure_graph
theorem LinearPMap.IsClosable.graph_closure_eq_closure_graph :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
f.IsClosable → f.graph.topologicalClosure = f.closure.graph
This theorem states that for a given linear map `f` from a module `E` over a commutative ring `R` to a module `F` over the same ring, under certain conditions, the closure of the graph of `f` (viewed as a submodule of `E × F`) is equal to the graph of the closure of `f` (viewed as a `LinearPMap`). The conditions include that `R`, `E`, and `F` have topological space structures and addition and scalar multiplication are continuous operations. "Closure" in this context means the smallest closed set (in the topological sense) that contains the set. A `LinearPMap` is a partially defined linear map, and its graph is the set of all pairs `(x, f(x))` for `x` in the domain of definition.
More concisely: Given a linear map `f` between modules `E` and `F` over a commutative ring `R` with topological structures such that addition and scalar multiplication are continuous, the closure of `f`'s graph as a submodule of `E × F` equals the graph of the closure of `f` as a `LinearPMap`.
|
LinearPMap.IsClosable.closureIsClosable
theorem LinearPMap.IsClosable.closureIsClosable :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
f.IsClosable → f.closure.IsClosable
This theorem states that if a linear map `f` from a topological vector space `E` to another topological vector space `F` over a commutative ring `R` is closable, then the closure of `f` is also closable. Closability here refers to the property that the graph of a linear operator can be extended to the graph of a closed operator. This is under the condition that `E` and `F` are both additive commutative groups, and they along with `R` are equipped with a topology such that the addition operation and scalar multiplication are continuous.
More concisely: If `f` is a closable linear map between topological vector spaces `E` and `F` over a commutative ring `R`, where `E` and `F` are additive commutative groups with continuous addition and scalar multiplication, then the closure of `f` is also a closable linear map.
|
LinearPMap.IsClosed.isClosable
theorem LinearPMap.IsClosed.isClosable :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, f.IsClosed → f.IsClosable
This theorem states that for all types R, E, and F, where R is a commutative ring, E and F are additive commutative groups, and both E and F are R-modules. If E and F are topological spaces, addition in E and F is continuous, and scalar multiplication by elements of R in E and F is also continuous, then given a linear map from E to F that is closed, this map is also closable.
More concisely: Given a commutative ring R, additive commutative groups E and F as R-modules, topological spaces with continuous addition and scalar multiplication, and a closed linear map from E to F between these structures, this map is closable.
|
LinearPMap.closureHasCore
theorem LinearPMap.closureHasCore :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] (f : E →ₗ.[R] F), f.closure.HasCore f.domain
This theorem states that for every unbounded operator `f`, the submodule `f.domain` is a core of its closure. This holds irrespective of whether `f` is closable or not, due to the definition of the closure. Here, the operator `f` is a linear map from `E` to `F`, where `E` and `F` are topological vector spaces over a commutative ring `R`. The theorem asserts that the closure of the operator, which is the smallest closed set containing the range of `f`, has `f.domain` as its core. The core of a closure is a subset such that closing the core produces the closure.
More concisely: For every unbounded linear map `f` between topological vector spaces `E` and `F` over a commutative ring `R`, the domain of `f` is a core of its closure.
|
LinearPMap.inverse_isClosable_iff
theorem LinearPMap.inverse_isClosable_iff :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
LinearMap.ker f.toFun = ⊥ → f.IsClosable → (f.inverse.IsClosable ↔ LinearMap.ker f.closure.toFun = ⊥)
This theorem states that for all types `R`, `E`, and `F` where `R` is a commutative ring, `E` and `F` are additive commutative group with an `R`-module structure, and `E`, `F`, and `R` are topological spaces. Also, the operations of addition in `E` and `F`, and scalar multiplication in `R`, `E`, and `F` are continuous. Given a linear map `f` from `E` to `F`, if the kernel of `f` is trivial and `f` is closable, then the inverse of `f` is closable if and only if the kernel of the closure of `f` is trivial.
More concisely: If `f` is a continuous linear map between two topological commutative `R`-modules `E` and `F` over a commutative ring `R`, with trivial kernel and closable range, then `f` has a closable inverse if and only if the kernel of its closure is trivial.
|
LinearPMap.IsClosable.existsUnique
theorem LinearPMap.IsClosable.existsUnique :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
f.IsClosable → ∃! f', f.graph.topologicalClosure = f'.graph
This theorem states that, given a commutative ring `R` and additively commutative groups `E` and `F` that are also `R`-modules and topological spaces, if `f` is a linear map from `E` to `F` that is closable, then there exists a unique `f'` such that the topological closure of the graph of `f` is equal to the graph of `f'`. The operations of addition and scalar multiplication in the spaces `E` and `F` are assumed to be continuous.
More concisely: Given a commutative ring `R`, additively commutative `R`-modules and topological spaces `E` and `F` with continuous addition and scalar multiplication, a linear and closable map `f` from `E` to `F`, there exists a unique linear map `f'` such that the graph of `f'` is the topological closure of the graph of `f`.
|
LinearPMap.IsClosable.closure_isClosed
theorem LinearPMap.IsClosable.closure_isClosed :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
f.IsClosable → f.closure.IsClosed
This theorem states that if a linear map `f` from a space `E` to a space `F` over a commutative ring `R` is closable, then the closure of `f` is a closed set. Here, `E` and `F` are both additive commutative groups and modules over `R`, and they, along with `R`, are equipped with topological structure. Also, addition in `E` and `F` and scalar multiplication in `E` and `F` are assumed to be continuous.
More concisely: If `f` is a closable linear map from a topological additive commutative group and module `E` over a commutative ring `R` to a topological additive commutative group and module `F`, then the closure of `f(A)` is a closed set for any closed set `A` in `E`.
|
LinearPMap.IsClosable.leIsClosable
theorem LinearPMap.IsClosable.leIsClosable :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f g : E →ₗ.[R] F},
f.IsClosable → g ≤ f → g.IsClosable
This theorem states that given two linear maps `f` and `g` from a vector space `E` to a vector space `F` over a commutative ring `R`, if `f` is closable and `g` is not larger than `f` (in the partial order sense), then `g` is also closable. Here, the vector spaces `E` and `F` are equipped with topological structures, and the scalar multiplication and addition are continuous operations. Being "closable" refers to the property of a map that it can be extended to the closure of its domain.
More concisely: If `f` is a closable linear map from a topological vector space `E` to another topological vector space `F` over a commutative ring `R`, and `g` is a linear map from `E` to `F` that is not larger than `f`, then `g` is also closable.
|
LinearPMap.inverse_closure
theorem LinearPMap.inverse_closure :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
LinearMap.ker f.toFun = ⊥ →
f.IsClosable → LinearMap.ker f.closure.toFun = ⊥ → f.inverse.closure = f.closure.inverse
This theorem states that if a linear map `f`, from a topological module `E` to another topological module `F` over a commutative ring `R`, is both invertible and closable, then the operations of taking the closure and taking the inverse commute. In other words, if the kernel of the function defined by `f` is trivial (i.e., only contains the zero element) and `f` is closable, if the closure of `f` also has a trivial kernel, then the closure of the inverse of `f` is equal to the inverse of the closure of `f`. All the operations are defined in the context of topological spaces, where addition and scalar multiplication are continuous operations.
More concisely: If a continuous, invertible linear map between topological modules over a commutative ring has a trivial kernel and is closable, then the closure of its inverse is equal to the inverse of the closure.
|
LinearPMap.closure_inverse_graph
theorem LinearPMap.closure_inverse_graph :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F},
LinearMap.ker f.toFun = ⊥ →
f.IsClosable →
LinearMap.ker f.closure.toFun = ⊥ → f.closure.inverse.graph = f.inverse.graph.topologicalClosure
This theorem states that for any commutative ring `R` and additive commutative groups `E` and `F` with `E` and `F` being `R`-modules and topological spaces, and `E` and `F` having continuous addition and scalar multiplication over `R`, if a linear map `f` from `E` to `F` has its kernel being the trivial subspace and is closable, and the closure of `f` also has its kernel being the trivial subspace, then the graph of the inverse function of the closure of `f` is equivalent to the topological closure of the graph of the inverse function of `f`.
More concisely: If `f` is a continuous linear map between commutative `R`-modules and topological spaces `E` and `F`, with trivial kernel and closed graph, then the closure of `f`'s graph is equivalent to the graph of `f`'s inverse.
|
LinearPMap.le_closure
theorem LinearPMap.le_closure :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
[inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F] (f : E →ₗ.[R] F), f ≤ f.closure
This theorem states that for any linear partially defined map `f`, from a topological module `E` over a commutative ring `R` to another topological module `F` over the same ring `R`, `f` is contained within its closure. The modules `E` and `F` are equipped with a topological space structure and a module structure over `R`, which is also equipped with a topological space structure. The addition operations on `E` and `F` are continuous, as is the scalar multiplication by elements of `R`.
More concisely: Given a linear partially defined map `f` from topological modules `E` and `F` over a commutative ring `R` with continuous addition and scalar multiplication operations, `f` is contained in the closure of its graph.
|