feat(RingTheory): polynomial over Gorenstein ring is Gorenstein

[Thmoas-Guan]

In this PR, we prove that polynomial over Gorenstein ring is Gorenstein.

---

• depends on: feat(Homology): Ext commute with flat base change #33369
• depends on: feat(RingTheory): definition of Gorenstein local ring #31884
• depends on: feat(RingTheory): injective dimension of quotSMulTop #32098

[github-actions]

PR summary 2ff88851d5

Import changes exceeding 2%

%	File
+6.94%	Mathlib.Algebra.Module.FinitePresentation

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.FinitePresentation	1341	1434	+93 (+6.94%)

Import changes for all files

Files	Import difference
17 files Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Unramified.LocalStructure	2
32 files Mathlib.Algebra.Module.SpanRankOperations Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Extension.Cotangent.BaseChange Mathlib.RingTheory.Flat.Rank Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Quotient Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.ZariskisMainTheorem	3
11 files Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Unramified.Dedekind Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Locus	4
3 files Mathlib.RingTheory.LocalProperties.InjectiveDimension Mathlib.RingTheory.LocalProperties.ProjectiveDimension Mathlib.RingTheory.QuasiFinite.Polynomial	13
Mathlib.RingTheory.TotallySplit	15
12 files Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent	16
6 files Mathlib.Algebra.Module.Presentation.Differentials Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Smooth.Kaehler	17
3 files Mathlib.RingTheory.LocalProperties.Injective Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.Localization.Free	18
Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite	93
Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact (new file)	1182
Mathlib.RingTheory.Flat.IsBaseChange (new file)	1403
Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (new file)	1583
Mathlib.Algebra.Category.ModuleCat.Ext.Ulift (new file)	1685
Mathlib.Algebra.Category.ModuleCat.Ext.Baer (new file)	1923
Mathlib.Algebra.Category.ModuleCat.Ext.BaseChange (new file)	1939
Mathlib.Algebra.Category.ModuleCat.InjectiveDimension (new file)	1940
Mathlib.RingTheory.Gorenstein.Defs (new file)	1974
Mathlib.RingTheory.Regular.InjectiveDimension (new file)	2387
Mathlib.RingTheory.Gorenstein.Polynomial (new file)	2398

---

Declarations diff

+ CategoryTheory.Abelian.Ext.isBaseChange_aux
+ Ext.isBaseChange
+ Ext.isBaseChange'
+ Ext.isBaseChangeMap
+ Ext.isBaseChangeMap'
+ Ext.isBaseChangeMap_aux
+ Ext.isBaseChangeMap_aux'
+ Ext.isLocalizedModule
+ Ext.isLocalizedModule'
+ Ext.isLocalizedModuleMap
+ Ext.isLocalizedModuleMap'
+ ExtendScalars'.map'
+ ExtendScalars'.map'_comp
+ ExtendScalars'.map'_id
+ ExtendScalars'.obj'
+ Function.Bijective.subsingleton_congr
+ Functor.mapExt_bijective_of_preservesInjectiveObjects
+ Functor.mapExt_bijective_of_preservesProjectiveObjects
+ IsBaseChange.comp_equiv
+ IsBaseChange.iff_of_equiv_comm
+ IsBaseChange.of_left_exact
+ IsBaseChange.of_right_exact
+ IsGorensteinLocalRing
+ IsGorensteinLocalRing.of_ringEquiv
+ IsGorensteinRing
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ Module.FinitePresentation.exists_fin'
+ Module.FinitePresentation.isBaseChange_map
+ Module.isBaseChange_map_of_finite_free
+ ModuleCat.extLinearEquivOfLinearEquiv
+ ModuleCat.extSemiLinearEquivOfSemiLinearEquiv
+ ModuleCat.extUliftLinearEquiv
+ ModuleCat.extUliftLinearEquiv_toLinearMap
+ ModuleCat.extendScalars'.mapExtLinearMap
+ ModuleCat.extendScalars'.mapExtLinearMap_eq_mapExt
+ ModuleCat.extendScalars'_map_LinearMap
+ ModuleCat.extendScalars'_map_LinearMap_eq_mapAddHom
+ ModuleCat.isBaseChange_hom
+ ModuleCat.iso_extendScalars'_of_isBaseChange
+ ModuleCat.iso_extendScalars'_of_isBaseChange'
+ ModuleCat.restrictScalars_additive
+ ModuleCat.restrictScalars_fullyFaithful_of_surjective
+ ModuleCat.restrictScalars_map_exact
+ ModuleCat.restrictScalars_map_exact'
+ ModuleCat.restrictScalars_preservesFiniteColimits
+ ModuleCat.restrictScalars_preservesFiniteLimits
+ ModuleCat.shortComplexOfConj
+ ModuleCat.shortComplexOfConj_exact
+ ModuleCat.shortComplexOfConj_shortExact
+ Polynomial.isGorensteinRing_of_isGorensteinRing
+ Polynomial.localization_at_comap_maximal_isGorensteinLocalRing_of_isGorensteinLocalRing
+ comp_linearEquiv
+ compl₂_comp_linearEquiv
+ compl₂_linearEquiv
+ compr₂_linearEquiv
+ exact_conj_of_exact
+ exist_nat_eq'
+ extClass_comp_mapExt_bijective
+ extClass_postcomp_bijective_of_isSMulRegular
+ extRestrictScalarsSemiLinearEquiv
+ extRestrictScalarsSemiLinearMap
+ extSemiLinearEquivOfSemiLinearEquiv_equal_universe
+ ext_quotient_one_subsingleton_iff
+ ext_residueField_subsingleton_iff
+ ext_subsingleton_of_all_gt
+ ext_subsingleton_of_support_subset
+ ext_vanish_of_residueField_vanish
+ extendScalars'
+ extendScalars'_map_exact
+ hasInjectiveDimensionLE_of_quotients
+ hasInjectiveDimensionLT_of_linearEquiv
+ hasInjectiveDimensionLT_of_quotients
+ hasInjectiveDimensionLT_of_semiLinearEquiv
+ hasProjectiveDimensionLE_finsupp_quotient_regular
+ injectiveDimension_eq_of_linearEquiv
+ injectiveDimension_eq_of_semiLinearEquiv
+ injectiveDimension_eq_sInf_of_finite
+ injectiveDimension_lt_iff_of_finite
+ injectiveDimension_quotSMulTop_succ_eq_injectiveDimension
+ injective_of_subsingleton_ext_quotient_one
+ instance (M N : ModuleCat.{v'} S) : IsScalarTower R S (M ⟶ N)
+ instance (M N : ModuleCat.{v'} S) : Module R (M ⟶ N)
+ instance (M N : Type*) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
+ instance (n : ℕ) (M N : ModuleCat.{v'} S) : IsScalarTower R S (Ext M N n)
+ instance (n : ℕ) (M N : ModuleCat.{v'} S) : Module R (Ext M N n)
+ instance : (ModuleCat.restrictScalars.{v} f).Additive
+ instance : (extendScalars' R S).Additive
+ instance : (restrictScalars (RingHomClass.toRingHom e)).IsEquivalence
+ instance : Limits.PreservesFiniteColimits (ModuleCat.restrictScalars.{v} f) := by
+ instance : Limits.PreservesFiniteLimits (ModuleCat.restrictScalars.{v} f) := by
+ instance [Module.Flat R S] : Limits.PreservesFiniteColimits (extendScalars' R S) := by
+ instance [Module.Flat R S] : Limits.PreservesFiniteLimits (extendScalars' R S) := by
+ isGorensteinLocalRing_def
+ isGorensteinLocalRing_iff_exists
+ isGorensteinRing_def
+ isGorensteinRing_def'
+ isGorensteinRing_of_ringEquiv
+ iso_restrictScalars
+ quotientIsBaseChangeMap
+ quotientIsBaseChangeMap_isBaseChange
+ quotientSMulShortComplex
+ quotientSMulShortComplex_exact
+ quotientSMulShortComplex_shortExact_of_isSMulRegular

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.

---

Increase in tech debt: (relative, absolute) = (24.00, 0.00)

Current number	Change	Type
6439	24	backward.isDefEq.respectTransparency

Current commit 18683e0c2b
Reference commit 2ff88851d5

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Homology): Ext commute with flat base change #33369
• feat(RingTheory): definition of Gorenstein local ring #31884
• feat(RingTheory): injective dimension of quotSMulTop #32098
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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