feat (NormedSpace.Dual): make Dual reducible (#6998)

Following `LinearAlgebra.Dual` this makes `NormedSpace.Dual` reducible.

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -65,10 +65,12 @@ namespace ContinuousLinearMap
 
 variable [CompleteSpace E] [CompleteSpace G]
 
+-- Note: made noncomputable to stop excess compilation
+-- leanprover-community/mathlib4#7103
 /-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary
 definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric
 equivalence. -/
-def adjointAux : (E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E :=
+noncomputable def adjointAux : (E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E :=
   (ContinuousLinearMap.compSL _ _ _ _ _ ((toDual 𝕜 E).symm : NormedSpace.Dual 𝕜 E →L⋆[𝕜] E)).comp
     (toSesqForm : (E →L[𝕜] F) →L[𝕜] F →L⋆[𝕜] NormedSpace.Dual 𝕜 E)
 #align continuous_linear_map.adjoint_aux ContinuousLinearMap.adjointAux

Mathlib/Analysis/InnerProductSpace/Dual.lean

@@ -174,7 +174,8 @@ variable (B : E →L⋆[𝕜] E →L[𝕜] 𝕜)
 
 @[simp]
 theorem continuousLinearMapOfBilin_apply (v w : E) : ⟪B♯ v, w⟫ = B v w := by
-  simp [continuousLinearMapOfBilin]
+  rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
+    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
 #align inner_product_space.continuous_linear_map_of_bilin_apply InnerProductSpace.continuousLinearMapOfBilin_apply
 
 theorem unique_continuousLinearMapOfBilin {v f : E} (is_lax_milgram : ∀ w, ⟪f, w⟫ = B v w) :

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -135,19 +135,10 @@ def adjointAux : T.adjointDomain →ₗ[𝕜] E where
     hT.eq_of_inner_left fun _ => by
       simp only [inner_add_left, Submodule.coe_add, InnerProductSpace.toDual_symm_apply,
         adjointDomainMkClmExtend_apply]
-      -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5026):
-      -- mathlib3 was finished here
-      rw [adjointDomainMkClmExtend_apply, adjointDomainMkClmExtend_apply,
-        adjointDomainMkClmExtend_apply]
-      simp only [AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid, inner_add_left]
   map_smul' _ _ :=
     hT.eq_of_inner_left fun _ => by
       simp only [inner_smul_left, Submodule.coe_smul_of_tower, RingHom.id_apply,
         InnerProductSpace.toDual_symm_apply, adjointDomainMkClmExtend_apply]
-      -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5026):
-      -- mathlib3 was finished here
-      rw [adjointDomainMkClmExtend_apply, adjointDomainMkClmExtend_apply]
-      simp only [Submodule.coe_smul_of_tower, inner_smul_left]
 #align linear_pmap.adjoint_aux LinearPMap.adjointAux
 
 theorem adjointAux_inner (y : T.adjointDomain) (x : T.domain) :

Mathlib/Analysis/NormedSpace/Dual.lean

@@ -53,35 +53,16 @@ variable (E : Type*) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 /-- The topological dual of a seminormed space `E`. -/
-def Dual :=
-  E →L[𝕜] 𝕜
+abbrev Dual : Type _ := E →L[𝕜] 𝕜
 #align normed_space.dual NormedSpace.Dual
 
--- Porting note: added manually
-section DerivedInstances
+-- TODO: helper instance for elaboration of inclusionInDoubleDual_norm_eq until
+-- leanprover/lean4#2522 is resolved; remove once fixed
+instance : NormedSpace 𝕜 (Dual 𝕜 E) := inferInstance
 
-instance : Inhabited (Dual 𝕜 E) :=
-  inferInstanceAs (Inhabited (E →L[𝕜] 𝕜))
-
-instance : SeminormedAddCommGroup (Dual 𝕜 E) :=
-  inferInstanceAs (SeminormedAddCommGroup (E →L[𝕜] 𝕜))
-
-instance : NormedSpace 𝕜 (Dual 𝕜 E) :=
-  inferInstanceAs (NormedSpace 𝕜 (E →L[𝕜] 𝕜))
-
-end DerivedInstances
-
-instance : ContinuousLinearMapClass (Dual 𝕜 E) 𝕜 E 𝕜 :=
-  ContinuousLinearMap.continuousSemilinearMapClass
-
-instance : CoeFun (Dual 𝕜 E) fun _ => E → 𝕜 :=
-  FunLike.hasCoeToFun
-
-instance : NormedAddCommGroup (Dual 𝕜 F) :=
-  ContinuousLinearMap.toNormedAddCommGroup
-
-instance [FiniteDimensional 𝕜 E] : FiniteDimensional 𝕜 (Dual 𝕜 E) :=
-  inferInstanceAs (FiniteDimensional 𝕜 (E →L[𝕜] 𝕜))
+-- TODO: helper instance for elaboration of inclusionInDoubleDual_norm_le until
+-- leanprover/lean4#2522 is resolved; remove once fixed
+instance : SeminormedAddCommGroup (Dual 𝕜 E) := inferInstance
 
 /-- The inclusion of a normed space in its double (topological) dual, considered
    as a bounded linear map. -/

docs/undergrad.yaml

@@ -434,7 +434,7 @@ Topology:
   Hilbert spaces:
     Hilbert projection theorem: 'exists_norm_eq_iInf_of_complete_convex'
     orthogonal projection onto closed vector subspaces: 'orthogonalProjection'
-    dual space: 'NormedSpace.instNormedSpaceDualToNormedFieldInstSeminormedAddCommGroupDual'
+    dual space: 'NormedSpace.Dual'
     Riesz representation theorem: 'InnerProductSpace.toDual'
     inner product space $l^2$: 'lp.instInnerProductSpace'
     its completeness: 'lp.instCompleteSpace'