refactor: use junk values in Submodule.toLinearPMap (#5529)

Change the definition of `Submodule.toLinearPMap` to use a junk value in the case that the condition that the subspace defines the graph of a function is not satisfied. In this case we define `Submodule.toLinearPMap` as the zero map. The domain is the same so that the domain does not depend on the graph-condition.



Co-authored-by: Oliver Nash <github@olivernash.org>

Mathlib/LinearAlgebra/LinearPMap.lean

@@ -945,41 +945,62 @@ theorem valFromGraph_mem {g : Submodule R (E × F)}
   (ExistsUnique.exists (existsUnique_from_graph @hg ha)).choose_spec
 #align submodule.val_from_graph_mem Submodule.valFromGraph_mem
 
-/-- Define a `LinearPMap` from its graph. -/
-noncomputable def toLinearPMap (g : Submodule R (E × F))
-    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) : E →ₗ.[R] F
+/-- Define a `LinearMap` from its graph.
+
+Helper definition for `LinearPMap`. -/
+noncomputable def toLinearPMapAux (g : Submodule R (E × F))
+    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
+    g.map (LinearMap.fst R E F) →ₗ[R] F where
+  toFun := fun x => valFromGraph hg x.2
+  map_add' := fun v w => by
+    have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2
+    have hvw := valFromGraph_mem hg hadd
+    have hvw' := g.add_mem (valFromGraph_mem hg v.2) (valFromGraph_mem hg w.2)
+    rw [Prod.mk_add_mk] at hvw'
+    exact (existsUnique_from_graph @hg hadd).unique hvw hvw'
+  map_smul' := fun a v => by
+    have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
+    have hav := valFromGraph_mem hg hsmul
+    have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
+    rw [Prod.smul_mk] at hav'
+    exact (existsUnique_from_graph @hg hsmul).unique hav hav'
+
+open Classical in
+/-- Define a `LinearPMap` from its graph.
+
+In the case that the submodule is not a graph of a `LinearPMap` then the underlying linear map
+is just the zero map. -/
+noncomputable def toLinearPMap (g : Submodule R (E × F)) : E →ₗ.[R] F
     where
   domain := g.map (LinearMap.fst R E F)
-  toFun :=
-    { toFun := fun x => valFromGraph hg x.2
-      map_add' := fun v w => by
-        have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2
-        have hvw := valFromGraph_mem hg hadd
-        have hvw' := g.add_mem (valFromGraph_mem hg v.2) (valFromGraph_mem hg w.2)
-        rw [Prod.mk_add_mk] at hvw'
-        exact (existsUnique_from_graph @hg hadd).unique hvw hvw'
-      map_smul' := fun a v => by
-        have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
-        have hav := valFromGraph_mem hg hsmul
-        have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
-        rw [Prod.smul_mk] at hav'
-        exact (existsUnique_from_graph @hg hsmul).unique hav hav' }
+  toFun := if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0 then
+    g.toLinearPMapAux hg else 0
 #align submodule.to_linear_pmap Submodule.toLinearPMap
 
-theorem toLinearPMap_domain (g : Submodule R (E × F))
-    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
-    (g.toLinearPMap hg).domain = g.map (LinearMap.fst R E F) := rfl
+theorem toLinearPMap_domain (g : Submodule R (E × F)) :
+    g.toLinearPMap.domain = g.map (LinearMap.fst R E F) := rfl
+
+theorem toLinearPMap_apply_aux {g : Submodule R (E × F)}
+    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
+    (x : g.map (LinearMap.fst R E F)) :
+    g.toLinearPMap x = valFromGraph hg x.2 := by
+  classical
+  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
+  rw [dif_pos]
+  · rfl
+  · exact hg
 
-theorem mem_graph_toLinearPMap (g : Submodule R (E × F))
+theorem mem_graph_toLinearPMap {g : Submodule R (E × F)}
     (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
-    (x : g.map (LinearMap.fst R E F)) : (x.val, g.toLinearPMap hg x) ∈ g :=
-  valFromGraph_mem hg x.2
+    (x : g.map (LinearMap.fst R E F)) : (x.val, g.toLinearPMap x) ∈ g := by
+  rw [toLinearPMap_apply_aux hg]
+  exact valFromGraph_mem hg x.2
 #align submodule.mem_graph_to_linear_pmap Submodule.mem_graph_toLinearPMap
 
 @[simp]
 theorem toLinearPMap_graph_eq (g : Submodule R (E × F))
     (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
-    (g.toLinearPMap hg).graph = g := by
+    g.toLinearPMap.graph = g := by
   ext x
   constructor <;> intro hx
   · rw [LinearPMap.mem_graph_iff] at hx
@@ -992,13 +1013,14 @@ theorem toLinearPMap_graph_eq (g : Submodule R (E × F))
     simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
     exact ⟨x_snd, hx⟩
   refine' ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, _⟩
+  rw [toLinearPMap_apply_aux hg]
   exact (existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx
 #align submodule.to_linear_pmap_graph_eq Submodule.toLinearPMap_graph_eq
 
 theorem toLinearPMap_range (g : Submodule R (E × F))
     (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
-    LinearMap.range (g.toLinearPMap hg).toFun = g.map (LinearMap.snd R E F) := by
-  rw [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]
+    LinearMap.range g.toLinearPMap.toFun = g.map (LinearMap.snd R E F) := by
+  rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]
 
 end SubmoduleToLinearPMap
 
@@ -1008,42 +1030,48 @@ namespace LinearPMap
 
 section inverse
 
-variable {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥)
-
 /-- The inverse of a `LinearPMap`. -/
-noncomputable def inverse : F →ₗ.[R] E :=
+noncomputable def inverse (f : E →ₗ.[R] F) : F →ₗ.[R] E :=
   (f.graph.map (LinearEquiv.prodComm R E F)).toLinearPMap
-  (fun v hv hv' => by
-    simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
-      LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk] at hv
-    rcases hv with ⟨a, b, ⟨ha, h1⟩, ⟨h2, h3⟩⟩
-    simp only at hv' ⊢
-    rw [hv'] at h1
-    rw [LinearMap.ker_eq_bot'] at hf
-    specialize hf ⟨a, ha⟩ h1
-    simp only [Submodule.mk_eq_zero] at hf
-    exact hf )
-
-theorem inverse_graph : (inverse hf).graph = f.graph.map (LinearEquiv.prodComm R E F) := by
-  rw [inverse, Submodule.toLinearPMap_graph_eq]
-
-theorem inverse_domain : (inverse hf).domain = LinearMap.range f.toFun := by
+
+variable {f : E →ₗ.[R] F}
+
+theorem inverse_domain : (inverse f).domain = LinearMap.range f.toFun := by
   rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
     ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
   rfl
 
-theorem inverse_range : LinearMap.range (inverse hf).toFun = f.domain := by
-  rw [inverse, Submodule.toLinearPMap_range, ← graph_map_fst_eq_domain,
-    ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
+variable (hf : LinearMap.ker f.toFun = ⊥)
+
+/-- The graph of the inverse generates a `LinearPMap`. -/
+theorem mem_inverse_graph_snd_eq_zero (x : F × E)
+    (hv : x ∈ (graph f).map (LinearEquiv.prodComm R E F))
+    (hv' : x.fst = 0) : x.snd = 0 := by
+  simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
+    LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk] at hv
+  rcases hv with ⟨a, b, ⟨ha, h1⟩, ⟨h2, h3⟩⟩
+  simp only at hv' ⊢
+  rw [hv'] at h1
+  rw [LinearMap.ker_eq_bot'] at hf
+  specialize hf ⟨a, ha⟩ h1
+  simp only [Submodule.mk_eq_zero] at hf
+  exact hf
+
+theorem inverse_graph : (inverse f).graph = f.graph.map (LinearEquiv.prodComm R E F) := by
+  rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]
+
+theorem inverse_range : LinearMap.range (inverse f).toFun = f.domain := by
+  rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
+    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
   rfl
 
-theorem mem_inverse_graph (x : f.domain) : (f x, (x : E)) ∈ (inverse hf).graph := by
-  simp only [inverse_graph, Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left,
+theorem mem_inverse_graph (x : f.domain) : (f x, (x : E)) ∈ (inverse f).graph := by
+  simp only [inverse_graph hf, Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left,
     exists_eq_left, LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
   exact ⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩
 
-theorem inverse_apply_eq {y : (inverse hf).domain} {x : f.domain} (hxy : f x = y) :
-    (inverse hf) y = x := by
+theorem inverse_apply_eq {y : (inverse f).domain} {x : f.domain} (hxy : f x = y) :
+    (inverse f) y = x := by
   have := mem_inverse_graph hf x
   simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left] at this
   rcases this with ⟨hx, h⟩

Mathlib/Topology/Algebra/Module/LinearPMap.lean

@@ -84,11 +84,9 @@ theorem IsClosable.leIsClosable {f g : E →ₗ.[R] F} (hf : f.IsClosable) (hfg
   have : g.graph.topologicalClosure ≤ f'.graph := by
     rw [← hf]
     exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
-  refine' ⟨g.graph.topologicalClosure.toLinearPMap _, _⟩
-  · intro x hx hx'
-    cases x
-    exact f'.graph_fst_eq_zero_snd (this hx) hx'
+  use g.graph.topologicalClosure.toLinearPMap
   rw [Submodule.toLinearPMap_graph_eq]
+  exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'
 #align linear_pmap.is_closable.le_is_closable LinearPMap.IsClosable.leIsClosable
 
 /-- The closure is unique. -/