Partially defined linear maps #
A linear_pmap R E F or E →ₗ.[R] 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.
Moreover, we define
linear_pmap.graphis 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, linear_pmap.Sup implies that every chain of linear_pmaps
is bounded above.
They are also the basis for the theory of unbounded 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 or E →ₗ.[R] F is a linear map from a submodule of E to F.
Instances for linear_pmap
@[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] :
@[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 : E →ₗ.[R] 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 : E →ₗ.[R] F) :
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) :
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) :
@[simp]
theorem
linear_pmap.mk_span_singleton'_apply_self
{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)
(h : x ∈ (linear_pmap.mk_span_singleton' x y H).domain) :
⇑(linear_pmap.mk_span_singleton' x y H) ⟨x, h⟩ = y
@[reducible]
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) :
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) ⟨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) :
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) :
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_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] :
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 : E →ₗ.[R] 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 : E →ₗ.[R] 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] :
@[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] :
@[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] :
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 (E →ₗ.[R] 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] :
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 : E →ₗ.[R] 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 : E →ₗ.[R] F)
(h : ∀ (x : ↥(f.domain)) (y : ↥(g.domain)), ↑x = ↑y → ⇑f 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.
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 : E →ₗ.[R] 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) :
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 : E →ₗ.[R] 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.
@[protected, instance]
def
linear_pmap.has_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]
{M : Type u_5}
[monoid M]
[distrib_mul_action M F]
[smul_comm_class R M F] :
theorem
linear_pmap.smul_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]
{M : Type u_5}
[monoid M]
[distrib_mul_action M F]
[smul_comm_class R M F]
(a : M)
(f : E →ₗ.[R] F)
(x : ↥((a • f).domain)) :
@[simp]
theorem
linear_pmap.coe_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]
{M : Type u_5}
[monoid M]
[distrib_mul_action M F]
[smul_comm_class R M F]
(a : M)
(f : E →ₗ.[R] F) :
@[protected, instance]
def
linear_pmap.smul_comm_class
{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]
{M : Type u_5}
{N : Type u_6}
[monoid M]
[distrib_mul_action M F]
[smul_comm_class R M F]
[monoid N]
[distrib_mul_action N F]
[smul_comm_class R N F]
[smul_comm_class M N F] :
smul_comm_class M N (E →ₗ.[R] F)
@[protected, instance]
def
linear_pmap.is_scalar_tower
{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]
{M : Type u_5}
{N : Type u_6}
[monoid M]
[distrib_mul_action M F]
[smul_comm_class R M F]
[monoid N]
[distrib_mul_action N F]
[smul_comm_class R N F]
[has_smul M N]
[is_scalar_tower M N F] :
is_scalar_tower M N (E →ₗ.[R] F)
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 : E →ₗ.[K] F)
(x : E)
(y : F)
(hx : x ∉ f.domain) :
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 : E →ₗ.[K] 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 : E →ₗ.[K] 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 (E →ₗ.[R] 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
- linear_pmap.Sup c hc = {domain := has_Sup.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 (E →ₗ.[R] F)}
(hc : directed_on has_le.le c)
{f : E →ₗ.[R] 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 (E →ₗ.[R] F)}
(hc : directed_on has_le.le c)
{g : E →ₗ.[R] F}
(hg : ∀ (f : E →ₗ.[R] F), f ∈ c → f ≤ g) :
linear_pmap.Sup c hc ≤ g
@[protected]
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]
{c : set (E →ₗ.[R] F)}
(hc : directed_on has_le.le c)
{l : E →ₗ.[R] F}
(hl : l ∈ c)
(x : ↥(l.domain)) :
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.
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 : E →ₗ.[R] F) :
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 : E →ₗ.[R] 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 : E →ₗ.[R] F)
(p : submodule R F)
(H : ∀ (x : ↥(f.domain)), ⇑f x ∈ 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 : F →ₗ.[R] G)
(f : E →ₗ.[R] F)
(H : ∀ (x : ↥(f.domain)), ⇑f x ∈ g.domain) :
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 : E →ₗ.[R] G)
(g : F →ₗ.[R] 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 : E →ₗ.[R] G)
(g : F →ₗ.[R] G)
(x : ↥((f.coprod g).domain)) :
def
linear_pmap.dom_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 : E →ₗ.[R] F)
(S : submodule R E) :
Restrict a partially defined linear map to a submodule of E contained in f.domain.
Equations
- f.dom_restrict S = {domain := S ⊓ f.domain, to_fun := f.to_fun.comp (submodule.of_le _)}
@[simp]
theorem
linear_pmap.dom_restrict_domain
{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)
{S : submodule R E} :
(f.dom_restrict S).domain = S ⊓ f.domain
theorem
linear_pmap.dom_restrict_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 : E →ₗ.[R] F}
{S : submodule R E} :
f.dom_restrict S ≤ f
Graph #
def
linear_pmap.graph
{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) :
The graph of a linear_pmap viewed as a submodule on E × F.
Equations
- f.graph = submodule.map (f.domain.subtype.prod_map linear_map.id) f.to_fun.graph
theorem
linear_pmap.mem_graph
{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)
(x : ↥(f.domain)) :
The tuple (x, f x) is contained in the graph of f.
theorem
linear_pmap.smul_graph
{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]
{M : Type u_5}
[monoid M]
[distrib_mul_action M F]
[smul_comm_class R M F]
(f : E →ₗ.[R] F)
(z : M) :
(z • f).graph = submodule.map (linear_map.id.prod_map (z • linear_map.id)) f.graph
The graph of z • f as a pushforward.
theorem
linear_pmap.neg_graph
{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) :
(-f).graph = submodule.map (linear_map.id.prod_map (-linear_map.id)) f.graph
The graph of -f as a pushforward.
theorem
linear_pmap.mem_graph_snd_inj
{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)
{x y : E}
{x' y' : F}
(hx : (x, x') ∈ f.graph)
(hy : (y, y') ∈ f.graph)
(hxy : x = y) :
x' = y'
theorem
linear_pmap.graph_fst_eq_zero_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]
(f : E →ₗ.[R] F)
{x : E}
{x' : F}
(h : (x, x') ∈ f.graph)
(hx : x = 0) :
x' = 0
The property that f 0 = 0 in terms of the graph.
theorem
linear_pmap.mem_domain_iff
{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}
{x : E} :
theorem
linear_pmap.mem_domain_of_mem_graph
{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}
{x : E}
{y : F}
(h : (x, y) ∈ f.graph) :
theorem
linear_pmap.mem_range_iff
{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}
{y : F} :
theorem
linear_pmap.le_of_le_graph
{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 : E →ₗ.[R] F}
(h : f.graph ≤ g.graph) :
f ≤ g
theorem
linear_pmap.le_graph_of_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 : E →ₗ.[R] F}
(h : f ≤ g) :
theorem
linear_pmap.le_graph_iff
{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 : E →ₗ.[R] F} :
theorem
linear_pmap.eq_of_eq_graph
{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 : E →ₗ.[R] F}
(h : f.graph = g.graph) :
f = g
theorem
submodule.exists_unique_from_graph
{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 : submodule R (E × F)}
(hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0)
{a : E}
(ha : a ∈ submodule.map (linear_map.fst R E F) g) :
∃! (b : F), (a, b) ∈ g
noncomputable
def
submodule.val_from_graph
{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 : submodule R (E × F)}
(hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0)
{a : E}
(ha : a ∈ submodule.map (linear_map.fst R E F) g) :
F
Auxiliary definition to unfold the existential quantifier.
Equations
- submodule.val_from_graph hg ha = _.some
theorem
submodule.val_from_graph_mem
{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 : submodule R (E × F)}
(hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0)
{a : E}
(ha : a ∈ submodule.map (linear_map.fst R E F) g) :
(a, submodule.val_from_graph hg ha) ∈ g
noncomputable
def
submodule.to_linear_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 : submodule R (E × F))
(hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0) :
Define a linear_pmap from its graph.
Equations
- g.to_linear_pmap hg = {domain := submodule.map (linear_map.fst R E F) g, to_fun := {to_fun := λ (x : ↥(submodule.map (linear_map.fst R E F) g)), submodule.val_from_graph hg _, map_add' := _, map_smul' := _}}
theorem
submodule.mem_graph_to_linear_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 : submodule R (E × F))
(hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0)
(x : ↥(submodule.map (linear_map.fst R E F) g)) :
(x.val, ⇑(g.to_linear_pmap hg) x) ∈ g
@[simp]
theorem
submodule.to_linear_pmap_graph_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]
(g : submodule R (E × F))
(hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0) :
(g.to_linear_pmap hg).graph = g