feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and mk (#18178)

Define the `mk` and lifts of normed spaces and normed groups by the inseparable setoid as `NormedAddGroupHom`, `CLM`, etc.



Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

Author: yoh-tanimoto

Mathlib.lean

@@ -1494,6 +1494,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
@@ -5310,6 +5311,7 @@ import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.Ring.Ideal
 import Mathlib.Topology.Algebra.Semigroup
 import Mathlib.Topology.Algebra.SeparationQuotient.Basic
+import Mathlib.Topology.Algebra.SeparationQuotient.Hom
 import Mathlib.Topology.Algebra.SeparationQuotient.Section
 import Mathlib.Topology.Algebra.Star
 import Mathlib.Topology.Algebra.StarSubalgebra

Mathlib/Analysis/Normed/Group/Hom.lean

@@ -229,6 +229,9 @@ protected theorem uniformContinuous (f : NormedAddGroupHom V₁ V₂) : UniformC
 protected theorem continuous (f : NormedAddGroupHom V₁ V₂) : Continuous f :=
   f.uniformContinuous.continuous
 
+instance : ContinuousMapClass (NormedAddGroupHom V₁ V₂) V₁ V₂ where
+  map_continuous := fun f => f.continuous
+
 theorem ratio_le_opNorm (x : V₁) : ‖f x‖ / ‖x‖ ≤ ‖f‖ :=
   div_le_of_le_mul₀ (norm_nonneg _) f.opNorm_nonneg (le_opNorm _ _)
 

Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

@@ -0,0 +1,142 @@
+/-
+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.Group.Hom
+import Mathlib.Topology.Algebra.SeparationQuotient.Hom
+
+/-!
+# 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 `SeparationQuotient` namespace. Hence we can access
+`SeparationQuotient.normedMk` as `normedMk`.
+
+* `normedMk` : the normed group hom from `M` to `SeparationQuotient M`.
+
+* `liftNormedAddGroupHom` :
+Any bounded group hom `f : M → N` such that `∀ x, ‖x‖ = 0 → f x = 0` descends to a bounded group hom
+`SeparationQuotient M → N`. Here, `(f : NormedAddGroupHom M N)`, `(hf : ∀ x : M, ‖x‖ = 0 → f x = 0)`
+and `liftNormedAddGroupHom f hf : NormedAddGroupHom (SeparationQuotient M) N` such that
+`liftNormedAddGroupHom f hf (mk x) = f x`.
+
+## Main results
+
+* `norm_normedMk_eq_one : the operator norm of the projection is `1` if the subspace is not `⊤`.
+
+* `norm_liftNormedAddGroupHom_le` : `‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖`.
+-/
+
+section
+
+open SeparationQuotient NNReal
+
+variable {M N : Type*} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N]
+
+namespace SeparationQuotient
+
+open NormedAddGroupHom
+
+/-- The morphism from a seminormed group to the quotient by the inseparable setoid. -/
+@[simps]
+noncomputable def normedMk : NormedAddGroupHom M (SeparationQuotient M) where
+  __ := mkAddMonoidHom
+  bound' := ⟨1, by simp⟩
+
+/-- The operator norm of the projection is at most `1`. -/
+theorem norm_normedMk_le : ‖normedMk (M := M)‖ ≤ 1 :=
+  NormedAddGroupHom.opNorm_le_bound _ zero_le_one fun m => by simp
+
+lemma apply_eq_apply_of_inseparable {F : Type*} [FunLike F M N] [AddMonoidHomClass F M N] (f : F)
+    (hf : ∀ x, ‖x‖ = 0 → f x = 0) : ∀ x y, Inseparable x y → f x = f y :=
+  fun x y h ↦ eq_of_sub_eq_zero <| by
+    rw [← map_sub]
+    rw [Metric.inseparable_iff, dist_eq_norm] at h
+    exact hf (x - y) h
+
+/-- The lift of a group hom to the separation quotient as a group hom. -/
+@[simps]
+noncomputable def liftNormedAddGroupHom (f : NormedAddGroupHom M N)
+    (hf : ∀ x, ‖x‖ = 0 → f x = 0) : NormedAddGroupHom (SeparationQuotient M) N where
+  toFun := SeparationQuotient.liftContinuousAddMonoidHom f <| apply_eq_apply_of_inseparable f hf
+  map_add' v₁ v₂ := map_add ..
+  bound' := by
+    refine ⟨‖f‖, fun v ↦ ?_⟩
+    obtain ⟨v, rfl⟩ := surjective_mk v
+    exact le_opNorm f v
+
+theorem norm_liftNormedAddGroupHom_apply_le (f : NormedAddGroupHom M N)
+    (hf : ∀ x, ‖x‖ = 0 → f x = 0) (x : SeparationQuotient M) :
+    ‖liftNormedAddGroupHom f hf x‖ ≤ ‖f‖ * ‖x‖ := by
+  obtain ⟨x, rfl⟩ := surjective_mk x
+  exact le_opNorm f x
+
+/-- The equivalence between `NormedAddGroupHom M N` vanishing on the inseparable setoid and
+`NormedAddGroupHom (SeparationQuotient M) N`. -/
+@[simps]
+noncomputable def liftNormedAddGroupHomEquiv {N : Type*} [SeminormedAddCommGroup N] :
+    {f : NormedAddGroupHom M N // ∀ x, ‖x‖ = 0 → f x = 0} ≃
+    NormedAddGroupHom (SeparationQuotient M) N where
+  toFun f := liftNormedAddGroupHom f f.prop
+  invFun g := ⟨g.comp normedMk, by
+    intro x hx
+    rw [← norm_mk, norm_eq_zero] at hx
+    simp [hx]⟩
+  left_inv _ := rfl
+  right_inv _ := by
+    ext x
+    obtain ⟨x, rfl⟩ := surjective_mk 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_le {N : Type*} [SeminormedAddCommGroup N]
+    (f : NormedAddGroupHom M N) (hf : ∀ s, ‖s‖ = 0 → 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, ‖s‖ = 0 → 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, ‖s‖ = 0 → f s = 0) (fb : f.NormNoninc) :
+    (liftNormedAddGroupHom f hf).NormNoninc := fun x => by
+  have fb' : ‖f‖ ≤ 1 := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb
+  exact le_trans (norm_liftNormedAddGroupHom_apply_le f hf x)
+    (mul_le_of_le_one_left (norm_nonneg x) fb')
+
+/-- The operator norm of the projection is `1` if there is an element whose norm is different from
+`0`. -/
+theorem norm_normedMk_eq_one (h : ∃ x : M, ‖x‖ ≠ 0) :
+    ‖normedMk (M := M)‖ = 1 := by
+  apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one
+  · simpa only [normedMk_apply, one_mul] using fun _ ↦ le_rfl
+  · intro N _ hle
+    obtain ⟨x, _⟩ := h
+    exact one_le_of_le_mul_right₀ (by positivity) (hle x)
+
+/-- The projection is `0` if and only if all the elements have norm `0`. -/
+theorem normedMk_eq_zero_iff : normedMk (M := M) = 0 ↔ ∀ (x : M), ‖x‖ = 0 := by
+  constructor
+  · intro h x
+    rw [SeparationQuotient.mk_eq_zero_iff.mp]
+    have : normedMk x = 0 := by
+      rw [h]
+      simp only [zero_apply]
+    rw [← this]
+    simp
+  · intro h
+    ext x
+    simpa [← norm_eq_zero] using h x
+
+end SeparationQuotient
+
+end

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -278,6 +278,13 @@ instance : CommGroup (ContinuousMonoidHom A E) where
   inv f := (inv E).comp f
   inv_mul_cancel f := ext fun x => inv_mul_cancel (f x)
 
+/-- For `f : F` where `F` is a class of continuous monoid hom, this yields an element
+`ContinuousMonoidHom A B`. -/
+@[to_additive "For `f : F` where `F` is a class of continuous additive monoid hom, this yields
+an element `ContinuousAddMonoidHom A B`."]
+def ofClass (F : Type*) [FunLike F A B] [ContinuousMapClass F A B]
+    [MonoidHomClass F A B] (f : F) : (ContinuousMonoidHom A B) := toContinuousMonoidHom f
+
 end ContinuousMonoidHom
 
 end

Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

@@ -21,6 +21,8 @@ which is a continuous linear map `SeparationQuotient E →L[K] E`.
 
 assert_not_exists LinearIndependent
 
+open scoped Topology
+
 namespace SeparationQuotient
 
 section SMul
@@ -195,6 +197,10 @@ instance instGroup [Group G] [TopologicalGroup G] : Group (SeparationQuotient G)
 instance instCommGroup [CommGroup G] [TopologicalGroup G] : CommGroup (SeparationQuotient G) :=
   surjective_mk.commGroup mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow
 
+/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
+theorem nhds_mk (x : G) : 𝓝 (mk x) = .map mk (𝓝 x) :=
+  le_antisymm ((SeparationQuotient.isOpenMap_mk).nhds_le x) continuous_quot_mk.continuousAt
+
 end Group
 
 section UniformGroup
@@ -364,8 +370,10 @@ end DistribSMul
 
 section Module
 
-variable {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
+variable {R S M N : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
     [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M]
+    [Semiring S] [AddCommMonoid N] [Module S N]
+    [TopologicalSpace N]
 
 instance instModule : Module R (SeparationQuotient M) :=
   surjective_mk.module R mkAddMonoidHom mk_smul
@@ -379,6 +387,20 @@ def mkCLM : M →L[R] SeparationQuotient M where
   map_add' := mk_add
   map_smul' := mk_smul
 
+variable {R M}
+
+/-- The lift (as a continuous linear map) of `f` with `f x = f y` for `Inseparable x y`. -/
+@[simps]
+noncomputable def liftCLM {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y) :
+    SeparationQuotient M →SL[σ] N where
+  toFun := SeparationQuotient.lift f hf
+  map_add' := Quotient.ind₂ <| map_add f
+  map_smul' {r} := Quotient.ind <| map_smulₛₗ f r
+
+@[simp]
+theorem liftCLM_mk {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y)
+    (x : M) : liftCLM f hf (mk x) = f x := rfl
+
 end Module
 
 section Algebra

Mathlib/Topology/Algebra/SeparationQuotient/Hom.lean

@@ -0,0 +1,40 @@
+/-
+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.Topology.Algebra.ContinuousMonoidHom
+import Mathlib.Topology.Algebra.SeparationQuotient.Basic
+
+/-!
+# Lift of `MonoidHom M N` to `MonoidHom (SeparationQuotient M) N`
+
+In this file we define the lift of a continuous monoid homomorphism `f` from `M` to `N` to
+`SeparationQuotient M`, assuming that `f` maps two inseparable elements to the same element.
+-/
+
+namespace SeparationQuotient
+
+section Monoid
+
+variable {M N : Type*} [TopologicalSpace M]  [TopologicalSpace N]
+
+/-- The lift of a monoid hom from `M` to a monoid hom from `SeparationQuotient M`. -/
+@[to_additive "The lift of an additive monoid hom from `M` to an additive monoid hom from
+`SeparationQuotient M`."]
+noncomputable def liftContinuousMonoidHom [CommMonoid M] [ContinuousMul M] [CommMonoid N]
+    (f : ContinuousMonoidHom M N) (hf : ∀ x y, Inseparable x y → f x = f y) :
+    ContinuousMonoidHom (SeparationQuotient M) N where
+  toFun := SeparationQuotient.lift f hf
+  map_one' := map_one f
+  map_mul' := Quotient.ind₂ <| map_mul f
+  continuous_toFun := SeparationQuotient.continuous_lift.mpr f.2
+
+@[to_additive (attr := simp)]
+theorem liftContinuousCommMonoidHom_mk [CommMonoid M] [ContinuousMul M] [CommMonoid N]
+    (f : ContinuousMonoidHom M N) (hf : ∀ x y, Inseparable x y → f x = f y) (x : M) :
+    liftContinuousMonoidHom f hf (mk x) = f x := rfl
+
+end Monoid
+
+end SeparationQuotient