fix(Analysis/Matrix): anchor the elementwise matrix norm's topology to instTopologicalSpaceMatrix

[dahlem]

With open scoped Matrix.Norms.Elementwise,

noncomputable example {m n : Type*} [Fintype m] [Fintype n] :
    Norm (Matrix m n ℝ →L[ℝ] Matrix m n ℝ) := inferInstance

fails to synthesize, even though the norm-induced topology on Matrix m n ℝ is definitionally equal to the ambient instTopologicalSpaceMatrix (rfl proves the equality).

What goes wrong: the →L[ℝ] type is elaborated with the direct instance instTopologicalSpaceMatrix, while ContinuousLinearMap.hasOpNorm's conclusion carries topologies that are projections of its SeminormedAddCommGroup arguments. During resolution, pending synthesis does find Matrix.seminormedAddCommGroup, but the projected topology then has to unify with instTopologicalSpaceMatrix, and the projection chain through fast_instance% Pi.seminormedAddCommGroup does not reduce to the same term. (Types like ℝ or EuclideanSpace don't hit this because they have no direct TopologicalSpace instance competing with the projection path — matrices do.)

Fix: anchor the topology field of Matrix.seminormedAddCommGroup / Matrix.normedAddCommGroup to instTopologicalSpaceMatrix via PseudoMetricSpace.replaceTopology / MetricSpace.replaceTopology with rfl proofs — the standard forgetful-inheritance pattern; the Frobenius family in the same file already achieves this through PiLp.seminormedAddCommGroupToPi. Anchoring to a freshly-elaborated inferInstanceAs <| TopologicalSpace (m → n → α) is not sufficient — the anchor must be the same instance term that appears in elaborated goal types, which is why this also adds public import Mathlib.Topology.Instances.Matrix (no cycle; that file only imports LinearAlgebra.Matrix.* and Topology.Algebra.*).

norm, dist, and the uniformity are untouched — only the packaging of the topology field changes, in the direction of the canonical instance. The fix works at Lean's default maxSynthPendingDepth. It also unblocks smul-continuity resolution in Fréchet-derivative developments over matrix codomains (HasFDerivAt.const_smul sites), where the goal's topology argument is the same non-reducing projection.

Motivation: hit in a downstream project (~4300 build jobs of matrix-valued Fréchet calculus) where ten files currently need local high-priority compat instances to work around this. A downstream repair cannot be shipped safely: boosting a repaired SeminormedAddCommGroup's priority steals ‖·‖ resolution from files mixing norm scopes (e.g. Matrix.Norms.L2Operator sections of a Davis–Kahan development silently re-resolve to the elementwise norm). The fix has to live in the instance definitions.

Validation: full lake build Mathlib passes with the change (8666 jobs), plus new regression tests in MathlibTest/MatrixNormTopology.lean (both rfl agreements, the Norm synthesis above, ‖f‖ usage, ContinuousConstSMul unification).

Open questions for reviewers:

• Should the linftyOp* family get the same anchor for uniformity of design?
• Is letI I := fast_instance% …; { I with … } the preferred spelling here?
• Is the added import acceptable, or should the anchored instances move to a file that already sees Topology.Instances.Matrix?

Disclosure: this PR was prepared with AI assistance (Claude); the diagnosis and fix were validated by the full mathlib build and the included regression tests.

🤖 Generated with Claude Code

[github-actions]

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]

PR summary 6441797742

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 6441797).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 6441797742
Reference commit 3de5ed81cc

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).