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:

mk_span_singleton defines a partial linear map defined on the span of a singleton.
sup takes two partial linear maps f, g that agree on the intersection of their domains, and returns the unique partial linear map on f.domain ⊔ g.domain that extends both f and g.
Sup takes a directed_on (≤) set of partial linear maps, and returns the unique partial linear map on the Sup of their domains that extends all these maps.

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)

domain : submodule R E
to_fun : ↥(c.domain) →ₗ[R] F

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

has_coe_to_fun (linear_pmap R E F)

Equations

linear_pmap.has_coe_to_fun = {F := λ (f : linear_pmap R E F), ↥(f.domain) → F, coe := λ (f : linear_pmap R E F), ⇑(f.to_fun)}

@[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 = 0 → c • 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

linear_pmap.mk_span_singleton' x y H = {domain := submodule.span R {x}, to_fun := {to_fun := λ (z : ↥(submodule.span R {x})), classical.some _ • y, map_add' := _, map_smul' := _}}

@[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 = 0 → c • y = 0) :

(linear_pmap.mk_span_singleton' x y H).domain = submodule.span R {x}

@[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 = 0 → c • y = 0) (c : R) (h : c • x ∈ (linear_pmap.mk_span_singleton' x y H).domain) :

⇑(linear_pmap.mk_span_singleton' x y H) ⟨c • x, h⟩ = c • y

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

linear_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

linear_pmap.mk_span_singleton x y hx = linear_pmap.mk_span_singleton' x y _

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

linear_pmap.fst p p' = {domain := p.prod p', to_fun := (linear_map.fst R E F).comp (p.prod p').subtype}

@[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')) :

⇑(linear_pmap.fst p p') x = ↑x.fst

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

linear_pmap.snd p p' = {domain := p.prod p', to_fun := (linear_map.snd R E F).comp (p.prod p').subtype}

@[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')) :

⇑(linear_pmap.snd p p') x = ↑x.snd

@[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] :

has_neg (linear_pmap R E F)

Equations

linear_pmap.has_neg = {neg := λ (f : linear_pmap R E F), {domain := f.domain, to_fun := -f.to_fun}}

@[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] :

has_le (linear_pmap R E F)

Equations

linear_pmap.has_le = {le := λ (f g : linear_pmap R E F), f.domain ≤ g.domain ∧ ∀ ⦃x : ↥(f.domain)⦄ ⦃y : ↥(g.domain)⦄, ↑x = ↑y → ⇑f x = ⇑g y}

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

f.eq_locus g = {carrier := {x : E | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ⇑f ⟨x, hf⟩ = ⇑g ⟨x, hg⟩}, zero_mem' := _, add_mem' := _, smul_mem' := _}

@[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] :

has_inf (linear_pmap R E F)

Equations

linear_pmap.has_inf = {inf := λ (f g : linear_pmap R E F), {domain := f.eq_locus g, to_fun := f.to_fun.comp (submodule.of_le _)}}

@[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] :

has_bot (linear_pmap R E F)

Equations

linear_pmap.has_bot = {bot := {domain := ⊥, to_fun := 0}}

@[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] :

inhabited (linear_pmap R E F)

Equations

linear_pmap.inhabited = {default := ⊥}

@[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] :

semilattice_inf_bot (linear_pmap R E F)

Equations

linear_pmap.semilattice_inf_bot = {bot := ⊥, le := has_le.le linear_pmap.has_le, lt := order_bot.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := has_inf.inf linear_pmap.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

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

strict_mono linear_pmap.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] (f g : linear_pmap R E F) (h : ∀ (x : ↥(f.domain)) (y : ↥(g.domain)), ↑x = ↑y → ⇑f 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

f.sup g h = {domain := f.domain ⊔ g.domain, to_fun := classical.some _}

@[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 = ↑y → ⇑f 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 = ↑y → ⇑f 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 = ↑y → ⇑f 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 = ↑y → ⇑f 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 = ↑y → ⇑f 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 {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) :

linear_pmap R E F

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

Equations

linear_pmap.Sup c hc = {domain := Sup (linear_pmap.domain '' c), to_fun := classical.some _}

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

f ≤ 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} (hg : ∀ (f : linear_pmap R E F), f ∈ c → f ≤ 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] (f : E →ₗ[R] F) (p : submodule R E) :

linear_pmap R E F

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

Equations

f.to_pmap p = {domain := p, to_fun := f.comp p.subtype}

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

linear_pmap R E G

Compose a linear map with a linear_pmap

Equations

g.comp_pmap f = {domain := f.domain, to_fun := g.comp f.to_fun}

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

linear_pmap R E ↥p

Restrict codomain of a linear_pmap

Equations

f.cod_restrict p H = {domain := f.domain, to_fun := linear_map.cod_restrict p f.to_fun H}

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

linear_pmap R E G

Compose two linear_pmaps

Equations

g.comp f H = g.to_fun.comp_pmap (f.cod_restrict g.domain H)

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

f.coprod g = {domain := f.domain.prod g.domain, to_fun := (f.comp (linear_pmap.fst f.domain g.domain) _).to_fun + (g.comp (linear_pmap.snd f.domain g.domain) _).to_fun}

@[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, _⟩