feat: add instances of MetricSpace, NormedAddGroup, and NormedAddCommGroup for DirectLimit by drocta · Pull Request #39673 · leanprover-community/mathlib4

drocta · 2026-05-21T21:34:00Z

add files Topology/MetricSpace/DirectLimit.lean (with an instance of MetricSpace for a DirectLimit of a directed system of MetricSpaces with IsometryClass map types between them) and Analysis/Normed/Group/DirectLimit.lean (with instances of NormedAddGroup and NormedAddCommGroup on DirectLimit)
also lemmas dist_def and norm_def for these.

This PR is part of a project of adding support for direct limits of $C^*$-algebras (as I described on Zulip ).
This PR uses IsometryClass to implement the requirement that the directed systems preserve the Norm on the NormedAddGroups, following the advice I got this Zulip thread .

Use of AI:
I again used ChatGPT a bit for some advice when writing this (for example, for ideas for simplifying parts of proofs that I suspected could be simpler/shorter, and for advice on which of a couple options would be more idiomatic).
I can personally vouch for all of these contributions, and that I understand this code.

… MetricSpace for a DirectLimit of MetricSpace s

…f_dist_eq_zero

…def by making an argument inferred

… dist_triangle in instance

… eq_of_dist_eq_zero in instance

… proof of eq_of_dist_eq_zero in instance

…edAddGroup s

…rom other instances

…ription and unnecessary arguments x y in rw step

…nstNormedAddCommGroup

…ctLimit.lean

… for NormedAddCommGroup as well

github-actions · 2026-05-21T21:34:10Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-05-21T21:35:15Z

PR summary 47f4c30346

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Topology.MetricSpace.DirectLimit` (new file)	1070
`Mathlib.Analysis.Normed.Group.DirectLimit` (new file)	1226
`Mathlib.Analysis.Normed.Ring.DirectLimit` (new file)	1293

Declarations diff

+ dist_def
+ edist_def
+ instance : EMetricSpace (DirectLimit G f)
+ instance : MetricSpace (DirectLimit G f)
+ instance : NonUnitalNormedRing (DirectLimit G f)
+ instance : NormedCommGroup (DirectLimit G f)
+ instance : NormedGroup (DirectLimit G f)
+ instance : NormedRing (DirectLimit G f)
+ instance : PseudoEMetricSpace (DirectLimit G f)
+ instance : PseudoMetricSpace (DirectLimit G f)
+ instance : SeminormedCommGroup (DirectLimit G f)
+ instance : SeminormedGroup (DirectLimit G f)
+ mul_enorm_def
+ mul_nnnorm_def
+ mul_norm_def
+ nndist_def

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

…r than between the imports and it

eric-wieser · 2026-05-22T00:27:33Z

+lemma 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


Could you add the nnnorm and enorm lemmas too?

For nnnorm_def/enorm_def, it looks like NormedGroup does not provide an NNNorm/ENorm instance?

SeminormedGroup.toNNNorm exists, so I'm not sure I agree.

Whoops, I assumed that if the instance existed it would already be in the scope of what I already had imported. Silly me. Thanks for the correction.

eric-wieser · 2026-05-22T00:27:57Z

+namespace NormedAddGroup
+
+variable [∀ i, NormedAddGroup (G i)]
+variable [∀ i j h, AddMonoidHomClass (T h) (G i) (G j)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance instNormedAddGroup : NormedAddGroup (DirectLimit G f) where


Does this also hold for SeminormedAddGroup? Can you to_additive it and use SeminormedGroup?

eric-wieser · 2026-05-22T00:29:05Z

+variable [∀ i, MetricSpace (G i)]
+variable [∀ i j h, IsometryClass (T h) (G i) (G j)]
+
+noncomputable instance : MetricSpace (DirectLimit G f) where


Does this genrealize to PseudoMetricSpace?

It does, yes. Will do.

Do you also want the instances for PseudoEMetricSpace and EMetricSpace?
(I believe copy/pasting the code and adding a handful of "e"s before things would make that work. I don't see a way to reduce redundancy by making the (Pseudo)MetricSpace instances use the (Pseudo)EMetricSpace code, or visa versa though. )

Yes, those would be great too; though perhaps slightly more work.

eric-wieser

I think it should be pretty easy to add the normed ring instances too, assuming they work how I think they do. Could you do that in this PR as well?

drocta · 2026-05-22T01:03:28Z

I think it should be pretty easy to add the normed ring instances too, assuming they work how I think they do. Could you do that in this PR as well?

Sure, can do, I was planning to make that be in a separate PR, but happy to do it in this one.

… the instance of MetricSpace, and making the instance of MetricSpace use it.

…it.lean

j-loreaux · 2026-05-22T02:01:31Z

I think this looks good modulo Eric's suggestions. Thanks!

… PseudoMetricSpace and MetricSpace into section blocks

…well as to_additive versions)

… excess whitespace

…move the separate instance (and namespace) specific to the NormedAddGroup version

…nce for NormedAddCommGroup with section and instance with to_additive of NormedCommGroup

eric-wieser · 2026-05-22T02:49:47Z

+  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)


I would guess you can drop this line now?

I can, if I replace the rw [lift₂_def] at h' with rw [dist_def] at h' .
Happy to make that change if preferred.
I had guessed (with low confidence) that it might be preferable to leave the definition of dist more directly exposed by doing it this way, but sounds like the other way around maybe?

We shouldn't define the distance twice, so please make that change.

eric-wieser · 2026-05-22T03:18:56Z

+  apply DirectLimit.lift_def
+
+end SeminormedGroup
+


I think you're missing SeminormedCommGroup?

eric-wieser · 2026-05-22T03:20:15Z

+
+See also `Metric.InductiveLimit` in `Mathlib/Topology/MetricSpace/Gluing.lean`, which
+handles sequential inductive limits of metric spaces.
+-/


Let's add a remark that for now the only uniform space and bornology available on a DirectLimit are the ones induced through the metric.

eric-wieser · 2026-05-22T03:32:59Z

+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]


Here you also need toTopologicalSpace := inferInstance, which will no doubt create a headache.

The test you need to pass (which we should commit) is:

example : (UniformSpace.toTopologicalSpace : TopologicalSpace (DirectLimit G f)) = instTopologicalSpaceQuotient := rfl

Sorry, I'm a bit confused here.
When I try to set toTopologicalSpace := inferInstance in there, it tells me that "toTopologicalSpace is not a field of structure PseudoMetricSpace" .

…f dist from the instance of PseudoMetricSpace instead of redefining it.

…ed.Group.Basic instead of Analysis.Normed.Group.Defs)

…d/Ring/DirectLimit.lean

drocta added 21 commits May 19, 2026 14:58

add Topology/MetricSpace/DirectLimit.lean, which gives an instance of…

bcf33a3

… MetricSpace for a DirectLimit of MetricSpace s

rename namespace, and change namespace for lemma

b8ce6ff

add a module docstring for Topology/MetricSpace/DirectLimit.lean

12f2b05

in Topology/MetricSpace/DirectLimit , slightly simplify proof of eq_o…

286d813

…f_dist_eq_zero

in Topology/MetricSpace/DirectLimit , slightly shorten proof of dist_…

fc170d6

…def by making an argument inferred

in Topology/MetricSpace/DirectLimit , shorten proofs of dist_comm and…

98c336a

… dist_triangle in instance

in Topology/MetricSpace/DirectLimit , shorten proofs of dist_self and…

b0e4bea

… eq_of_dist_eq_zero in instance

in Topology/MetricSpace/DirectLimit , move apostrophes for clarity in…

8e35650

… proof of eq_of_dist_eq_zero in instance

improve module docstring for Topology/MetricSpace/DirectLimit.lean

c243914

add instance of NormedAddGroup for DirectLimit

24ee6ab

add lemma DirectLimit.NormedAddGroup.norm_def for DirectLimit of Norm…

ea02f04

…edAddGroup s

add instance of NormedAddCommGroup for DirectLimit

b394832

add module docstring for Analysis/Normed/Group/DirectLimit.lean

d0e0b4f

make fields of instNormedAddCommGroup all be obtained by inheriting f…

b09c2aa

…rom other instances

whitespaces fixes in Analysis/Normed/Group/DirectLimit.lean

a5ce1cf

in Analysis/Normed/Group/DirectLimit.lean replace => with \mapsto

572df6a

in Analysis/Normed/Group/DirectLimit.lean remove unnecessary type asc…

4ab90f8

…ription and unnecessary arguments x y in rw step

use inferInstance rather than _ in the __ field for AddCommGroup in i…

e265879

…nstNormedAddCommGroup

rephrase module docstring in Analys/Normed/Group/DirectLimit.lean

5e688ed

remove more unnecessary type ascription in Analysis/Normed/Group/Dire…

2d606d8

…ctLimit.lean

remove example showing that DirectLimit.NormedAddGroup.norm_def works…

947769b

… for NormedAddCommGroup as well

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 21, 2026

github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label May 21, 2026

drocta added 2 commits May 21, 2026 14:50

run lake exe mk_all

12252bf

move the expose public section to be after the module docstring rathe…

0d08ac8

…r than between the imports and it

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Topology/MetricSpace/DirectLimit.lean

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Topology/MetricSpace/DirectLimit.lean Outdated

eric-wieser reviewed May 22, 2026

View reviewed changes

drocta added 2 commits May 21, 2026 18:05

make instance of PseudoMetricSpace for DirectLimit, pulling it out of…

579e942

… the instance of MetricSpace, and making the instance of MetricSpace use it.

add nndist_def and edist_def lemmas in Topology/MetricSpace/DirectLim…

0e28c84

…it.lean

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2026

drocta added 5 commits May 21, 2026 19:25

in Topology/MetricSpace/DirectLimit.lean changes the namespace blocks…

8203924

… PseudoMetricSpace and MetricSpace into section blocks

add instances of SeminormedGroup and NormedGroup for DirectLimit (as …

a74866d

…well as to_additive versions)

remove redundant instance of NormedGroup, and a #synth line, and some…

4703329

… excess whitespace

add @[to_additive] on instance of NormedGroup for DirectLimit, and re…

506ed18

…move the separate instance (and namespace) specific to the NormedAddGroup version

in Analysis/Normed/Group/DirectLimit.lean replace namespace and insta…

b5ef65e

…nce for NormedAddCommGroup with section and instance with to_additive of NormedCommGroup

eric-wieser reviewed May 22, 2026

View reviewed changes

drocta added 6 commits May 21, 2026 20:37

make the instance of MetricSpace for DirectLimit get the definition o…

f54956e

…f dist from the instance of PseudoMetricSpace instead of redefining it.

add lemmas mul_nnnorm_def and mul_enorm_def (and import Analysis.Norm…

fcbc4e5

…ed.Group.Basic instead of Analysis.Normed.Group.Defs)

add instances of (Pseudo)EMetricSpace to DirectLimit

40b3149

add instance of SeminormedCommGroup to DirectLimit

c6e97a3

add instances of NormedRing and NonUnitalNormedRing in Analysis/Norme…

a0c8075

…d/Ring/DirectLimit.lean

ran lake exe mk_all

47f4c30

		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)

Conversation

drocta commented May 21, 2026

Uh oh!

github-actions Bot commented May 21, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 47f4c30346

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

drocta commented May 22, 2026

Uh oh!

j-loreaux commented May 22, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented May 21, 2026 •

edited

Loading