feat(RingTheory/MvPowerSeries): introduce rename

[BryceT233]

This file establishes the rename operation on multivariate power series under a map with finite fibers,
which modifies the set of variables.

This file is patterned after 'Mathlib/Algebra/MvPolynomial/Rename.lean`

---

[github-actions]

PR summary c287e212ea

Import changes exceeding 2%

%	File
+4.58%	Mathlib.Data.Finsupp.Antidiagonal

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Finsupp.Antidiagonal	699	731	+32 (+4.58%)

Import changes for all files

Files	Import difference
Mathlib.Data.Finsupp.Antidiagonal	32
Mathlib.Order.Filter.TendstoCofinite (new file)	910
Mathlib.RingTheory.MvPowerSeries.Rename (new file)	1124

---

Declarations diff

+ Finsupp.mapDomain_tendstoCofinite
+ TendstoCofinite
+ TendstoCofinite.finite_preimage
+ TendstoCofinite.finite_preimage_singleton
+ coeff_embDomain_rename
+ coeff_killCompl
+ coeff_killComplFun
+ coeff_rename
+ coeff_renameFun
+ coeff_rename_eq_zero
+ comp
+ constantCoeff_rename
+ degree_comapDomain_le_of_canonicallyOrderedAdd
+ degree_mapDomain_eq_of_subsingletonAddUnits
+ embDomain_refl
+ embDomain_trans_apply
+ embedding
+ equiv
+ id
+ image_prodMap_embDomain_antidiagonal
+ isLowerSet_range_embDomain
+ killCompl
+ killComplFun
+ killComplFun_monomial_embDomain
+ killComplFun_monomial_eq_zero
+ killComplFun_mul
+ killCompl_C
+ killCompl_X
+ killCompl_X_eq_zero
+ killCompl_comp_rename
+ killCompl_map
+ killCompl_monomial_embDomain
+ killCompl_monomial_eq_zero
+ killCompl_rename_app
+ mapDomain
+ mapDomain_add
+ mapDomain_apply_eq_sum
+ mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits
+ mapDomain_eq_zero
+ mapDomain_smul
+ mapDomain_support_of_subsingletonAddUnits
+ mem_range_embDomain_iff
+ rename
+ renameEquiv
+ renameEquiv_refl
+ renameEquiv_symm
+ renameEquiv_trans
+ renameFun
+ renameFunAux
+ renameFunAux'
+ renameFunAuxImage
+ renameFun_monomial
+ renameFun_mul
+ rename_C
+ rename_X
+ rename_coe
+ rename_comp_rename
+ rename_id
+ rename_id_apply
+ rename_injective
+ rename_map
+ rename_monomial
+ rename_rename
+ tendstoCofinite_iff_finite_preimage_singleton
+ tendstoCofinite_of_finite
+ tendstoCofinite_of_injective

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./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).

[riccardobrasca]

I think consistency is a good think, so let's add it to mapDomain_apply_eq_zero_iff.

[BryceT233]

I've updated the files as suggested. Also, since this PR generalizes your previous work and ideas, I thought it was only appropriate to add your name to the authors list for the files.

[riccardobrasca]

Sorry for the very long time I took to make this review and thanks a lot! A couple of cosmetic comments and then it is ready to go.

bors d+

[riccardobrasca]

Suggested change

	variable [CommSemiring R] [CommSemiring S]
	variable [Semiring R] [Semiring S]

The very beginning works in this generality, why not (you may need to create a new section to avoid reintroducing R and S.)

[BryceT233]

I tested relaxing R and S to Semiring, and actually most of the file compiles fine if I only define rename as a RingHom. However, this will creates a discrepancy with the current definition of MvPolynomial.rename, which is defined as an AlgHom (requiring CommSemiring). I know there are ongoing works to relax the CommSemiring assumption in MvPolynomial as well. Given this context,should I:

1. Keep it as CommSemiring and AlgHom for now to maintain API symmetry with current MvPolynomial?
2. Go ahead with Semiring and RingHom for the general parts, and assume CommSemiring when defining AlgHom versions? (e. g. MvPowerSeries.renameₐ)

I prefer option 2, but what to you think?

[riccardobrasca]

Mmm, unless you have very good reasons I would say 1: people will almost use it in the CommSemiring case and it's nice to have the map as a bundled hom.

[riccardobrasca]

Can you add the inj version? See https://leanprover-community.github.io/contribute/naming.html#injectivity

[riccardobrasca]

Can you use R⟦τ⟧ in this docstring?

[mathlib-bors]

✌️ BryceT233 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.