feat(Mathlib/RingTheory/Ideal/Cotangent): Submodule.map definition of cotangent spaces

[sun123zxy]

This PR adds an alternative definition of the cotangent space as an image under the R-module quotient map.

---

Split from PR #33247

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

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.

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 7862cbdfda

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Ideal.Quotient.Operations	1166	1168	+2 (+0.17%)

Import changes for all files

Files

Import difference

80 files Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.Topology Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.Algebra.DirectSum.Idempotents Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Nilpotent Mathlib.Data.ZMod.QuotientRing Mathlib.Dynamics.Newton Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.RingTheory.AdicCompletion.Basic Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.AdicCompletion.Topology Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.DividedPowers.SubDPIdeal Mathlib.RingTheory.DualNumber Mathlib.RingTheory.Ideal.AssociatedPrime.Basic Mathlib.RingTheory.Ideal.MinimalPrime.Basic Mathlib.RingTheory.Ideal.MinimalPrime.Localization Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.Ideal.Quotient.Operations Mathlib.RingTheory.Idempotents Mathlib.RingTheory.Jacobson.Ideal Mathlib.RingTheory.Lasker Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.LocalSubring Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.NonLocalRing Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime.Basic Mathlib.RingTheory.Localization.Ideal Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.Nakayama Mathlib.RingTheory.Polynomial.ContentIdeal Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.RingTheory.Polynomial.Eisenstein.Criterion Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.Polynomial.Morse Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Exp Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.SimpleRing.Matrix Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.TensorProduct.Quotient Mathlib.RingTheory.Valuation.Quotient Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.Topology.Algebra.IsOpenUnits Mathlib.Topology.Sheaves.CommRingCat

2

---

Declarations diff

+ cotangentEquivSubmodule
+ cotangentSubmodule
+ quotientIdealSubmoduleEquivMap

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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