From 9341c08e4ef6a4d9ec046a0965ae9a5b4d2f3317 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 8 Oct 2024 23:23:08 +0000
Subject: [PATCH] feat: add `Normed` instances for SeparationQuotient (#17452)

We already have the corresponding metric spaces structures in `MetricSpace.Basic`.

This adds `Algebra`, `NormOneClass`, `Normed(Add)CommGroup`, `(Nonunital)Normed(Comm)Ring`, `NormedSpace`, and `NormedAlgebra` instances.

The slightly heavy imports here can be blamed on `Topology.Algebra.SeparationQuotient` importing `LinearAlgebra.Basis.VectorSpace` for the final 50-100 lines of the file. Moving this to a new file would cut the chain, as would generalizing it to work in free modules (continuing from #17560), assuming it actually holds there.
---
 Mathlib/Analysis/Normed/Field/Lemmas.lean     | 32 +++++++++++++++++--
 Mathlib/Analysis/Normed/Group/Basic.lean      | 10 ++++++
 Mathlib/Analysis/Normed/Group/Uniform.lean    | 23 +++++++++++++
 Mathlib/Analysis/Normed/Module/Basic.lean     |  7 ++++
 .../Topology/Algebra/SeparationQuotient.lean  | 21 ++++++++++++
 Mathlib/Topology/MetricSpace/Algebra.lean     |  7 ++++
 6 files changed, 98 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Field/Lemmas.lean b/Mathlib/Analysis/Normed/Field/Lemmas.lean
index 7b97a37837eb7..a2236fabdefec 100644
--- a/Mathlib/Analysis/Normed/Field/Lemmas.lean
+++ b/Mathlib/Analysis/Normed/Field/Lemmas.lean
@@ -148,7 +148,7 @@ instance Pi.normedCommutativeRing {π : ι → Type*} [Fintype ι] [∀ i, Norme
 end NormedCommRing
 
 -- see Note [lower instance priority]
-instance (priority := 100) semi_normed_ring_top_monoid [NonUnitalSeminormedRing α] :
+instance (priority := 100) NonUnitalSeminormedRing.toContinuousMul [NonUnitalSeminormedRing α] :
     ContinuousMul α :=
   ⟨continuous_iff_continuousAt.2 fun x =>
       tendsto_iff_norm_sub_tendsto_zero.2 <| by
@@ -174,9 +174,37 @@ instance (priority := 100) semi_normed_ring_top_monoid [NonUnitalSeminormedRing
 
 -- see Note [lower instance priority]
 /-- A seminormed ring is a topological ring. -/
-instance (priority := 100) semi_normed_top_ring [NonUnitalSeminormedRing α] :
+instance (priority := 100) NonUnitalSeminormedRing.toTopologicalRing [NonUnitalSeminormedRing α] :
     TopologicalRing α where
 
+namespace SeparationQuotient
+
+instance [NonUnitalSeminormedRing α] : NonUnitalNormedRing (SeparationQuotient α) where
+  __ : NonUnitalRing (SeparationQuotient α) := inferInstance
+  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
+  norm_mul := Quotient.ind₂ norm_mul_le
+
+instance [NonUnitalSeminormedCommRing α] : NonUnitalNormedCommRing (SeparationQuotient α) where
+  __ : NonUnitalCommRing (SeparationQuotient α) := inferInstance
+  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
+  norm_mul := Quotient.ind₂ norm_mul_le
+
+instance [SeminormedRing α] : NormedRing (SeparationQuotient α) where
+  __ : Ring (SeparationQuotient α) := inferInstance
+  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
+  norm_mul := Quotient.ind₂ norm_mul_le
+
+instance [SeminormedCommRing α] : NormedCommRing (SeparationQuotient α) where
+  __ : CommRing (SeparationQuotient α) := inferInstance
+  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
+  norm_mul := Quotient.ind₂ norm_mul_le
+
+instance [SeminormedAddCommGroup α] [One α] [NormOneClass α] :
+    NormOneClass (SeparationQuotient α) where
+  norm_one := norm_one (α := α)
+
+end SeparationQuotient
+
 section NormedDivisionRing
 
 variable [NormedDivisionRing α] {a : α}
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index 1eba1978859f4..04e1413e4bea8 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -770,6 +770,16 @@ theorem continuous_norm' : Continuous fun a : E => ‖a‖ := by
 theorem continuous_nnnorm' : Continuous fun a : E => ‖a‖₊ :=
   continuous_norm'.subtype_mk _
 
+set_option linter.docPrime false in
+@[to_additive Inseparable.norm_eq_norm]
+theorem Inseparable.norm_eq_norm' {u v : E} (h : Inseparable u v) : ‖u‖ = ‖v‖ :=
+  h.map continuous_norm' |>.eq
+
+set_option linter.docPrime false in
+@[to_additive Inseparable.nnnorm_eq_nnnorm]
+theorem Inseparable.nnnorm_eq_nnnorm' {u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊ :=
+  h.map continuous_nnnorm' |>.eq
+
 @[to_additive]
 theorem mem_closure_one_iff_norm {x : E} : x ∈ closure ({1} : Set E) ↔ ‖x‖ = 0 := by
   rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).le_iff_eq]
diff --git a/Mathlib/Analysis/Normed/Group/Uniform.lean b/Mathlib/Analysis/Normed/Group/Uniform.lean
index 7ec9757016b86..f8e72a4535b45 100644
--- a/Mathlib/Analysis/Normed/Group/Uniform.lean
+++ b/Mathlib/Analysis/Normed/Group/Uniform.lean
@@ -365,6 +365,29 @@ instance (priority := 100) SeminormedCommGroup.to_uniformGroup : UniformGroup E
 instance (priority := 100) SeminormedCommGroup.toTopologicalGroup : TopologicalGroup E :=
   inferInstance
 
+/-! ### SeparationQuotient -/
+
+namespace SeparationQuotient
+
+@[to_additive instNorm]
+instance instMulNorm : Norm (SeparationQuotient E) where
+  norm := lift Norm.norm fun _ _ h => h.norm_eq_norm'
+
+set_option linter.docPrime false in
+@[to_additive (attr := simp) norm_mk]
+theorem norm_mk' (p : E) : ‖mk p‖ = ‖p‖ := rfl
+
+@[to_additive]
+instance : NormedCommGroup (SeparationQuotient E) where
+  __ : CommGroup (SeparationQuotient E) := instCommGroup
+  dist_eq := Quotient.ind₂ dist_eq_norm_div
+
+set_option linter.docPrime false in
+@[to_additive (attr := simp) nnnorm_mk]
+theorem nnnorm_mk' (p : E) : ‖mk p‖₊ = ‖p‖₊ := rfl
+
+end SeparationQuotient
+
 @[to_additive]
 theorem cauchySeq_prod_of_eventually_eq {u v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n)
     (hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k) :
diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean
index b35a5c4e3baf1..d1bb26f18316d 100644
--- a/Mathlib/Analysis/Normed/Module/Basic.lean
+++ b/Mathlib/Analysis/Normed/Module/Basic.lean
@@ -119,6 +119,9 @@ instance Pi.normedSpace {ι : Type*} {E : ι → Type*} [Fintype ι] [∀ i, Sem
       NNReal.mul_finset_sup]
     exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _
 
+instance SeparationQuotient.instNormedSpace : NormedSpace 𝕜 (SeparationQuotient E) where
+  norm_smul_le := norm_smul_le
+
 instance MulOpposite.instNormedSpace : NormedSpace 𝕜 Eᵐᵒᵖ where
   norm_smul_le _ x := norm_smul_le _ x.unop
 
@@ -348,6 +351,10 @@ instance Pi.normedAlgebra {ι : Type*} {E : ι → Type*} [Fintype ι] [∀ i, S
 
 variable [SeminormedRing E] [NormedAlgebra 𝕜 E]
 
+instance SeparationQuotient.instNormedAlgebra : NormedAlgebra 𝕜 (SeparationQuotient E) where
+  __ : NormedSpace 𝕜 (SeparationQuotient E) := inferInstance
+  __ : Algebra 𝕜 (SeparationQuotient E) := inferInstance
+
 instance MulOpposite.instNormedAlgebra {E : Type*} [SeminormedRing E] [NormedAlgebra 𝕜 E] :
     NormedAlgebra 𝕜 Eᵐᵒᵖ where
   __ := instAlgebra
diff --git a/Mathlib/Topology/Algebra/SeparationQuotient.lean b/Mathlib/Topology/Algebra/SeparationQuotient.lean
index 9772c5b922683..83775bba6cbe3 100644
--- a/Mathlib/Topology/Algebra/SeparationQuotient.lean
+++ b/Mathlib/Topology/Algebra/SeparationQuotient.lean
@@ -333,6 +333,12 @@ instance instCommRing [CommRing R] [TopologicalRing R] :
   surjective_mk.commRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul mk_pow
     mk_natCast mk_intCast
 
+/-- `SeparationQuotient.mk` as a `RingHom`. -/
+@[simps]
+def mkRingHom [NonAssocSemiring R] [TopologicalSemiring R] : R →+* SeparationQuotient R where
+  toFun := mk
+  map_one' := mk_one; map_zero' := mk_zero; map_add' := mk_add; map_mul' := mk_mul
+
 end Ring
 
 section DistribSMul
@@ -375,6 +381,21 @@ def mkCLM : M →L[R] SeparationQuotient M where
 
 end Module
 
+section Algebra
+variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
+    [TopologicalSpace A] [TopologicalSemiring A] [ContinuousConstSMul R A]
+
+instance instAlgebra : Algebra R (SeparationQuotient A) where
+  toRingHom := mkRingHom.comp (algebraMap R A)
+  commutes' r := Quotient.ind fun a => congrArg _ <| Algebra.commutes r a
+  smul_def' r := Quotient.ind fun a => congrArg _ <| Algebra.smul_def r a
+
+@[simp]
+theorem mk_algebraMap (r : R) : mk (algebraMap R A r) = algebraMap R (SeparationQuotient A) r :=
+  rfl
+
+end Algebra
+
 section VectorSpace
 
 variable (K E : Type*) [DivisionRing K] [AddCommGroup E] [Module K E]
diff --git a/Mathlib/Topology/MetricSpace/Algebra.lean b/Mathlib/Topology/MetricSpace/Algebra.lean
index 724512392f31b..e185b9abdc3ba 100644
--- a/Mathlib/Topology/MetricSpace/Algebra.lean
+++ b/Mathlib/Topology/MetricSpace/Algebra.lean
@@ -6,6 +6,7 @@ Authors: Heather Macbeth
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.MetricSpace.Lipschitz
+import Mathlib.Topology.Algebra.SeparationQuotient
 
 /-!
 # Compatibility of algebraic operations with metric space structures
@@ -213,5 +214,11 @@ instance Prod.instBoundedSMul {α β γ : Type*} [PseudoMetricSpace α] [PseudoM
     max_le ((dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_left _ _) dist_nonneg)
       ((dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_right _ _) dist_nonneg)
 
+instance {α β : Type*}
+    [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [BoundedSMul α β] :
+    BoundedSMul α (SeparationQuotient β) where
+  dist_smul_pair' _ := Quotient.ind₂ <| dist_smul_pair _
+  dist_pair_smul' _ _ := Quotient.ind <| dist_pair_smul _ _
+
 -- We don't have the `SMul α γ → SMul β δ → SMul (α × β) (γ × δ)` instance, but if we did, then
 -- `BoundedSMul α γ → BoundedSMul β δ → BoundedSMul (α × β) (γ × δ)` would hold