feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531)

This PR adds more lemmas about the graph of a partially defined linear map, in particular about scalar multiplication and negation of `linear_pmap`s as well as relating inequalities and equalities between the graph and the `linear_pmap`.

src/linear_algebra/linear_pmap.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Yury Kudryashov All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Moritz Doll
 -/
 import linear_algebra.basic
 import linear_algebra.prod
@@ -19,11 +19,14 @@ a `semilattice_inf` with `order_bot` instance on this this, and define three ope
 * `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.
 
+Moreover, we define
+* `linear_pmap.graph` is the graph of the partial linear map viewed as a submodule of `E × 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_pmap`s
 is bounded above.
+They are also the basis for the theory of unbounded operators.
 
-Another possible use (not yet in `mathlib`) would be the theory of unbounded linear operators.
 -/
 
 open set
@@ -478,6 +481,60 @@ by { cases x, simp_rw [mem_graph_iff', prod.mk.inj_iff] }
 lemma mem_graph (f : linear_pmap R E F) (x : domain f) : ((x : E), f x) ∈ f.graph :=
 by simp
 
+variables {M : Type*} [monoid M] [distrib_mul_action M F] [smul_comm_class R M F] (y : M)
+
+/-- The graph of `z • f` as a pushforward. -/
+lemma smul_graph (f : linear_pmap R E F) (z : M) :
+  (z • f).graph = f.graph.map (linear_map.id.prod_map (z • linear_map.id)) :=
+begin
+  ext x, cases x,
+  split; intros h,
+  { rw mem_graph_iff at h,
+    rcases h with ⟨y, hy, h⟩,
+    rw linear_pmap.smul_apply at h,
+    rw submodule.mem_map,
+    simp only [mem_graph_iff, linear_map.prod_map_apply, linear_map.id_coe, id.def,
+      linear_map.smul_apply, prod.mk.inj_iff, prod.exists, exists_exists_and_eq_and],
+    use [x_fst, y],
+    simp [hy, h] },
+  rw submodule.mem_map at h,
+  rcases h with ⟨x', hx', h⟩,
+  cases x',
+  simp only [linear_map.prod_map_apply, linear_map.id_coe, id.def, linear_map.smul_apply,
+    prod.mk.inj_iff] at h,
+  rw mem_graph_iff at hx' ⊢,
+  rcases hx' with ⟨y, hy, hx'⟩,
+  use y,
+  rw [←h.1, ←h.2],
+  simp[hy, hx'],
+end
+
+/-- The graph of `-f` as a pushforward. -/
+lemma neg_graph (f : linear_pmap R E F) :
+  (-f).graph = f.graph.map (linear_map.id.prod_map (-linear_map.id)) :=
+begin
+  ext, cases x,
+  split; intros h,
+  { rw mem_graph_iff at h,
+    rcases h with ⟨y, hy, h⟩,
+    rw linear_pmap.neg_apply at h,
+    rw submodule.mem_map,
+    simp only [mem_graph_iff, linear_map.prod_map_apply, linear_map.id_coe, id.def,
+      linear_map.neg_apply, prod.mk.inj_iff, prod.exists, exists_exists_and_eq_and],
+    use [x_fst, y],
+    simp [hy, h] },
+  rw submodule.mem_map at h,
+  rcases h with ⟨x', hx', h⟩,
+  cases x',
+  simp only [linear_map.prod_map_apply, linear_map.id_coe, id.def, linear_map.neg_apply,
+    prod.mk.inj_iff] at h,
+  rw mem_graph_iff at hx' ⊢,
+  rcases hx' with ⟨y, hy, hx'⟩,
+  use y,
+  rw [←h.1, ←h.2],
+  simp [hy, hx'],
+end
+
 lemma mem_graph_snd_inj (f : linear_pmap R E F) {x y : E} {x' y' : F} (hx : (x,x') ∈ f.graph)
   (hy : (y,y') ∈ f.graph) (hxy : x = y) : x' = y' :=
 begin
@@ -498,6 +555,72 @@ lemma graph_fst_eq_zero_snd (f : linear_pmap R E F) {x : E} {x' : F} (h : (x,x')
   (hx : x = 0) : x' = 0 :=
 f.mem_graph_snd_inj h f.graph.zero_mem hx
 
+lemma mem_domain_iff {f : linear_pmap R E F} {x : E} : x ∈ f.domain ↔ ∃ y : F, (x,y) ∈ f.graph :=
+begin
+  split; intro h,
+  { use f ⟨x, h⟩,
+    exact f.mem_graph ⟨x, h⟩ },
+  cases h with y h,
+  rw mem_graph_iff at h,
+  cases h with x' h,
+  simp only at h,
+  rw ←h.1,
+  simp,
+end
+
+lemma image_iff {f : linear_pmap R E F} {x : E} {y : F} (hx : x ∈ f.domain) :
+  y = f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph :=
+begin
+  rw mem_graph_iff,
+  split; intro h,
+  { use ⟨x, hx⟩,
+    simp [h] },
+  rcases h with ⟨⟨x', hx'⟩, ⟨h1, h2⟩⟩,
+  simp only [submodule.coe_mk] at h1 h2,
+  simp only [←h2, h1],
+end
+
+lemma mem_range_iff {f : linear_pmap R E F} {y : F} : y ∈ set.range f ↔ ∃ x : E, (x,y) ∈ f.graph :=
+begin
+  split; intro h,
+  { rw set.mem_range at h,
+    rcases h with ⟨⟨x, hx⟩, h⟩,
+    use x,
+    rw ←h,
+    exact f.mem_graph ⟨x, hx⟩ },
+  cases h with x h,
+  rw mem_graph_iff at h,
+  cases h with x h,
+  rw set.mem_range,
+  use x,
+  simp only at h,
+  rw h.2,
+end
+
+lemma mem_domain_iff_of_eq_graph {f g : linear_pmap R E F} (h : f.graph = g.graph) {x : E} :
+  x ∈ f.domain ↔ x ∈ g.domain :=
+by simp_rw [mem_domain_iff, h]
+
+lemma le_of_le_graph {f g : linear_pmap R E F} (h : f.graph ≤ g.graph) : f ≤ g :=
+begin
+  split,
+  { intros x hx,
+    rw mem_domain_iff at hx ⊢,
+    cases hx with y hx,
+    use y,
+    exact h hx },
+  rintros ⟨x, hx⟩ ⟨y, hy⟩ hxy,
+  rw image_iff,
+  refine h _,
+  simp only [submodule.coe_mk] at hxy,
+  rw hxy at hx,
+  rw ←image_iff hx,
+  simp [hxy],
+end
+
+lemma eq_of_eq_graph {f g : linear_pmap R E F} (h : f.graph = g.graph) : f = g :=
+by {ext, exact mem_domain_iff_of_eq_graph h, exact (le_of_le_graph h.le).2 }
+
 end graph
 
 end linear_pmap