refactor: rename the diag name token to diagonal - #43494
Conversation
PR summary 8280979c1fImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (strong) |
|---|---|---|
| misnamed declarations: definition names with an underscore | 477 | 1 |
Current commit 8280979c1f
Reference commit 21118bea64
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.py pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
Bot
added
the
file-removed
wrenna-robson
added
the
LLM-generated
github-actions
Bot
removed
the
file-removed
|
How about a separate PR per area or per def? And also one PR at a time, to avoid wasting your time if the maintainers change their mind. (I'd start with the |
|
Thanks for doing this clean-up! With my maintainer hat on, may I ask you do to two things:
|
I would frankly find this a lot more unmanageable to do. |
|
@grunweg Certainly: I believe this is the thread. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/antidiagonal.20vs.20antidiag/with/622080434 I was working on #38380, entirely ignorant of this until a few days ago. In terms of breaking up this PR: I can do that, though I will wait until I have a working build first (a lot easier to do that way). My strategy for this thus far has been to throw Claude at it because it's tedious work but essentially is just a matter of renaming things and fixing downstream issues. To be clear - I'm not using Claude to generate this text (that would be IMO quite rude)! But in my experience a big "touch-everything" PR like this is something it is quite useful to have machine-assistance with. There are some PRs I want to do on top of this. #38380 will rename Set.diagonal and add in a new Set.diagonal to match Finseet.diagonal (err, which is currently Finset.diag). I haven't touched Matrixdiag and Matrix.diagonal in this because it is unclear exactly what they should be (there was some different of opinions). I think there are a few places where "diag" means "diagram" and I think it would make sense to do that, but that isn't part of this PR. This PR is just "rename everything called diag/offDiag and similar" (with the caveat that Function.diag becomes Prod.diagonal because it should always have been in Prod. namespace - that's my error). Let me land this so that CI works, and then we can look at where we are, and I'll perhaps seek to break it up. I don't think it ought to be too bad to review - as long as you check the redefinitions are OK, everything else is just downstream of that. |
I'm confused as to how your opinion changed that fast, but I'm happy that we all agree :) |
There's no contradiction - I would find it a lot more unmanageable, but I am trying to be a considerate community member and show willing. It just means it will take a lot, lot longer. |
|
@grunweg Alright, I'm running green. If you do want this split up, how would you like that to be done? I'm minded to rebase the branch so that the history is more easily reviewable, if you're happy for it all to be on this PR. |
d37bfad to
e133a78
Compare
|
Could you avoid renaming (and deprecating) any files in this PR, to not break their git history? Ideally they should only move after the declaration renames are complete, and then the old modules reintroduced in a 3rd PR. |
9163797 to
66b2038
Compare
Ah, so maintain Diag in file names for this PR and then follow up with that later? |
|
I've (alright, Claude did with my supervising gently to make it actually do the work during my morning meeting) reorged the commits so that they're more logically separate. |
…iagonal)
`Function.diag` (the map `a ↦ (a, a)`) is renamed to `Prod.diagonal` and
moved into the `Prod` namespace, alongside its lemmas (`diag_apply` →
`Prod.diagonal_apply`, etc.) and the downstream map lemmas `tendsto_diag`,
`continuous_diag`, `measurable_diag`, `tendsto_diag_uniformity`,
`Eventually.diag_of_prod{,_left,_right}`, `FiberBundle.Prod.isInducing_diag`,
`Function.diag_def` (in `Kernel.Deterministic`), plus the collision fix in
`Topology/Algebra/ProperAction/Basic.lean` where the bare `diagonal` had
become ambiguous with the pre-existing `Set.diagonal`.
Deprecated aliases are provided for every renamed declaration, and the alias
for `Function.diag` is kept `protected` to match the original declaration
(otherwise `open Function` reintroduces `diag` ambiguously).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
`Set.offDiag`, `Finset.diag`/`Finset.offDiag`, `List.offDiag` and the off-diagonal lemmas on `Set`/`Finset`/`List`: `offDiag` → `offDiagonal`, `Finset.diag` → `Finset.diagonal` (built from `Prod.diagonal`, renamed in the previous commit). The declarations stay in `Data/List/OffDiag.lean`; the module itself is not renamed in this PR (that can follow once the declaration renames have landed). Also covers the two `Finset.diag` call sites that don't touch `Sym2` and so belong here rather than with the `Sym2` commit: `Finset.prod_diag`/`sum_diag` and `A_maps_to_offDiag_judgePair` in `Archive/Imo1998Q2`. Deprecated aliases are provided for every renamed declaration, including a few missed on the first pass (`Set.Nontrivial.offDiag_nonempty`, `Set.Subsingleton.offDiag_eq_empty`). Also fixes an unrelated `diagaonal` typo in the Cartan matrix lemma names in `RootSystem/CartanMatrix.lean`. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
…tream) * `Sym2.diag` → `Sym2.diagonal`, `Sym2.IsDiag` → `Sym2.IsDiagonal`, `Sym2.diagElem` → `Sym2.diagonalElem`, `Sym2.diagSet` → `Sym2.diagonalSet`, and all `isDiag_*` / `IsDiag.*` / `*_isDiag` lemmas, with fallout through `Combinatorics/SimpleGraph/*` (`not_isDiag_of_mem_edgeSet`, `edgeSet_subset_compl_diagSet`, …), including the dot-notation alias `Sym2.IsDiag.not_mem_edgeSet` which needed re-adding under the new `Sym2.IsDiagonal` namespace to keep firing. * The `Finset`-of-`Sym2` API (`Finset.diag`/`offDiag` restated for `Sym2`, `QuadraticForm` polarisation) that's built on both renames together. Deprecated aliases for every renamed declaration; long lines re-wrapped; `scripts/nolints.json` updated for the renamed `Sym2` instances/defs. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
Rename the `antidiag` name token to `antidiagonal` throughout: * `Finset.piAntidiag` → `Finset.piAntidiagonal` * `Finset.finsuppAntidiag` → `Finset.finsuppAntidiagonal` (+ `…Equiv`, `…EquivSubtype`) * `Finset.finMulAntidiag` → `Finset.finMulAntidiagonal` * `Nat.Partition.toFinsuppAntidiag` → `toFinsuppAntidiagonal` * `Int.divisorsAntidiag` → `Int.divisorsAntidiagonal` (+ lemmas) * `MonoidAlgebra.coeff_mul_antidiag` / `AddMonoidAlgebra.coeff_mul_antidiag` → `…coeff_mul_antidiagonal` The declarations stay in their existing `Mathlib/Algebra/Order/Antidiag/*.lean` modules; the modules themselves are not renamed in this PR (that can follow once the declaration renames have landed). `docs/1000.yaml` is updated to point the Multinomial theorem entry at the renamed `…_piAntidiagonal_of_commute`. Every renamed declaration gets a `@[deprecated (since := "2026-09-06")]` alias (dropping the redundant explicit `to_additive` name where it's exactly what `to_additive` autogenerates, and the alias mkalias generated for the private, unreferenceable `card_finMulAntidiagonal_pi`). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
…l decls)
Rename the `diag` name token where it abbreviates "diagonal" in the core
`CategoryTheory` diagonal-of-an-object construction and its consequences:
* `CategoryTheory.Limits.diag`/`codiag` → `diagonal`/`codiagonal`, then
further namespaced as `Limits.prod.diagonal`/`Limits.coprod.codiagonal`
(matching its own lemma prefixes `prod.diagonal_map`,
`coprod.map_codiagonal`, …) once the plain `diagonal` name collided with
`pullback.diagonal` via `open pullback` in `Limits/Shapes/Diagonal.lean`;
the `Limits.diag`/`Limits.codiag` deprecated aliases are retargeted
accordingly, with downstream uses in `ModelCategory/Cylinder.lean` and
`ModelCategory/PathObject.lean` updated to match.
* `CategoryTheory.Functor.diag` → `Functor.diagonal`
* `IsSubterminal.isIso_diag`/`isoDiag`/`isSubterminal_of_isIso_diag` → `…diagonal…`
* `Abelian.NonPreadditive` `diag_σ`, `Monoidal.Functor` `diag_ε/η/μ/δ` → `diagonal_*`
* `StructuredArrow`/`CostructuredArrow.ofDiagEquivalence(') ` → `ofDiagonalEquivalence(')`
* `Functor.{final,initial}_diag_of_isFiltered` → `…_diagonal_…`
* `externalProductCompDiagIso` → `externalProductCompDiagonalIso`
* `MorphismProperty.Representable` `of_diag`/`diag_iff`/`diag_of_map_from_obj` → `…diagonal…`
The `(Co)limitPresentation.diag` field and `Galois.EssSurj.quotientDiag` abbreviate
"diagram", not "diagonal", and are deliberately left untouched.
Every renamed declaration gets a `@[deprecated (since := "2026-09-06")]` alias.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
`TypeVec` `prod.diag`, `diagSub`, `fst_diag`, `snd_diag`, `dropFun_diag`, `diag_sub_val` → `…diagonal…`, with the downstream use in `QPF/Multivariate/Constructions/Cofix.lean` updated to match. This is the multivariate-QPF `TypeVec` machinery, unrelated to the core `CategoryTheory` diagonal construction renamed in the previous commit beyond sharing the `diag` token. Every renamed declaration gets a `@[deprecated (since := "2026-09-06")]` alias. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
Rename remaining `diag`-as-"diagonal" declarations outside Matrix/Set/uniformity: * `OrderHom.diag`/`onDiag` → `OrderHom.diagonal`/`onDiagonal` * `LinearMap.diag` (Pi) → `LinearMap.diagonal` (+ `single_eq_pi_diag`), which made the bare `diagonal` ambiguous with `Matrix.diagonal` in `RingTheory/MatrixPolynomialAlgebra.lean` and `LinearAlgebra/Matrix/Diagonal.lean`; qualified accordingly. Downstream reference in `RingTheory/Coalgebra/Basic.lean` updated to match. * `SimplexCategory.diag` → `SimplexCategory.diagonal` (+ `diag_subinterval_eq`), with the `SimplicialObject.diagonal`/`Quasicategory` call sites (which reference it, and became ambiguous where a file opens both `SimplicialObject` and `SimplexCategory`) updated and qualified to match. * `FormalMultilinearSeries.derivSeries_apply_diag`, `HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag` → `…_diagonal` * `SpecialLinearGroup.diag2`/`diag2n`/`diag2_*`/`diag_commute`/`diag_eq_diag2n_prod`/ `commutator_diag2_transvection` → `diagonal2`/`diagonal2n`/… * `diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne` → `diagonal_…` * `exteriorPower.ιMultiDual_apply_diag`/`_nondiag` → `…_diagonal`/`_nondiagonal` * `IsClub.diag` → `IsClub.diagonal` * `WittVector.IsPoly₂.diag` → `IsPoly₂.diagonal` * `Finset.prod_range_diag_flip`/`prod_prod_Ioi_mul_eq_prod_prod_off_diag` → `…diagonal…` * `TopPair.diag`/`proj₁AdjDiag` → `TopPair.diagonal`/`proj₁AdjDiagonal` Every renamed declaration gets a `@[deprecated (since := "2026-09-06")]` alias. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
* `Finset.piDiag` → `Finset.piDiagonal` (+ `mem_piDiag`, `card_piDiag`, `piDiag_subset_piFinset`) * `Nat.diag_induction` → `Nat.diagonal_induction` * `IsHeckeTriple.diag_left`/`diag_right` → `diagonal_left`/`diagonal_right` * `ContinuousMonoidHom.diag` → `ContinuousMonoidHom.diagonal` Every renamed declaration gets a `@[deprecated (since := "2026-09-06")]` alias. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CNPGZ1QMoRHjVquVwdfFTU
020d5e3 to
62bf013
Compare
|
@SnirBroshi should be clear now. |
4 participants
Per recent discussion on Zulip, we want to move away from
diagshould not be used as a name token. This renames every declaration wherediagabbreviates diagonal to spell it out in full, with a@[deprecated]alias for each. It also renames the directoryMathlib/Algebra/Order/Antidiag/toAntidiagonal/.I've tried to split it into reviewable commits by area (
Prod/offDiag,Sym2/Finset.diag,antidiag,CategoryTheory, misc, leftovers) plus a smalldiagaonaltypo fix. I will try and break it up into discrete sub-PRs if necessary.Out of scope, handled in follow-ups:
Set.diagonal/Prod.diagonalSet- to be handled in feat(Data/Set): addSet.diag#38380Matrix.diag/blockDiag/IsDiagconstructor/extractor swap - there's one or two of these where something is being constructed/extracted or wherediag-means-diagram cases ((Co)limitPresentation.diag,Galois.EssSurj.quotientDiag,CommDiag), which will be renamed todiagram🤖 Generated with Claude Code