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 with order_bot instance on this this, and define three operations:
mk_span_singletondefines a partial linear map defined on the span of a singleton.suptakes two partial linear mapsf,gthat agree on the intersection of their domains, and returns the unique partial linear map onf.domain ⊔ g.domainthat extends bothfandg.Suptakes adirected_on (≤)set of partial linear maps, and returns the unique partial linear map on theSupof 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)
A linear_pmap R E F is a linear map from a submodule of E to F.
@[protected, 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) (λ (f : linear_pmap R E F), ↥(f.domain) → F)
Equations
- linear_pmap.has_coe_to_fun = {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)) :
@[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) :
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)) :
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)) :
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)) :
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)) :
noncomputable
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 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 := have H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → c₁ • y = c₂ • y, from _, {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) :
noncomputable
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 _
theorem
linear_pmap.mk_span_singleton_apply'
(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}
(hx : x ≠ 0)
(y : F) :
⇑((linear_pmap.mk_span_singleton x y hx).to_fun) ⟨x, _⟩ = y
@[protected]
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
@[protected]
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
@[protected, 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)
@[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)) :
@[protected, 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)
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) :
submodule 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.
@[protected, 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 _)}}
@[protected, 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)
@[protected, 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
@[protected, instance]
def
linear_pmap.semilattice_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] :
semilattice_inf (linear_pmap R E F)
Equations
- linear_pmap.semilattice_inf = {inf := has_inf.inf linear_pmap.has_inf, le := has_le.le linear_pmap.has_le, lt := partial_order.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
def
linear_pmap.order_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] :
order_bot (linear_pmap R E F)
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] :
@[protected]
noncomputable
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.
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
Hypothesis for linear_pmap.sup holds, if f.domain is disjoint with g.domain.
noncomputable
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) :
linear_pmap K E F
Extend a linear_pmap to f.domain ⊔ K ∙ x.
Equations
- f.sup_span_singleton x y hx = f.sup (linear_pmap.mk_span_singleton x y _) _
@[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) :
(f.sup_span_singleton x y hx).domain = f.domain ⊔ submodule.span K {x}
@[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) :
@[protected]
noncomputable
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 _}
@[protected]
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
@[protected]
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.
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
@[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)) :
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
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.
@[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)) :