mathlib documentation

linear_algebra.linear_pmap

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:

Moreover, we define

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] :
has_coe_to_fun (E →ₗ.[R] F) (λ (f : E →ₗ.[R] F), (f.domain) → 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 : E →ₗ.[R] F) (x : (f.domain)) :
(f.to_fun) x = f x
@[ext]
theorem linear_pmap.ext {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 = g.domain) (h' : ∀ ⦃x : (f.domain)⦄ ⦃y : (g.domain)⦄, x = yf x = g y) :
f = g
@[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) :
f 0 = 0
theorem linear_pmap.ext_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} :
f = g ∃ (domain_eq : f.domain = g.domain), ∀ ⦃x : (f.domain)⦄ ⦃y : (g.domain)⦄, x = yf x = g y
theorem linear_pmap.ext' {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] {s : submodule R E} {f g : s →ₗ[R] F} (h : f = g) :
{domain := s, to_fun := f} = {domain := s, to_fun := g}
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 : E →ₗ.[R] 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 : E →ₗ.[R] 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 : E →ₗ.[R] 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 : E →ₗ.[R] 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
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 = 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) :
@[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 = 0c y = 0) (h : x (linear_pmap.mk_span_singleton' x y H).domain) :
@[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
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) :
@[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) :
E × F →ₗ.[R] 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')) :
@[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) :
E × F →ₗ.[R] 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')) :
@[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] :
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 : E →ₗ.[R] F) (x : ((-f).domain)) :
(-f) x = -f x
@[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] :
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 : 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) :

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
@[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] :
Equations
@[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] :
Equations
@[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] :
Equations
@[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] :
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 : 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 = 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 : E →ₗ.[R] 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 : E →ₗ.[R] 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
@[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 : E →ₗ.[R] F) (h : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) :
f f.sup g h
@[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 : E →ₗ.[R] F) (h : ∀ (x : (f.domain)) (y : (g.domain)), x = yf x = g y) :
g f.sup g h
@[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] {f g h : E →ₗ.[R] 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 : E →ₗ.[R] 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.

@[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] :
Equations
@[simp]
theorem linear_pmap.smul_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] {M : Type u_5} [monoid M] [distrib_mul_action M F] [smul_comm_class R M F] (a : M) (f : E →ₗ.[R] F) :
(a f).domain = f.domain
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)) :
(a f) x = a f x
@[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) :
(a f) = a 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] :
@[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] :
@[protected, instance]
def linear_pmap.mul_action {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] :
Equations
@[protected, instance]
def linear_pmap.has_vadd {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.vadd_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) (g : E →ₗ.[R] F) :
theorem linear_pmap.vadd_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) (g : E →ₗ.[R] F) (x : ((f +ᵥ g).domain)) :
(f +ᵥ g) x = f x + g x
@[simp]
theorem linear_pmap.coe_vadd {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) (g : E →ₗ.[R] F) :
@[protected, instance]
def linear_pmap.add_action {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
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
@[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) :
@[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) :
(f.sup_span_singleton x y hx) x' + c x, _⟩ = f x', hx'⟩ + c y
@[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
@[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) :
@[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 cf 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)) :
(linear_pmap.Sup c hc) x, _⟩ = l x
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 : E →ₗ.[R] 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 : E →ₗ.[R] 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 : E →ₗ.[R] 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 : F →ₗ.[R] G) (f : E →ₗ.[R] 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 : E →ₗ.[R] G) (g : F →ₗ.[R] G) :
E × 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.

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 : E →ₗ.[R] G) (g : F →ₗ.[R] G) (x : ((f.coprod g).domain)) :
(f.coprod g) x = f x.fst, _⟩ + g x.snd, _⟩
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
@[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} :
theorem linear_pmap.dom_restrict_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} {S : submodule R E} ⦃x : (S f.domain) ⦃y : (f.domain)⦄ (h : x = y) :
(f.dom_restrict S) x = f y
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} :

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) :
submodule R (E × F)

The graph of a linear_pmap viewed as a submodule on E × F.

Equations
theorem linear_pmap.mem_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 : E →ₗ.[R] F) {x : E × F} :
x f.graph ∃ (y : (f.domain)), (y, f y) = x
@[simp]
theorem linear_pmap.mem_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 : E →ₗ.[R] F) {x : E × F} :
x f.graph ∃ (y : (f.domain)), y = x.fst f y = x.snd
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)) :
(x, f x) f.graph

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

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

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.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 × F} (hx : x f.graph) (hy : y f.graph) (hxy : x.fst = y.fst) :
x.snd = y.snd
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} :
x f.domain ∃ (y : F), (x, y) f.graph
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.image_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} {y : F} (hx : x f.domain) :
y = f x, hx⟩ (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} :
y set.range f ∃ (x : E), (x, y) f.graph
theorem linear_pmap.mem_domain_iff_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) {x : E} :
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 gx.fst = 0x.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 gx.fst = 0x.snd = 0) {a : E} (ha : a submodule.map (linear_map.fst R E F) g) :
F

Auxiliary definition to unfold the existential quantifier.

Equations
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 gx.fst = 0x.snd = 0) {a : E} (ha : a submodule.map (linear_map.fst R E F) 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 gx.fst = 0x.snd = 0) :

Define a linear_pmap from its graph.

Equations
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 gx.fst = 0x.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 gx.fst = 0x.snd = 0) :