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 725c803ee9

Import changes exceeding 2%

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

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.FinitePresentation	1072	1166	+94 (+8.77%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Smooth.Flat	2
23 files Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.Cyclotomic.Basic 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.Grassmannian Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing	3
11 files Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Sites.Etale 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.Unramified.Locus	4
Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor	7
19 files Mathlib.Algebra.Module.Presentation.Differentials Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmoothOfFree	16
Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite	94
Mathlib.RingTheory.Flat.IsBaseChange (new file)	1133
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (new file)	1135
Mathlib.Algebra.Category.ModuleCat.Ulift (new file)	1176
Mathlib.Algebra.Homology.DerivedCategory.Ext.Bijection (new file)	1305
Mathlib.Algebra.Category.ModuleCat.Ext.Ulift (new file)	1365
Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting (new file)	1722
Mathlib.Algebra.Category.ModuleCat.Ext.Finite (new file)	1723
Mathlib.Algebra.Category.ModuleCat.Baer (new file)	1727
Mathlib.Algebra.Category.ModuleCat.InjectiveDimension (new file)	1738
Mathlib.RingTheory.Gorenstein.Defs (new file)	1768
Mathlib.Algebra.Category.ModuleCat.Ext.BaseChange (new file)	1861
Mathlib.RingTheory.Regular.InjectiveDimension (new file)	2130
Mathlib.RingTheory.Gorenstein.Polynomial (new file)	2140

---

Declarations diff

+ Abelian.Ext.mapExactFunctor
+ Abelian.Ext.mapExactFunctor_add
+ Abelian.Ext.mapExactFunctor_eq_shiftedHom_map
+ Abelian.Ext.mapExactFunctor_zero
+ CategoryTheory.Abelian.Ext.isBaseChange_aux
+ CategoryTheory.Functor.mapCochainComplexSingleFunctor
+ CategoryTheory.InjectivePresentation.shortComplex
+ CategoryTheory.InjectivePresentation.shortComplex_shortExact
+ CategoryTheory.isBaseChange_hom
+ 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.mapExactFunctor_smul
+ Functor.mapExtAddHom
+ Functor.mapExtAddHom_apply
+ Functor.mapExtAddHom_coe
+ Functor.mapExtLinearMap
+ Functor.mapExtLinearMap_apply
+ Functor.mapExtLinearMap_coe
+ Functor.mapExtLinearMap_toAddMonoidHom
+ Functor.mapExt_bijective_of_preservesInjectiveObjects
+ Functor.mapExt_bijective_of_preservesProjectiveObjects
+ Functor.mapHomologicalComplex_map_exact
+ Functor.mapShiftedHom_singleδ
+ Functor.mapTriangleOfSESδ
+ IsBaseChange.comp_equiv
+ IsBaseChange.of_equiv_left
+ IsBaseChange.of_equiv_right
+ IsBaseChange.of_left_exact
+ IsBaseChange.of_right_exact
+ IsGorensteinLocalRing
+ IsGorensteinLocalRing.of_ringEquiv
+ IsGorensteinRing
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ IsLocalRing.ResidueField.map_injective
+ LinearMap.shortComplexKer
+ LinearMap.shortExact_shortComplexKer
+ Module.FinitePresentation.exists_fin'
+ Module.FinitePresentation.isBaseChange_map
+ Module.exists_finite_presentation
+ Module.finite_shrink
+ Module.free_shrink
+ 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.finite_ext
+ ModuleCat.iso_extendScalars'_of_isBaseChange
+ ModuleCat.iso_extendScalars'_of_isBaseChange'
+ ModuleCat.projective_shortComplex
+ ModuleCat.projective_shortComplex_shortExact
+ ModuleCat.restrictScalars_additive
+ ModuleCat.restrictScalars_fullyFaithful_of_surjective
+ ModuleCat.restrictScalars_map_exact
+ ModuleCat.restrictScalars_map_exact'
+ ModuleCat.restrictScalars_preservesFiniteColimits
+ ModuleCat.restrictScalars_preservesFiniteLimits
+ Polynomial.isCM_of_isCM
+ Polynomial.localization_at_comap_maximal_isGorenstein_of_isGorenstein
+ WithBot.add_le_add_natCast_left_iff
+ WithBot.add_le_add_natCast_right_iff
+ WithBot.add_le_add_one_left_iff
+ WithBot.add_le_add_one_right_iff
+ WithBot.add_natCast_cancel
+ WithBot.add_one_cancel
+ WithBot.add_one_le_zero_iff_eq_bot'
+ WithBot.natCast_add_cancel
+ WithBot.one_add_cancel
+ WithTop.add_cast_cancel
+ WithTop.add_le_add_cast_iff_left
+ WithTop.add_le_add_cast_iff_right
+ WithTop.cast_add_cancel
+ descShortComplex_hom
+ exist_nat_eq'
+ extClass_comp_mapExt_bijective
+ extClass_postcomp_bijective_of_isSMulRegular
+ extClass_postcomp_surjective_of_projective_X₂
+ extClass_precomp_surjective_of_projective_X₂
+ extRestrictScalarsSemiLinearEquiv
+ extRestrictScalarsSemiLinearMap
+ extSemiLinearEquivOfSemiLinearEquiv_equal_universe
+ ext_quotient_one_subsingleton_iff
+ ext_residueField_subsingleton_iff
+ ext_subsingleton_of_all_gt
+ ext_subsingleton_of_quotients
+ ext_subsingleton_of_quotients'
+ ext_subsingleton_of_support_subset
+ ext_vanish_of_residueField_vanish
+ extendScalars'
+ extendScalars'_map_exact
+ fullyFaithfulUliftFunctor
+ hasInjectiveDimensionLT_of_linearEquiv
+ 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 (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) :
+ instance (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) [Linear R V] [Linear R W] [F.Linear R] :
+ 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 : (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism
+ instance : (ModuleCat.restrictScalars.{v} f).Additive
+ instance : (extendScalars' R S).Additive
+ instance : (restrictScalars (RingHomClass.toRingHom e)).IsEquivalence
+ instance : (uliftFunctor R).Additive
+ instance : (uliftFunctor.{v', v} R).Faithful := (fullyFaithfulUliftFunctor R).faithful
+ instance : (uliftFunctor.{v', v} R).Full := (fullyFaithfulUliftFunctor R).full
+ instance : (uliftFunctor.{v', v} R).Linear R
+ instance : Limits.PreservesFiniteColimits (ModuleCat.restrictScalars.{v} f) := by
+ instance : Limits.PreservesFiniteColimits (uliftFunctor.{v', v} R) := by
+ instance : Limits.PreservesFiniteLimits (ModuleCat.restrictScalars.{v} f) := by
+ instance : Limits.PreservesFiniteLimits (uliftFunctor.{v', v} R)
+ instance : Limits.PreservesLimitsOfSize.{v, v} (uliftFunctor.{v', v} R)
+ instance : NatTrans.CommShift F.mapDerivedCategoryFactors.symm.hom ℤ
+ instance [F.Linear R] : F.mapDerivedCategory.Linear R := by
+ instance [Linear R G] : Linear R (F ⋙ G)
+ instance [Module.Flat R S] : Limits.PreservesFiniteColimits (extendScalars' R S) := by
+ instance [Module.Flat R S] : Limits.PreservesFiniteLimits (extendScalars' R S) := by
+ instance [Small.{v} R] (M : ModuleCat.{v} R) : Module.Free R M.projective_shortComplex.X₂
+ instance [Small.{v} R] : (uliftFunctor.{v', v} R).PreservesInjectiveObjects
+ instance [Small.{v} R] : (uliftFunctor.{v', v} R).PreservesProjectiveObjects
+ instance [h : HasExt.{w'} D] (X Y : C) : HasSmallLocalizedShiftedHom.{w'}
+ instance {M : ModuleCat.{v} R} (ip : InjectivePresentation M) : Injective ip.shortComplex.X₂ := ip.2
+ instance {ι : Type*} (c : ComplexShape ι) :
+ instance {ι : Type*} (c : ComplexShape ι) : PreservesFiniteLimits (F.mapHomologicalComplex c) := by
+ isGorensteinLocalRing_def
+ isGorensteinLocalRing_iff_exists
+ isGorensteinRing_def
+ isGorensteinRing_def'
+ isGorensteinRing_of_ringEquiv
+ iso_restrictScalars
+ linear_of_full_essSurj_comp
+ mapDerivedCategorySingleFunctor
+ mapExactFunctor₀
+ mapExt_comp_eq_comp_mapExt
+ mapExt_extClass_eq_extClass_map
+ mapExt_mk₀_eq_mk₀_map
+ quotSMulTop_nontrivial''
+ quotientIsBaseChangeMap
+ quotientIsBaseChangeMap_isBaseChange
+ quotientSMulShortComplex
+ quotientSMulShortComplex_exact
+ quotientSMulShortComplex_shortExact_of_isSMulRegular
+ subsingleton_of_injective
+ subsingleton_of_projective
+ triangleOfSESδ_hom
+ triangle_mor₃_hom
+ uliftFunctor
+ uliftFunctorForgetIso
+ uliftFunctor_map_exact
- instance {E : Type*} [Category* E] [Preadditive E] [CategoryTheory.Linear R E] (G : D ⥤ E)

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 script/declarations_diff.sh contains some details about this script.

---

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

Current number	Change	Type
638	2	erw

Current commit 40582d9218
Reference commit 725c803ee9

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

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