From 83f594621f6dd54850770da491d866c1ab60dada Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Thu, 3 Aug 2023 09:17:13 +0000 Subject: [PATCH] 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 --- Mathlib/LinearAlgebra/LinearPMap.lean | 130 +++++++++++------- .../Topology/Algebra/Module/LinearPMap.lean | 6 +- 2 files changed, 81 insertions(+), 55 deletions(-) diff --git a/Mathlib/LinearAlgebra/LinearPMap.lean b/Mathlib/LinearAlgebra/LinearPMap.lean index 33da054618dfa..8eb088d87a8ac 100644 --- a/Mathlib/LinearAlgebra/LinearPMap.lean +++ b/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⟩ diff --git a/Mathlib/Topology/Algebra/Module/LinearPMap.lean b/Mathlib/Topology/Algebra/Module/LinearPMap.lean index 013f8128ce681..4ce94a466d6d1 100644 --- a/Mathlib/Topology/Algebra/Module/LinearPMap.lean +++ b/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. -/