feat(Analysis/InnerProductSpace/Dual, Mathlib/Analysis/Normed/Group/SeparationQuotient): add null submodule and various lifts

Mathlib.lean

@@ -1268,6 +1268,7 @@ import Mathlib.Analysis.Normed.Group.SemiNormedGrp
 import Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
 import Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
 import Mathlib.Analysis.Normed.Group.Seminorm
+import Mathlib.Analysis.Normed.Group.SeparationQuotient
 import Mathlib.Analysis.Normed.Group.Submodule
 import Mathlib.Analysis.Normed.Group.Tannery
 import Mathlib.Analysis.Normed.Group.Ultra

Mathlib/Analysis/InnerProductSpace/Dual.lean

@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis
 -/
 import Mathlib.Analysis.InnerProductSpace.Projection
 import Mathlib.Analysis.Normed.Module.Dual
+import Mathlib.Analysis.Normed.Group.SeparationQuotient
 
 /-!
 # The Fréchet-Riesz representation theorem
@@ -33,7 +34,6 @@ given by substituting `E →L[𝕜] 𝕜` with `E` using `toDual`.
 dual, Fréchet-Riesz
 -/
 
-
 noncomputable section
 
 open scoped Classical
@@ -48,6 +48,7 @@ open RCLike ContinuousLinearMap
 variable (𝕜 E : Type*)
 
 section Seminormed
+
 variable [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 
 local notation "⟪" x ", " y "⟫" => @inner 𝕜 E _ x y
@@ -69,6 +70,61 @@ variable {E}
 theorem toDualMap_apply {x y : E} : toDualMap 𝕜 E x y = ⟪x, y⟫ :=
   rfl
 
+section NullSubmodule
+
+open SeparationQuotientAddGroup LinearMap
+
+variable (E)
+
+/-- The null space with respect to the norm. -/
+def nullSubmodule : Submodule 𝕜 E where
+  __ := nullSubgroup
+  smul_mem' c x (hx : ‖x‖ = 0) := show ‖c • x‖ = 0 from
+    le_antisymm (norm_smul_le _ _ |>.trans <| by rw [hx, mul_zero]) (norm_nonneg _)
+
+@[simp]
+lemma mem_nullSubmodule_iff {x : E} : x ∈ nullSubmodule 𝕜 E ↔ ‖x‖ = 0 := Iff.rfl
+
+lemma inner_eq_zero_of_left (x y : E) (h : ‖x‖ = 0) :
+    ⟪x, y⟫_𝕜 = 0 := by
+  rw [← norm_eq_zero, ← sq_eq_zero_iff]
+  apply le_antisymm _ (sq_nonneg _)
+  rw [sq]
+  nth_rw 2 [← RCLike.norm_conj]
+  rw [_root_.inner_conj_symm]
+  calc ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜 := inner_mul_inner_self_le _ _
+  _ = (‖x‖ * ‖x‖) * re ⟪y, y⟫_𝕜 := by rw [inner_self_eq_norm_mul_norm x]
+  _ = (0 * 0) * re ⟪y, y⟫_𝕜 := by rw [(mem_nullSubmodule_iff 𝕜 E).mp h]
+  _ = 0 := by ring
+
+lemma inner_nullSubmodule_right_eq_zero (x y : E) (h : ‖y‖ = 0) : ⟪x, y⟫_𝕜 = 0 := by
+  rw [inner_eq_zero_symm]
+  exact inner_eq_zero_of_left 𝕜 E y x h
+
+lemma norm_sub_eq_norm (x y : E) (h : ‖y‖ = 0) : ‖x - y‖ = ‖x‖ := by
+  apply le_antisymm ?_ ?_
+  · simpa [h] using norm_sub_le x y
+  · simpa [h] using norm_add_le (x - y) y
+
+/-- For each `x : E`, the kernel of `⟪x, ⬝⟫` includes the null space. -/
+lemma nullSubmodule_le_ker_toDualMap (x : E) : nullSubmodule 𝕜 E ≤ ker (toDualMap 𝕜 E x) := by
+  intro y hy
+  refine LinearMap.mem_ker.mpr ?_
+  simp only [toDualMap_apply]
+  exact inner_nullSubmodule_right_eq_zero 𝕜 E x y hy
+
+/-- The kernel of the map `x ↦ ⟪x, ⬝⟫` includes the null space. -/
+lemma nullSubmodule_le_ker_toDualMap' : nullSubmodule 𝕜 E ≤ ker (toDualMap 𝕜 E) := by
+  intro x hx
+  refine LinearMap.mem_ker.mpr ?_
+  ext y
+  simp only [toDualMap_apply, ContinuousLinearMap.zero_apply]
+  exact inner_eq_zero_of_left 𝕜 E x y hx
+
+lemma isClosed_nullSubmodule : IsClosed (nullSubmodule 𝕜 E : Set E) := isClosed_nullSubgroup
+
+end NullSubmodule
+
 end Seminormed
 
 section Normed

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -418,7 +418,7 @@ theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf [TopologicalAd
       t = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace := by
   rw [p.withSeminorms_iff_nhds_eq_iInf,
     TopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
-    nhds_iInf]
+    _root_.nhds_iInf]
   congrm _ = ⨅ i, ?_
   exact @comap_norm_nhds_zero _ (p i).toSeminormedAddGroup
 
@@ -438,7 +438,7 @@ theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf [u : UniformSpace
     WithSeminorms p ↔ u = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace := by
   rw [p.withSeminorms_iff_nhds_eq_iInf,
     UniformAddGroup.ext_iff inferInstance (uniformAddGroup_iInf fun i => inferInstance),
-    UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
+    UniformSpace.toTopologicalSpace_iInf, _root_.nhds_iInf]
   congrm _ = ⨅ i, ?_
   exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup
 

Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2024 Yoh Tanimoto. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yoh Tanimoto
+-/
+import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.Analysis.Normed.Group.Hom
+
+-- TODO modify doc, check if instances are really needed, golf
+-- want to define liftCLM. problem: a CLM on a normed vector space
+-- is not automatically a `NormedAddGroupHom
+
+
+/-!
+# Lifts of maps to separation quotients of seminormed groups
+
+For any `SeminormedAddCommGroup M`, a `NormedAddCommGroup` instance has been defined in
+`Mathlib.Analysis.Normed.Group.Uniform`.
+
+## Main definitions
+
+We use `M` and `N` to denote seminormed groups.
+All the following definitions are in the `NullSubgroup` namespace. Hence we can access
+`NullSubgroup.normedMk` as `normedMk`.
+
+* `normedAddCommGroupQuotient` : The normed group structure on the quotient by the null subgroup.
+    This is an instance so there is no need to explicitly use it.
+
+* `normedMk` : the normed group hom from `M` to `SeparationQuotient M`.
+
+* `lift f hf`: implements the universal property of `SeparationQuotient M`. Here
+    `(f : NormedAddGroupHom M N)`, `(hf : ∀ s ∈ nullSubgroup M, f s = 0)` and
+    `lift f hf : NormedAddGroupHom (SeparationQuotient M) N`.
+
+* `IsQuotient`: given `f : NormedAddGroupHom M N`, `IsQuotient f` means `N` is isomorphic
+    to a quotient of `M` by the null subgroup, with projection `f`. Technically it asserts `f` is
+    surjective and the norm of `f x` is the infimum of the norms of `x + m` for `m` in `f.ker`.
+
+## Main results
+
+* `norm_normedMk` : the operator norm of the projection is `1` if the subspace is not dense.
+
+* `IsQuotient.norm_lift`: Provided `f : normed_hom M N` satisfies `IsQuotient f`, for every
+     `n : N` and positive `ε`, there exists `m` such that `f m = n ∧ ‖m‖ < ‖n‖ + ε`.
+
+
+## Implementation details
+
+For any `SeminormedAddCommGroup M`, we define a norm on `SeparationQuotient M` by
+`‖x‖ = ‖mk x‖` using the lift.
+
+-/
+
+
+noncomputable section
+
+open SeparationQuotient Metric Set Topology NNReal
+
+variable {M N : Type*} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N]
+
+namespace SeparationQuotientAddGroup
+
+/-- The null subgroup with respect to the norm. -/
+def nullSubgroup : AddSubgroup M where
+  carrier := {x : M | ‖x‖ = 0}
+  add_mem' {x y} (hx : ‖x‖ = 0) (hy : ‖y‖ = 0) := by
+    apply le_antisymm _ (norm_nonneg _)
+    refine (norm_add_le x y).trans_eq ?_
+    rw [hx, hy, add_zero]
+  zero_mem' := norm_zero
+  neg_mem' {x} (hx : ‖x‖ = 0) := by
+    simp only [mem_setOf_eq, norm_neg]
+    exact hx
+
+lemma inseparable_iff_norm_zero (x y : M) : Inseparable x y ↔ ‖x - y‖ = 0 := by
+  rw [Metric.inseparable_iff, dist_eq_norm]
+
+lemma isClosed_nullSubgroup : IsClosed (@nullSubgroup M _ : Set M) :=
+  isClosed_singleton.preimage continuous_norm
+
+instance : Nonempty (@nullSubgroup M _) := ⟨0⟩
+
+variable (x : SeparationQuotient M)
+
+variable (z : M)
+
+/-- The norm of the image of `m : M` in the quotient by the null space is zero if and only if `m`
+belongs to the null space. -/
+theorem quotient_norm_eq_zero_iff (m : M) :
+    ‖mk m‖ = 0 ↔ m ∈ nullSubgroup := by
+  rw [norm_mk]
+  exact Eq.to_iff rfl
+
+/-- If for `(m : M)` it holds that `mk m = 0`, then `m  ∈ nullSubgroup`. -/
+theorem mk_eq_zero_iff (m : M) : mk m = 0 ↔ m ∈ nullSubgroup := by
+  rw [← quotient_norm_eq_zero_iff]
+  exact Iff.symm norm_eq_zero
+
+open NormedAddGroupHom
+
+/-- The morphism from a seminormed group to the quotient by the null space. -/
+noncomputable def normedMk : NormedAddGroupHom M (SeparationQuotient M) :=
+  { mkAddGroupHom with
+    bound' := ⟨1, fun m => by simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe,
+      mkAddGroupHom_apply, norm_mk, one_mul, le_refl]⟩}
+
+/-- `mkAddGroupHom` agrees with `QuotientAddGroup.mk`. -/
+@[simp]
+theorem normedMk.apply (m : M) : normedMk m = mk m := rfl
+
+/-- `normedMk` is surjective. -/
+theorem surjective_normedMk : Function.Surjective (@normedMk M _) :=
+  surjective_quot_mk _
+
+/-- The kernel of `normedMk` is `nullSubgroup`. -/
+theorem ker_normedMk : (@normedMk M _).ker = nullSubgroup := by
+  ext _; exact mk_eq_zero_iff _
+
+/-- The operator norm of the projection is at most `1`. -/
+theorem norm_normedMk_le : ‖(@normedMk M _)‖ ≤ 1 :=
+  NormedAddGroupHom.opNorm_le_bound _ zero_le_one fun m => by simp only [normedMk.apply, norm_mk,
+    one_mul, le_refl]
+
+lemma eq_of_inseparable (f : NormedAddGroupHom M N) (hf : ∀ x ∈ nullSubgroup, f x = 0) :
+    ∀ x y, Inseparable x y → f x = f y :=
+  fun _ _ h ↦ eq_of_sub_eq_zero <| by
+    rw [← map_sub]
+    exact hf _ <| inseparable_iff_norm_zero .. |>.mp h
+
+/-- The lift of a group hom to the separation quotient as a group hom. -/
+noncomputable def liftNormedAddGroupHom (f : NormedAddGroupHom M N)
+    (hf : ∀ x ∈ nullSubgroup, f x = 0) : NormedAddGroupHom (SeparationQuotient M) N :=
+  { SeparationQuotient.liftContinuousAddMonoidHom ⟨f.toAddMonoidHom, f.continuous⟩
+      <| eq_of_inseparable f hf with
+    bound' := by
+      use ‖f‖
+      intro v
+      obtain ⟨v', hv'⟩ := surjective_mk v
+      rw [← hv']
+      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe,
+        liftContinuousAddCommMonoidHom_apply, AddMonoidHom.coe_coe, norm_mk]
+      exact le_opNorm f v'}
+
+@[simp]
+theorem liftNormedAddGroupHom_apply (f : NormedAddGroupHom M N) (hf : ∀ x ∈ nullSubgroup, f x = 0)
+    (x : M) : liftNormedAddGroupHom f hf (mk x) = f x := rfl
+
+/-- For a norm-continuous group homomorphism `f`, its lift to the separation quotient
+is bounded by the norm of `f`-/
+theorem norm_liftNormedAddGroupHom_apply_le (f : NormedAddGroupHom M N)
+    (hf : ∀ x ∈ nullSubgroup, f x = 0) (x : SeparationQuotient M) :
+    ‖liftNormedAddGroupHom f hf x‖ ≤ ‖f‖ * ‖x‖ := by
+  obtain ⟨x', hx'⟩ := surjective_mk x
+  rw [← hx']
+  simp only [coe_toAddMonoidHom, lift_mk, norm_mk]
+  exact le_opNorm f x'
+
+theorem liftNormedAddGroupHom_unique {N : Type*} [SeminormedAddCommGroup N]
+    (f : NormedAddGroupHom M N) (hf : ∀ s ∈ nullSubgroup, f s = 0)
+    (g : NormedAddGroupHom (SeparationQuotient M) N) (h : g.comp normedMk = f) :
+    g = liftNormedAddGroupHom f hf := by
+  ext x
+  rcases surjective_normedMk x with ⟨x, rfl⟩
+  change g.comp normedMk x = _
+  simp only [h]
+  rfl
+
+theorem norm_liftNormedAddGroupHom_le {N : Type*} [SeminormedAddCommGroup N]
+    (f : NormedAddGroupHom M N) (hf : ∀ s ∈ nullSubgroup, f s = 0) :
+    ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖ :=
+  NormedAddGroupHom.opNorm_le_bound _ (norm_nonneg f) (norm_liftNormedAddGroupHom_apply_le f hf)
+
+theorem liftNormedAddGroupHom_norm_le {N : Type*} [SeminormedAddCommGroup N]
+    (f : NormedAddGroupHom M N) (hf : ∀ s ∈ nullSubgroup, f s = 0) {c : ℝ≥0} (fb : ‖f‖ ≤ c) :
+    ‖liftNormedAddGroupHom f hf‖ ≤ c :=
+  (norm_liftNormedAddGroupHom_le f hf).trans fb
+
+theorem liftNormedAddGroupHom_normNoninc {N : Type*} [SeminormedAddCommGroup N]
+    (f : NormedAddGroupHom M N) (hf : ∀ s ∈ nullSubgroup, f s = 0) (fb : f.NormNoninc) :
+    (liftNormedAddGroupHom f hf).NormNoninc := fun x => by
+  have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb
+  simpa using NormedAddGroupHom.le_of_opNorm_le _
+    (liftNormedAddGroupHom_norm_le f _ fb') _
+
+/-- The operator norm of the projection is `1` if the null space is not dense. -/
+theorem norm_normedMk (h : (@nullSubgroup M _ : Set M) ≠ univ) :
+    ‖(@normedMk M _)‖ = 1 := by
+  apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one
+  · simp only [normedMk.apply, one_mul]
+    exact fun x ↦ Preorder.le_refl ‖SeparationQuotient.mk x‖
+  · simp only [ge_iff_le, normedMk.apply]
+    intro N hN hx
+    rw [← nonempty_compl] at h
+    obtain ⟨x, hxnn⟩ := h
+    have : 0 < ‖x‖ := Ne.lt_of_le (Ne.symm hxnn) (norm_nonneg x)
+    exact one_le_of_le_mul_right₀ this (hx x)
+
+/-- The operator norm of the projection is `0` if the null space is dense. -/
+theorem norm_trivial_separationQuotient_mk (h : (@nullSubgroup M _ : Set M) = Set.univ) :
+    ‖@normedMk M _‖ = 0 := by
+  apply NormedAddGroupHom.opNorm_eq_of_bounds _ (le_refl 0)
+  · intro x
+    have : x ∈ nullSubgroup := by
+      rw [← SetLike.mem_coe, h]
+      exact trivial
+    simp only [normedMk.apply, zero_mul, norm_le_zero_iff]
+    exact (mk_eq_zero_iff x).mpr this
+  · exact fun N => fun hN => fun _ => hN
+
+end SeparationQuotientAddGroup