Partially defined linear maps #
A LinearPMap R E F
or E →ₗ.[R] F
is a linear map from a submodule of E
to F
.
We define a SemilatticeInf
with OrderBot
instance on this, and define three operations:
mkSpanSingleton
defines a partial linear map defined on the span of a singleton.sup
takes two partial linear mapsf
,g
that agree on the intersection of their domains, and returns the unique partial linear map onf.domain ⊔ g.domain
that extends bothf
andg
.sSup
takes aDirectedOn (· ≤ ·)
set of partial linear maps, and returns the unique partial linear map on thesSup
of their domains that extends all these maps.
Moreover, we define
LinearPMap.graph
is the graph of the partial linear map viewed as a submodule ofE × F
.
Partially defined maps are currently used in Mathlib
to prove Hahn-Banach theorem
and its variations. Namely, LinearPMap.sSup
implies that every chain of LinearPMap
s
is bounded above.
They are also the basis for the theory of unbounded operators.
A LinearPMap R E F
or E →ₗ.[R] F
is a linear map from a submodule of E
to F
.
- domain : Submodule R E
Instances For
Equations
Instances For
The unique LinearPMap
on R ∙ x
that sends x
to y
. This version works for modules
over rings, and requires a proof of ∀ c, c • x = 0 → c • y = 0
.
Equations
Instances For
The unique LinearPMap
on span R {x}
that sends a non-zero vector x
to y
.
This version works for modules over division rings.
Equations
Instances For
Projection to the first coordinate as a LinearPMap
Equations
Instances For
Projection to the second coordinate as a LinearPMap
Equations
Instances For
Equations
Given two partial linear maps f
, g
, the set of points x
such that
both f
and g
are defined at x
and f x = g x
form a submodule.
Equations
Instances For
Equations
Equations
Equations
Equations
Given two partial linear maps that agree on the intersection of their domains,
f.sup g h
is the unique partial linear map on f.domain ⊔ g.domain
that agrees
with f
and g
.
Equations
Instances For
Hypothesis for LinearPMap.sup
holds, if f.domain
is disjoint with g.domain
.
Algebraic operations #
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Extend a LinearPMap
to f.domain ⊔ K ∙ x
.
Equations
Instances For
Equations
Instances For
Restrict a linear map to a submodule, reinterpreting the result as a LinearPMap
.
Equations
Instances For
Compose a linear map with a LinearPMap
Equations
Instances For
Restrict codomain of a LinearPMap
Equations
Instances For
Compose two LinearPMap
s
Equations
Instances For
f.coprod g
is the partially defined linear map defined on f.domain × g.domain
,
and sending p
to f p.1 + g p.2
.
Equations
Instances For
Graph #
The graph of a LinearPMap
viewed as a submodule on E × F
.
Equations
Instances For
The graph of z • f
as a pushforward.
The graph of -f
as a pushforward.
Auxiliary definition to unfold the existential quantifier.
Equations
Instances For
Define a LinearMap
from its graph.
Helper definition for LinearPMap
.
Equations
Instances For
Define a LinearPMap
from its graph.
In the case that the submodule is not a graph of a LinearPMap
then the underlying linear map
is just the zero map.
Equations
Instances For
The inverse of a LinearPMap
.
Equations
Instances For
The graph of the inverse generates a LinearPMap
.