feat(RingTheory/MvPowerSeries): various equivalences for MvPowerSeries

[BryceT233]

This PR adds a number of equivalences related to power series rings and is patterned after Mathlib/Algebra/MvPolynomial/Equiv.lean.

To be specific, it adds:

• MvPowerSeries.isEmptyEquiv : The isomorphism between multivariable power series
  in no variables and the ground ring.

• MvPowerSeries.uniqueEquiv : The isomorphism between multivariable power series
  in a single variable and power series over the ground ring.

• MvPowerSeries.mapEquiv, MvPowerSeries.mapAlgEquiv : The isomorhism between
  multivariable power series induced by an isomorphism between the coefficient rings.

• MvPowerSeries.sumAlgEquiv : The isomorphism between multivariable power series
  in a sum of two types, and multivariable power series in one of the types,
  with coefficients in multivariable power series in the other type.

• MvPowerSeries.commAlgEquiv : The isomorphism between multivariable power series
  in variables σ of multivariable power series in variables τ and multivariable power series
  in variables τ of multivariable power series in variables σ.

• MvPowerSeries.optionEquivLeft : The isomorphism between multivariable power series
  in Option σ and power series with coefficients in MvPowerSeries σ R.

• MvPowerSeries.optionEquivRight : The isomorphism between multivariable power series
  in Option σ and multivariable power series in σ with coefficients in PowerSeries R

• MvPowerSeries.finSuccEquiv : The isomorphism between multivariable power series
  in Fin (n + 1) and power series over multivariable power series in Fin n.

---

• depends on: [Merged by Bors] - feat(Data/Finsupp): add computational lemmas for cons and single #35329
• depends on: [Merged by Bors] - feat(Data/Finsupp): add lemmas for Finsupp and Sum #36506
• depends on: feat(RingTheory/MvPowerSeries): multivariable power series ring is a noetherian ring when the index is finite #40205

[github-actions]

PR summary 44c2bb9350

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coeff_coeff_finSuccEquiv
+ coeff_coeff_optionEquivLeft
+ coeff_coeff_optionEquivRight
+ coeff_coeff_optionFunLeft
+ coeff_coeff_optionFunRight
+ coeff_iterToSumFun
+ coeff_optionInvFunLeft
+ coeff_optionInvFunRight
+ coeff_sumAlgEquiv_symm_apply
+ coeff_sumToIter
+ coeff_sumToIterFun
+ coeff_uniqueEquiv
+ commAlgEquiv
+ commAlgEquiv_C
+ commAlgEquiv_X
+ congrAlgEquiv
+ congrAlgEquiv_refl
+ congrAlgEquiv_symm
+ congrAlgEquiv_trans
+ congrRingEquiv
+ congrRingEquiv_refl
+ congrRingEquiv_symm
+ congrRingEquiv_trans
+ embDomain_finSuccEquiv_cons
+ finSuccEquiv
+ finSuccEquiv_C
+ finSuccEquiv_X_succ
+ finSuccEquiv_X_zero
+ finSuccEquiv_comp_C
+ finSuccEquiv_renameEquiv_finSuccEquiv
+ image_optionElim_product_antidiagonal
+ isEmptyEquiv
+ iterToSumFun
+ map_injective
+ map_injective_iff
+ map_leftInverse
+ map_rightInverse
+ map_surjective
+ map_surjective_iff
+ optionEquivLeft
+ optionEquivLeft_C
+ optionEquivLeft_X_none
+ optionEquivLeft_X_some
+ optionEquivLeft_monomial
+ optionEquivRight
+ optionEquivRight_C
+ optionEquivRight_X_none
+ optionEquivRight_X_some
+ optionEquivRight_monomial
+ optionFunLeft
+ optionFunLeft_monomial
+ optionFunLeft_mul
+ optionFunRight
+ optionFunRight_monomial
+ optionFunRight_mul
+ optionInvFunLeft
+ optionInvFunRight
+ sumAlgEquiv
+ sumAlgEquiv_comp_rename_inl
+ sumAlgEquiv_comp_rename_inr
+ sumAlgEquiv_symm_C_C
+ sumAlgEquiv_symm_C_X
+ sumAlgEquiv_symm_X
+ sumToIter
+ sumToIterFun
+ sumToIterFun_monomial
+ sumToIterFun_mul
+ sumToIter_C
+ sumToIter_Xl
+ sumToIter_Xr
+ sumToIter_monomial
+ uniqueEquiv
+ uniqueEquiv_C
+ uniqueEquiv_X

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.

Current commit 44c2bb9350
Reference commit 97f12126be

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Data/Finsupp): add computational lemmas for cons and single #35329
• [Merged by Bors] - feat(Data/Finsupp): add lemmas for Finsupp and Sum #36506
• feat(RingTheory/MvPowerSeries): multivariable power series ring is a noetherian ring when the index is finite #40205
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

How many of these would you need if MvPowerSeries were defined as an abbrev for HahnSeries, and how many would generalise to HahnSeries?

[Thmoas-Guan]

How many of these would you need if MvPowerSeries were defined as an abbrev for HahnSeries, and how many would generalise to HahnSeries?

I have a question may be stupid: is HahnSeries really full generalization to MvPowerSeries?

My quetsion about generalization is : can it really cover all the usages? Also, if we wish to deduce these APIs from HahnSeries, is this definition with connected isomorphisms really pleasant?
If either is no, I think these constructions are needed and HahnSeries stuffs should be done in a separate PR and prove compatibilities?

[BryceT233]

How many of these would you need if MvPowerSeries were defined as an abbrev for HahnSeries, and how many would generalise to HahnSeries?

Thanks for the insightful question! I haven't worked much with HahnSeries before, but looking at it now, I can see how MvPowerSeries conceptually fits as a special case. To answer your question:

• mapEquiv part is not needed if it is done for HahnSeries since changing the coefficient ring does not affect the support.
• (from what gemini told me :)) sumAlgEquiv, commAlgEquiv conceptually corresponds to the isomorphism of iterated Hahn series: HahnSeries (Γ × Δ) R ≃ HahnSeries Γ (HahnSeries Δ R). While mathematically true, formalizing this would require dealing with the well-foundedness of supports under product orders. This feels like a substantial project on its own and might be out of scope for this current PR.
• The rest equivalences like isEmptyEquiv, uniqueEquiv, optionEquivLeft/Right, finSuccEquiv are meant to provide user-friendly APIs that mirrors MvPolynomial/Equiv.lean, I guess they are needed anyway even if MvPowerSeries were defined as an abbrev for HahnSeries.

[YaelDillies]

There's no semantic difference between MvPowerSeries and HahnSeries. What do you mean by "connected isomorphisms"? I am suggesting we make MvPowerSeries an abbrev for HahnSeries (with the correct arguments)

[Thmoas-Guan]

There's no semantic difference between MvPowerSeries and HahnSeries. What do you mean by "connected isomorphisms"? I am suggesting we make MvPowerSeries an abbrev for HahnSeries (with the correct arguments)

My fault, I am really being stupid here (misreading some of the commenst).
Then the only question I have is why the congruence for HahnSeries and MvPowerSeries only have finite index version? I was probably mislead by this issue.

[Thmoas-Guan]

Due to the differnt situations for different equivalences mentioned, I have an idea that maybe we should try to handle isEmptyEquiv, uniqueEquiv, optionEquivLeft/Right, finSuccEquiv first in this PR, then deal with other ones do having generalizations separately.

Also, I think the map injective/surjective stuffs are smoehow unrelated? Maybe we should split it also.

[YaelDillies]

Do you mean HahnSeries.toMvPowerSeries? I agree that this looks strangely specialised

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.