[Merged by Bors] - feat: Shrink instances for NormedSpace and ContinuousLinearEquiv

Mathlib.lean

@@ -1920,6 +1920,7 @@ public import Mathlib.Analysis.Normed.Module.RCLike.Extend
 public import Mathlib.Analysis.Normed.Module.RCLike.Real
 public import Mathlib.Analysis.Normed.Module.Ray
 public import Mathlib.Analysis.Normed.Module.Span
+public import Mathlib.Analysis.Normed.Module.TransferInstance
 public import Mathlib.Analysis.Normed.Module.WeakDual
 public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Analysis.Normed.Operator.Asymptotics
@@ -6677,10 +6678,12 @@ public import Mathlib.Topology.Algebra.Module.Multilinear.Topology
 public import Mathlib.Topology.Algebra.Module.PerfectPairing
 public import Mathlib.Topology.Algebra.Module.PerfectSpace
 public import Mathlib.Topology.Algebra.Module.PointwiseConvergence
+public import Mathlib.Topology.Algebra.Module.Shrink
 public import Mathlib.Topology.Algebra.Module.Simple
 public import Mathlib.Topology.Algebra.Module.Star
 public import Mathlib.Topology.Algebra.Module.StrongDual
 public import Mathlib.Topology.Algebra.Module.StrongTopology
+public import Mathlib.Topology.Algebra.Module.TransferInstance
 public import Mathlib.Topology.Algebra.Module.UniformConvergence
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 public import Mathlib.Topology.Algebra.Module.WeakDual

Mathlib/Analysis/Normed/Module/TransferInstance.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2025 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+module
+
+public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.Algebra.Group.TransferInstance
+public import Mathlib.Algebra.Module.TransferInstance
+
+/-!
+# Transfer algebraic structures across `Equiv`s
+
+In this file, we transfer a (pseudo-)metric space, (semi-)normed additive commutive group
+and normed space structures across an equivalence.
+This continues the pattern set in `Mathlib/Algebra/Module/TransferInstance.lean`.
+-/
+
+@[expose] public section
+
+variable {α β : Type*}
+
+namespace Equiv
+
+variable (e : α ≃ β)
+
+/-- Transfer a `Dist` across an `Equiv` -/
+protected abbrev dist (e : α ≃ β) : ∀ [Dist β], Dist α := ⟨fun x y ↦ dist (e x) (e y)⟩
+
+/-- Transfer a `PseudoMetricSpace` across an `Equiv` -/
+protected abbrev pseudometricSpace (e : α ≃ β) : ∀ [PseudoMetricSpace β], PseudoMetricSpace α :=
+  .induced e ‹_›
+
+/-- Transfer a `MetricSpace` across an `Equiv` -/
+protected abbrev metricSpace (e : α ≃ β) : ∀ [MetricSpace β], MetricSpace α :=
+  .induced e e.injective ‹_›
+
+/-- Transfer a `SeminormedAddCommGroup` across an `Equiv` -/
+protected abbrev seminormedAddCommGroup (e : α ≃ β) :
+    ∀ [SeminormedAddCommGroup β], SeminormedAddCommGroup α :=
+  letI := e.addCommGroup
+  { SeminormedAddCommGroup.induced _ _ e.addEquiv with toPseudoMetricSpace := e.pseudometricSpace }
+
+/-- Transfer a `NormedAddCommGroup` across an `Equiv` -/
+protected abbrev normedAddCommGroup (e : α ≃ β) :
+    ∀ [NormedAddCommGroup β], NormedAddCommGroup α :=
+  letI := e.addCommGroup
+  { NormedAddCommGroup.induced _ _ e.addEquiv e.injective
+    with toPseudoMetricSpace := e.pseudometricSpace }
+
+/-- Transfer `NormedSpace` across an `Equiv` -/
+protected abbrev normedSpace (𝕜 : Type*) [NormedField 𝕜] (e : α ≃ β) [SeminormedAddCommGroup β] :
+    let _ := Equiv.seminormedAddCommGroup e
+    ∀ [NormedSpace 𝕜 β], NormedSpace 𝕜 α :=
+  letI := e.seminormedAddCommGroup
+  letI := e.module 𝕜
+  .induced _ _ _ (e.linearEquiv _)
+
+end Equiv

Mathlib/Topology/Algebra/Module/Shrink.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+module
+
+public import Mathlib.Algebra.Module.Shrink
+public import Mathlib.Analysis.Normed.Module.TransferInstance
+-- XXX: for import reduction purposes, the file should be split in two, with these imports
+-- going into a second file. This does not seem warrented at the moment.
+public import Mathlib.Topology.Algebra.Module.TransferInstance
+public import Mathlib.Topology.Instances.Shrink
+public import Mathlib.Analysis.Normed.Module.Basic
+
+/-!
+# Transfer algebraic structures from `α` to `Shrink α`
+
+-/
+
+@[expose] public section
+
+namespace Shrink
+
+universe v
+variable {R 𝕜 α : Type*} [Small.{v} α] [Semiring R] [NormedField 𝕜]
+
+suppress_compilation
+
+instance [SeminormedAddCommGroup α] : SeminormedAddCommGroup (Shrink.{v} α) :=
+  (equivShrink α).symm.seminormedAddCommGroup
+
+instance [NormedAddCommGroup α] : NormedAddCommGroup (Shrink.{v} α) :=
+  (equivShrink α).symm.normedAddCommGroup
+
+instance [SeminormedAddCommGroup α] [NormedSpace 𝕜 α] : NormedSpace 𝕜 (Shrink.{v} α) :=
+  (equivShrink α).symm.normedSpace 𝕜
+
+variable (R α) in
+/-- Shrinking `α` to a smaller universe preserves the continuous module structure. -/
+@[simps!]
+def continuousLinearEquiv [AddCommMonoid α] [TopologicalSpace α] [Module R α] :
+    Shrink.{v} α ≃L[R] α := by
+  convert (equivShrink α).symm.continuousLinearEquiv R
+
+end Shrink

Mathlib/Topology/Algebra/Module/TransferInstance.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2025 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+module
+
+public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.Algebra.Module.TransferInstance
+public import Mathlib.Topology.Algebra.Module.Equiv
+
+/-!
+# Transfer algebraic structures across `Equiv`s
+
+In this file, we transfer a topological space and continuous linear equivalence structure
+across an equivalence.
+This continues the pattern set in `Mathlib/Algebra/Normed/Module/TransferInstance.lean`.
+-/
+
+@[expose] public section
+
+variable {R α β : Type*}
+
+namespace Equiv
+
+variable (e : α ≃ β)
+
+/-- Transfer a `TopologicalSpace` across an `Equiv` -/
+protected abbrev topologicalSpace (e : α ≃ β) : ∀ [TopologicalSpace β], TopologicalSpace α :=
+  .induced e ‹_›
+
+/-- An equivalence e : α ≃ β gives a homeomorphism α ≃ₜ β where the topological space structure
+on α is the one obtained by transporting the topological space structure on β back along e. -/
+def homeomorph (e : α ≃ β) [TopologicalSpace β] :
+    letI := e.topologicalSpace
+    α ≃ₜ β :=
+  letI := e.topologicalSpace
+  { e with
+    continuous_toFun := continuous_induced_dom
+    continuous_invFun := by convert continuous_coinduced_rng; exact e.coinduced_symm.symm }
+
+variable [TopologicalSpace β] [AddCommMonoid β] [Semiring R] [Module R β]
+
+variable (R) in
+/-- An equivalence `e : α ≃ β` gives a continuous linear equivalence `α ≃L[R] β`
+where the continuous `R`-module structure on `α` is the one obtained by transporting an
+`R`-module structure on `β` back along `e`.
+
+This is `e.linearEquiv` as a continuous linear equivalence. -/
+def continuousLinearEquiv (e : α ≃ β) :
+    letI := e.topologicalSpace
+    letI := e.addCommMonoid
+    letI := e.module R
+    α ≃L[R] β :=
+  letI := e.topologicalSpace
+  letI := e.addCommMonoid
+  letI := e.module R
+  { toLinearEquiv := e.linearEquiv _
+    __ := e.homeomorph }
+
+@[simp]
+lemma continuousLinearEquiv_toLinearEquiv (e : α ≃ β) :
+    let _ := e.topologicalSpace
+    let _ := e.addCommMonoid
+    let _ := e.module R
+    (e.continuousLinearEquiv R).toLinearEquiv = e.linearEquiv R := by rfl
+
+end Equiv

Mathlib/Topology/Instances/Shrink.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Logic.Small.Defs
 public import Mathlib.Topology.Defs.Induced
 public import Mathlib.Topology.Homeomorph.Defs
+public import Mathlib.Topology.Algebra.Module.TransferInstance
 
 /-!
 # Topological space structure on `Shrink X`
@@ -21,17 +22,12 @@ namespace Shrink
 
 noncomputable instance (X : Type u) [TopologicalSpace X] [Small.{v} X] :
     TopologicalSpace (Shrink.{v} X) :=
-  .coinduced (equivShrink X) inferInstance
+  (equivShrink X).symm.topologicalSpace
 
 /-- `equivShrink` as a homeomorphism. -/
-@[simps toEquiv]
+@[simps! toEquiv]
 noncomputable def homeomorph (X : Type u) [TopologicalSpace X] [Small.{v} X] :
-    X ≃ₜ Shrink.{v} X where
-  __ := equivShrink X
-  continuous_toFun := continuous_coinduced_rng
-  continuous_invFun := by
-    convert continuous_induced_dom
-    simp only [Equiv.invFun_as_coe, Equiv.induced_symm]
-    rfl
+    X ≃ₜ Shrink.{v} X :=
+  (equivShrink X).symm.homeomorph.symm
 
 end Shrink