mathlib documentation

linear_algebra.linear_pmap

Partially defined linear maps #

A linear_pmap R E F is a linear map from a submodule of E to F. We define a semilattice_inf_bot instance on this this, and define three operations:

Partially defined maps are currently used in mathlib to prove Hahn-Banach theorem and its variations. Namely, linear_pmap.Sup implies that every chain of linear_pmaps is bounded above.

Another possible use (not yet in mathlib) would be the theory of unbounded linear operators.

structure linear_pmap (R : Type u) [ring R] (E : Type v) [add_comm_group E] [module R E] (F : Type w) [add_comm_group F] [module R F] :
Type (max v w)

A linear_pmap R E F is a linear map from a submodule of E to F.

@[instance]
def linear_pmap.has_coe_to_fun {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
@[simp]
theorem linear_pmap.to_fun_eq_coe {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (x : (f.domain)) :
(f.to_fun) x = f x
@[simp]
theorem linear_pmap.map_zero {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) :
f 0 = 0
theorem linear_pmap.map_add {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (x y : (f.domain)) :
f (x + y) = f x + f y
theorem linear_pmap.map_neg {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (x : (f.domain)) :
f (-x) = -f x
theorem linear_pmap.map_sub {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (x y : (f.domain)) :
f (x - y) = f x - f y
theorem linear_pmap.map_smul {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (c : R) (x : (f.domain)) :
f (c x) = c f x
@[simp]
theorem linear_pmap.mk_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (p : submodule R E) (f : p →ₗ[R] F) (x : p) :
{domain := p, to_fun := f} x = f x
def linear_pmap.mk_span_singleton' {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) :

The unique linear_pmap 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
@[simp]
theorem linear_pmap.domain_mk_span_singleton {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) :
@[simp]
theorem linear_pmap.mk_span_singleton_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (x : E) (y : F) (H : ∀ (c : R), c x = 0c y = 0) (c : R) (h : c x (linear_pmap.mk_span_singleton' x y H).domain) :
def linear_pmap.mk_span_singleton {K : Type u_1} {E : Type u_2} {F : Type u_3} [division_ring K] [add_comm_group E] [module K E] [add_comm_group F] [module K F] (x : E) (y : F) (hx : x 0) :

The unique linear_pmap on span R {x} that sends a non-zero vector x to y. This version works for modules over division rings.

Equations
def linear_pmap.fst {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (p : submodule R E) (p' : submodule R F) :
linear_pmap R (E × F) E

Projection to the first coordinate as a linear_pmap

Equations
@[simp]
theorem linear_pmap.fst_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (p : submodule R E) (p' : submodule R F) (x : (p.prod p')) :
def linear_pmap.snd {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (p : submodule R E) (p' : submodule R F) :
linear_pmap R (E × F) F

Projection to the second coordinate as a linear_pmap

Equations
@[simp]
theorem linear_pmap.snd_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (p : submodule R E) (p' : submodule R F) (x : (p.prod p')) :
@[instance]
def linear_pmap.has_neg {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
@[simp]
theorem linear_pmap.neg_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (x : ((-f).domain)) :
(-f) x = -f x
@[instance]
def linear_pmap.has_le {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
theorem linear_pmap.eq_of_le_of_domain_eq {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {f g : linear_pmap R E F} (hle : f g) (heq : f.domain = g.domain) :
f = g
def linear_pmap.eq_locus {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f g : linear_pmap R E F) :

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
@[instance]
def linear_pmap.has_inf {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
@[instance]
def linear_pmap.has_bot {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
@[instance]
def linear_pmap.inhabited {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
@[instance]
def linear_pmap.semilattice_inf_bot {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
Equations
theorem linear_pmap.le_of_eq_locus_ge {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {f g : linear_pmap R E F} (H : f.domain f.eq_locus g) :
f g
theorem linear_pmap.domain_mono {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] :
def linear_pmap.sup {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f g : linear_pmap R E F) (h : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) :

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
@[simp]
theorem linear_pmap.domain_sup {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f g : linear_pmap R E F) (h : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) :
(f.sup g h).domain = f.domain g.domain
theorem linear_pmap.sup_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {f g : linear_pmap R E F} (H : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) (x : (f.domain)) (y : (g.domain)) (z : ((f.sup g H).domain)) (hz : x + y = z) :
(f.sup g H) z = f x + g y
theorem linear_pmap.left_le_sup {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f g : linear_pmap R E F) (h : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) :
f f.sup g h
theorem linear_pmap.right_le_sup {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f g : linear_pmap R E F) (h : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) :
g f.sup g h
theorem linear_pmap.sup_le {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {f g h : linear_pmap R E F} (H : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) (fh : f h) (gh : g h) :
f.sup g H h
theorem linear_pmap.sup_h_of_disjoint {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f g : linear_pmap R E F) (h : disjoint f.domain g.domain) (x : (f.domain)) (y : (g.domain)) (hxy : x = y) :
f x = g y

Hypothesis for linear_pmap.sup holds, if f.domain is disjoint with g.domain.

def linear_pmap.sup_span_singleton {E : Type u_2} [add_comm_group E] {F : Type u_3} [add_comm_group F] {K : Type u_5} [division_ring K] [module K E] [module K F] (f : linear_pmap K E F) (x : E) (y : F) (hx : x f.domain) :

Extend a linear_pmap to f.domain ⊔ K ∙ x.

Equations
@[simp]
theorem linear_pmap.domain_sup_span_singleton {E : Type u_2} [add_comm_group E] {F : Type u_3} [add_comm_group F] {K : Type u_5} [division_ring K] [module K E] [module K F] (f : linear_pmap K E F) (x : E) (y : F) (hx : x f.domain) :
@[simp]
theorem linear_pmap.sup_span_singleton_apply_mk {E : Type u_2} [add_comm_group E] {F : Type u_3} [add_comm_group F] {K : Type u_5} [division_ring K] [module K E] [module K F] (f : linear_pmap K E F) (x : E) (y : F) (hx : x f.domain) (x' : E) (hx' : x' f.domain) (c : K) :
(f.sup_span_singleton x y hx) x' + c x, _⟩ = f x', hx'⟩ + c y
def linear_pmap.Sup {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (c : set (linear_pmap R E F)) (hc : directed_on has_le.le c) :

Glue a collection of partially defined linear maps to a linear map defined on Sup of these submodules.

Equations
theorem linear_pmap.le_Sup {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {c : set (linear_pmap R E F)} (hc : directed_on has_le.le c) {f : linear_pmap R E F} (hf : f c) :
theorem linear_pmap.Sup_le {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {c : set (linear_pmap R E F)} (hc : directed_on has_le.le c) {g : linear_pmap R E F} (hg : ∀ (f : linear_pmap R E F), f cf g) :
def linear_map.to_pmap {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : E →ₗ[R] F) (p : submodule R E) :

Restrict a linear map to a submodule, reinterpreting the result as a linear_pmap.

Equations
@[simp]
theorem linear_map.to_pmap_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : E →ₗ[R] F) (p : submodule R E) (x : p) :
(f.to_pmap p) x = f x
def linear_map.comp_pmap {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] (g : F →ₗ[R] G) (f : linear_pmap R E F) :

Compose a linear map with a linear_pmap

Equations
@[simp]
theorem linear_map.comp_pmap_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] (g : F →ₗ[R] G) (f : linear_pmap R E F) (x : ((g.comp_pmap f).domain)) :
(g.comp_pmap f) x = g (f x)
def linear_pmap.cod_restrict {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : linear_pmap R E F) (p : submodule R F) (H : ∀ (x : (f.domain)), f x p) :

Restrict codomain of a linear_pmap

Equations
def linear_pmap.comp {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] (g : linear_pmap R F G) (f : linear_pmap R E F) (H : ∀ (x : (f.domain)), f x g.domain) :

Compose two linear_pmaps

Equations
def linear_pmap.coprod {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] (f : linear_pmap R E G) (g : linear_pmap R F G) :
linear_pmap R (E × F) G

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
@[simp]
theorem linear_pmap.coprod_apply {R : Type u_1} [ring R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] {G : Type u_4} [add_comm_group G] [module R G] (f : linear_pmap R E G) (g : linear_pmap R F G) (x : ((f.coprod g).domain)) :
(f.coprod g) x = f x.fst, _⟩ + g x.snd, _⟩