feat: add instances of MetricSpace, NormedAddGroup, and NormedAddCommGroup for DirectLimit

Mathlib.lean

@@ -2117,6 +2117,7 @@ public import Mathlib.Analysis.Normed.Group.Constructions
 public import Mathlib.Analysis.Normed.Group.Continuity
 public import Mathlib.Analysis.Normed.Group.ControlledClosure
 public import Mathlib.Analysis.Normed.Group.Defs
+public import Mathlib.Analysis.Normed.Group.DirectLimit
 public import Mathlib.Analysis.Normed.Group.FunctionSeries
 public import Mathlib.Analysis.Normed.Group.Hom
 public import Mathlib.Analysis.Normed.Group.HomCompletion
@@ -2211,6 +2212,7 @@ public import Mathlib.Analysis.Normed.Order.Hom.Ultra
 public import Mathlib.Analysis.Normed.Order.Lattice
 public import Mathlib.Analysis.Normed.Order.UpperLower
 public import Mathlib.Analysis.Normed.Ring.Basic
+public import Mathlib.Analysis.Normed.Ring.DirectLimit
 public import Mathlib.Analysis.Normed.Ring.Finite
 public import Mathlib.Analysis.Normed.Ring.InfiniteProd
 public import Mathlib.Analysis.Normed.Ring.InfiniteSum
@@ -7817,6 +7819,7 @@ public import Mathlib.Topology.MetricSpace.CoveringNumbers
 public import Mathlib.Topology.MetricSpace.Defs
 public import Mathlib.Topology.MetricSpace.Dilation
 public import Mathlib.Topology.MetricSpace.DilationEquiv
+public import Mathlib.Topology.MetricSpace.DirectLimit
 public import Mathlib.Topology.MetricSpace.Equicontinuity
 public import Mathlib.Topology.MetricSpace.Gluing
 public import Mathlib.Topology.MetricSpace.GromovHausdorff

Mathlib/Analysis/Normed/Group/DirectLimit.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Matthew Corbelli. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matthew Corbelli
+-/
+module
+
+public import Mathlib.Analysis.Normed.Group.Basic
+public import Mathlib.Algebra.Colimit.DirectLimit
+public import Mathlib.Topology.MetricSpace.DirectLimit
+
+/-!
+# Direct Limit of normed additive groups
+
+We introduct instances of `NormedAddGroup` and `NormedAddCommGroup` on `DirectLimit`,
+under the assumption that the types `T h` that the maps in the directed system come from,
+all have instances of `IsometryClass`.
+-/
+
+@[expose] public section
+
+namespace DirectLimit
+
+variable {ι : Type*} [Preorder ι] {G : ι → Type*}
+variable {T : ∀ ⦃i j : ι⦄, i ≤ j → Type*} {f : ∀ _ _ h, T h}
+variable [∀ i j (h : i ≤ j), FunLike (T h) (G i) (G j)] [DirectedSystem G (f · · ·)]
+variable [IsDirectedOrder ι]
+variable [Nonempty ι]
+
+section SeminormedGroup
+
+variable [∀ i, SeminormedGroup (G i)]
+variable [∀ i j h, MonoidHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+@[to_additive]
+noncomputable instance : SeminormedGroup (DirectLimit G f) where
+  norm := DirectLimit.lift f (ih := fun i x ↦ ‖x‖) (fun i j h x ↦ by
+    simpa [SeminormedGroup.dist_eq] using (IsometryClass.dist_eq (f i j h) 1 x).symm)
+  dist_eq := DirectLimit.induction₂ f (fun i x y ↦ by
+    rw [dist_def, SeminormedGroup.dist_eq, inv_def, mul_def, DirectLimit.lift_def])
+
+@[to_additive norm_def]
+lemma mul_norm_def (i : ι) (x : G i) : ‖(⟦⟨i, x⟩⟧ : DirectLimit G f)‖ = ‖x‖ := by
+  change DirectLimit.lift f (ih := fun i x ↦ ‖x‖) _ ⟦⟨i, x⟩⟧ = ‖x‖
+  apply DirectLimit.lift_def
+
+@[to_additive nnnorm_def]
+lemma mul_nnnorm_def (i : ι) (x : G i) : ‖(⟦⟨i, x⟩⟧ : DirectLimit G f)‖₊ = ‖x‖₊ := by
+  simp_rw [← @norm_toNNReal', mul_norm_def]
+
+@[to_additive enorm_def]
+lemma mul_enorm_def (i : ι) (x : G i) : ‖(⟦⟨i, x⟩⟧ : DirectLimit G f)‖ₑ = ‖x‖ₑ := by
+  rw [@enorm'_eq_iff_norm_eq,  mul_norm_def]
+
+end SeminormedGroup
+
+section NormedGroup
+
+variable [∀ i, NormedGroup (G i)]
+variable [∀ i j h, MonoidHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+@[to_additive]
+noncomputable instance : NormedGroup (DirectLimit G f) where
+  __ := (inferInstance : SeminormedGroup (DirectLimit G f))
+  __ := (inferInstance : MetricSpace (DirectLimit G f))
+
+end NormedGroup
+
+section SeminormedCommGroup
+
+variable [∀ i, SeminormedCommGroup (G i)]
+variable [∀ i j h, MonoidHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+@[to_additive]
+noncomputable instance : SeminormedCommGroup (DirectLimit G f) where
+  __ := (inferInstance : SeminormedGroup (DirectLimit G f))
+  __ := (inferInstance : CommGroup (DirectLimit G f))
+
+end SeminormedCommGroup
+
+section NormedCommGroup
+
+variable [∀ i, NormedCommGroup (G i)]
+variable [∀ i j h, MonoidHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+@[to_additive]
+noncomputable instance : NormedCommGroup (DirectLimit G f) where
+  __ := (inferInstance : NormedGroup (DirectLimit G f))
+  __ := (inferInstance : CommGroup (DirectLimit G f))
+
+end NormedCommGroup
+
+end DirectLimit

Mathlib/Analysis/Normed/Ring/DirectLimit.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Matthew Corbelli. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matthew Corbelli
+-/
+module
+
+public import Mathlib.Analysis.Normed.Group.DirectLimit
+public import Mathlib.Analysis.Normed.Ring.Basic
+public import Mathlib.Algebra.Colimit.DirectLimit
+
+/-!
+# Direct Limit of normed rings
+
+We introduct instances of `NormedRing` and `NonUnitalNormedRing` on `DirectLimit`,
+under the assumption that the types `T h` that the maps in the directed system come from,
+all have instances of `IsometryClass`.
+-/
+
+@[expose] public section
+
+namespace DirectLimit
+
+variable {ι : Type*} [Preorder ι] {G : ι → Type*}
+variable {T : ∀ ⦃i j : ι⦄, i ≤ j → Type*} {f : ∀ _ _ h, T h}
+variable [∀ i j (h : i ≤ j), FunLike (T h) (G i) (G j)] [DirectedSystem G (f · · ·)]
+variable [IsDirectedOrder ι]
+variable [Nonempty ι]
+
+section NonUnitalNormedRing
+
+variable [∀ i, NonUnitalNormedRing (G i)]
+variable [∀ i j h, NonUnitalRingHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : NonUnitalNormedRing (DirectLimit G f) where
+  __ := (inferInstance : NormedAddCommGroup (DirectLimit G f))
+  __ := (inferInstance : NonUnitalRing (DirectLimit G f))
+  norm_mul_le := DirectLimit.induction₂ f
+    fun i x y ↦ by simp_rw [mul_def, norm_def]; exact norm_mul_le x y
+
+end NonUnitalNormedRing
+
+section NormedRing
+
+variable [∀ i, NormedRing (G i)]
+variable [∀ i j h, RingHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : NormedRing (DirectLimit G f) where
+  __ := (inferInstance : Ring (DirectLimit G f))
+  __ := (inferInstance : NonUnitalNormedRing (DirectLimit G f))
+
+end NormedRing
+
+
+end DirectLimit

Mathlib/Topology/MetricSpace/DirectLimit.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2026 Matthew Corbelli. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matthew Corbelli
+-/
+module
+
+public import Mathlib.Order.DirectedInverseSystem
+public import Mathlib.Topology.MetricSpace.Isometry
+
+/-!
+# Metrics on direct limits
+
+This file defines a `MetricSpace` instance on `DirectLimit G f` when `G` and `f` form a directed
+system of metric spaces and the transition maps `f` are isometries (using `IsometryClass`).
+
+See also `Metric.InductiveLimit` in `Mathlib/Topology/MetricSpace/Gluing.lean`, which
+handles sequential inductive limits of metric spaces.
+-/
+@[expose] public section
+
+namespace DirectLimit
+
+variable {ι : Type*} [Preorder ι] {G : ι → Type*}
+variable {T : ∀ ⦃i j : ι⦄, i ≤ j → Type*} {f : ∀ _ _ h, T h}
+variable [∀ i j (h : i ≤ j), FunLike (T h) (G i) (G j)] [DirectedSystem G (f · · ·)]
+variable [IsDirectedOrder ι]
+
+section PseudoEMetricSpace
+
+variable [∀ i, PseudoEMetricSpace (G i)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : PseudoEMetricSpace (DirectLimit G f) where
+  edist := DirectLimit.lift₂ f f (fun i ↦ edist (α := G i))
+    (fun i j h x y ↦ (IsometryClass.edist_eq (f i j h) x y).symm)
+  edist_self := DirectLimit.induction f fun i x ↦ by rw [← edist_self x, lift₂_def]
+  edist_comm := DirectLimit.induction₂ f fun i x y ↦ by simp_rw [lift₂_def, edist_comm x y]
+  edist_triangle := DirectLimit.induction₃ f fun i x y z ↦ by simp_rw [lift₂_def, edist_triangle]
+
+lemma edist_def (i : ι) (x y : G i) :
+    edist (α := DirectLimit G f) ⟦⟨i,x⟩⟧ ⟦⟨i,y⟩⟧ = edist x y := by
+  change DirectLimit.lift₂ f f _
+    (fun i j h x y ↦ (IsometryClass.edist_eq (f i j h) x y).symm)
+    ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = edist x y
+  rw [lift₂_def]
+
+end PseudoEMetricSpace
+
+section EMetricSpace
+
+variable [∀ i, EMetricSpace (G i)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : EMetricSpace (DirectLimit G f) where
+  __ := (inferInstance : PseudoEMetricSpace (DirectLimit G f))
+  eq_of_edist_eq_zero {x y} h := DirectLimit.induction₂ f (fun i x' y' h' ↦ by
+    rw [edist_def] at h'
+    simp [eq_of_edist_eq_zero h']) x y h
+
+end EMetricSpace
+
+section PseudoMetricSpace
+
+variable [∀ i, PseudoMetricSpace (G i)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : PseudoMetricSpace (DirectLimit G f) where
+  dist := DirectLimit.lift₂ f f (fun i ↦ dist (α := G i))
+    (fun i j h x y ↦ (IsometryClass.dist_eq (f i j h) x y).symm)
+  dist_self := DirectLimit.induction f fun i x ↦ by rw [← dist_self x, lift₂_def]
+  dist_comm := DirectLimit.induction₂ f fun i x y ↦ by simp_rw [lift₂_def, dist_comm x y]
+  dist_triangle := DirectLimit.induction₃ f fun i x y z ↦ by simp_rw [lift₂_def, dist_triangle]
+
+lemma dist_def (i : ι) (x y : G i) :
+    dist (α := DirectLimit G f) ⟦⟨i,x⟩⟧ ⟦⟨i,y⟩⟧ = dist x y := by
+  change DirectLimit.lift₂ f f _
+    (fun i j h x y ↦ (IsometryClass.dist_eq (f i j h) x y).symm)
+    ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = dist x y
+  rw [lift₂_def]
+
+lemma nndist_def (i : ι) (x y : G i) :
+    nndist (α := DirectLimit G f) ⟦⟨i,x⟩⟧ ⟦⟨i,y⟩⟧ = nndist x y := by
+  simp_rw [nndist_dist, dist_def]
+
+end PseudoMetricSpace
+
+section MetricSpace
+
+variable [∀ i, MetricSpace (G i)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : MetricSpace (DirectLimit G f) where
+  __ := (inferInstance : PseudoMetricSpace (DirectLimit G f))
+  eq_of_dist_eq_zero {x y} h := DirectLimit.induction₂ f (fun i x' y' h' ↦ by
+    rw [dist_def] at h'
+    simp [eq_of_dist_eq_zero h']) x y h
+
+end MetricSpace
+
+end DirectLimit