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) :
(∀ (c : R), c x = 0c y = 0)linear_pmap R E F

The unique linear_pmap on span 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) :
F → x 0linear_pmap K E F

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] :
submodule R Esubmodule R Flinear_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] :
submodule R Esubmodule R Flinear_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} :
f gf.domain = g.domainf = 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] :
linear_pmap R E Flinear_pmap R E Fsubmodule R E

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} :
f.domain f.eq_locus gf 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) :
(∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y)linear_pmap R E F

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)) :
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) :
f hg hf.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)) :
x = yf x = g y

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

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)) :

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} :
f cf linear_pmap.Sup c hc

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} :
(∀ (f : linear_pmap R E F), f cf g)linear_pmap.Sup c hc 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] :
(E →ₗ[R] F)submodule R Elinear_pmap R E F

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] :
(F →ₗ[R] G)linear_pmap R E Flinear_pmap R E G

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) :
(∀ (x : (f.domain)), f x p)linear_pmap R E 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) :
(∀ (x : (f.domain)), f x g.domain)linear_pmap R E G

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] :
linear_pmap R E Glinear_pmap R F Glinear_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, _⟩