feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version)#29703
feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version)#29703Thmoas-Guan wants to merge 2354 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
large-import
PR summary 52b9aaf523Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.Regular.Category | 1468 | 1953 | +485 (+33.04%) |
| Mathlib.RingTheory.Regular.Depth | 1796 | 2244 | +448 (+24.94%) |
| Mathlib.Algebra.Module.SpanRank | 1269 | 1284 | +15 (+1.18%) |
Import changes for all files
| Files | Import difference |
|---|---|
78 filesMathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.LocalStructure Mathlib.RingTheory.Unramified.Locus Mathlib.Topology.Algebra.Ring.Compact |
1 |
45 filesMathlib.Algebra.Module.Presentation.Differentials Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Extension.Presentation.Basic Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Pi |
2 |
8 filesMathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.RingTheory.Extension.Basic Mathlib.RingTheory.Extension.Generators Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct |
3 |
Mathlib.RingTheory.PowerSeries.Ideal |
12 |
Mathlib.Algebra.Module.SpanRank |
15 |
Mathlib.RingTheory.Regular.Depth |
448 |
Mathlib.RingTheory.Regular.Category |
485 |
Mathlib.RingTheory.RegularLocalRing.Defs (new file) |
1842 |
Mathlib.RingTheory.RegularLocalRing.RegularRing.Basic (new file) |
1843 |
Mathlib.RingTheory.RegularLocalRing.RegularRing.Polynomial (new file) |
1860 |
Mathlib.RingTheory.RegularLocalRing.Basic (new file) |
1868 |
Mathlib.Algebra.Category.ModuleCat.Baer (new file) |
1886 |
Mathlib.RingTheory.LocalProperties.ProjectiveDimension (new file) |
2055 |
Mathlib.RingTheory.GlobalDimension (new file) |
2060 |
Mathlib.RingTheory.Regular.Ischebeck (new file) |
2285 |
Mathlib.RingTheory.Regular.AuslanderBuchsbaum (new file) |
2330 |
Mathlib.RingTheory.CohenMacaulay.Basic (new file) |
2389 |
Mathlib.RingTheory.CohenMacaulay.Maximal (new file) |
2393 |
Mathlib.RingTheory.RegularLocalRing.GlobalDimension (new file) |
2417 |
Mathlib.RingTheory.RegularLocalRing.RegularRing.GlobalDimension (new file) |
2419 |
Mathlib.RingTheory.RegularLocalRing.RegularRing.Syzygy (new file) |
2425 |
Declarations diff
+ AuslanderBuchsbaum
+ AuslanderBuchsbaum_one
+ CategoryTheory.Abelian.Ext.pow_mono_of_mono
+ CategoryTheory.Abelian.Ext.smul_id_postcomp_eq_zero_of_mem_ann
+ FG.spanRank_eq_spanFinrank
+ Hilberts_Syzygy
+ Ideal.depth
+ Ideal.depth_eq_of_iso
+ Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+ IsCohenMacaulayLocalRing
+ IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing
+ IsCohenMacaulayRing
+ IsCohenMacaulayRing.of_isCohenMacaulayLocalRing
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ IsLocalRing.ResidueField.map_injective
+ IsLocalRing.depth
+ IsLocalRing.depth_eq_of_algebraMap_surjective
+ IsLocalRing.depth_eq_of_iso
+ IsLocalRing.depth_eq_of_ringEquiv
+ IsLocalRing.depth_eq_sSup_length_regular
+ IsLocalRing.depth_quotSMulTop_succ_eq_moduleDepth
+ IsLocalRing.depth_quotient_regular_sequence_add_length_eq_depth
+ IsLocalRing.depth_quotient_regular_succ_eq_depth
+ IsLocalRing.depth_quotient_span_regular_succ_eq_depth
+ IsLocalRing.ideal_depth_eq_sSup_length_regular
+ IsLocalRing.ideal_depth_le_depth
+ IsRegularLocalRing
+ IsRegularLocalRing.globalDimension_eq_ringKrullDim
+ IsRegularLocalRing.of_isDVR
+ IsRegularLocalRing.of_isField
+ IsRegularLocalRing.of_isRegularRing
+ IsRegularRing
+ IsRegularRing.globalDimension_eq_ringKrullDim
+ IsRegularRing.of_isDedekindDomain
+ IsRegularRing.of_isField
+ LinearMapOfSemiLinearMapAlgebraMap
+ Module.finrank_eq_spanFinrank_of_free
+ ModuleCat.IsCohenMacaulay
+ ModuleCat.IsCohenMacaulay_of_iso
+ ModuleCat.IsMaximalCohenMacaulay
+ ModuleCat.depth_eq_supportDim_of_cohenMacaulay
+ ModuleCat.depth_eq_supportDim_unbot_of_cohenMacaulay
+ ModuleCat.exists_isRegular_of_exists_subsingleton_ext
+ ModuleCat.exists_isRegular_tfae
+ ModuleCat.free_of_projective_of_isLocalRing
+ ModuleCat.isCohenMacaulay_iff
+ ModuleCat.subsingleton_ext_of_exists_isRegular
+ MvPolynomial.isRegularRing_of_isRegularRing
+ Polynomial.isRegularRing_of_isRegularRing
+ Polynomial.localization_at_comap_maximal_isRegularRing_isRegularRing
+ SemiLinearMapAlgebraMapOfLinearMap
+ Submodule.comap_lt_top_of_lt_range
+ Submodule.span_val_image_eq_iff
+ 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.natCast_add_cancel
+ WithBot.one_add_cancel
+ _root_.AddLECancellable.withBot
+ _root_.AddLECancellable.withTop
+ _root_.IsAddLeftRegular.withBot
+ _root_.IsAddLeftRegular.withTop
+ _root_.IsAddRightRegular.withBot
+ _root_.IsAddRightRegular.withTop
+ associatedPrimes_self_eq_minimalPrimes
+ associated_prime_eq_minimalPrimes_isCohenMacaulay
+ associated_prime_minimal_of_isCohenMacaulay
+ basis_lift
+ basis_lift_ker_le
+ depth_eq_dim_quotient_associated_prime_of_isCohenMacaulay
+ depth_le_ringKrullDim
+ depth_le_ringKrullDim_associatedPrime
+ depth_le_supportDim
+ depth_ne_top
+ depth_quotient_regular_sequence_add_length_eq_depth
+ exist_nat_eq
+ ext_hom_zero_of_mem_ideal_smul
+ ext_quotient_one_subsingleton_iff
+ ext_subsingleton_of_lt_moduleDepth
+ ext_subsingleton_of_quotients
+ ext_subsingleton_of_quotients'
+ finite_projectiveDimension_of_isRegularLocalRing_aux
+ finte_free_ext_vanish_iff
+ free_depth_eq_ring_depth
+ free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ free_of_quotSMulTop_free
+ globalDimension
+ globalDimension_eq_bot_iff
+ globalDimension_eq_iSup_loclization_maximal
+ globalDimension_eq_iSup_loclization_prime
+ globalDimension_eq_sup_injectiveDimension
+ globalDimension_eq_sup_projectiveDimension_finite
+ globalDimension_le_iff
+ globalDimension_le_tfae
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ iff_finrank_cotangentSpace
+ injective_of_subsingleton_ext_quotient_one
+ instance (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
+ instance (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) :
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ instance [IsNoetherianRing R] [IsLocalRing R] [Small.{v} R]
+ instance [IsRegularLocalRing R] : IsDomain R := isDomain_of_isRegularLocalRing R
+ instance [Small.{v} R] (S : Submonoid R) :
+ isCohenMacaulayLocalRing_def
+ isCohenMacaulayLocalRing_iff
+ isCohenMacaulayLocalRing_localization_atPrime
+ isCohenMacaulayLocalRing_of_isRegularLocalRing
+ isCohenMacaulayLocalRing_of_ringEquiv
+ isCohenMacaulayLocalRing_of_ringKrullDim_le_depth
+ isCohenMacaulayRing_def
+ isCohenMacaulayRing_def'
+ isCohenMacaulayRing_iff
+ isCohenMacaulayRing_of_ringEquiv
+ isCohenMacaulay_of_isMaximalCohenMacaulay
+ isDomain_of_isRegularLocalRing
+ isField_of_isRegularLocalRing_of_dimension_zero
+ isLocalization_at_prime_prime_depth_le_depth
+ isLocalize_at_prime_depth_eq_of_isCohenMacaulay
+ isLocalize_at_prime_dim_eq_prime_depth_of_isCohenMacaulay
+ isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ isLocalizedModule_quotSMulTop_isLocalizedModule_map
+ isMaximalCohenMacaulay_def
+ isRegularLocalRing_def
+ isRegularRing_iff
+ isRegularRing_of_ringEquiv
+ isRegular_of_span_eq_maximalIdeal
+ localize_at_prime_depth_eq_of_isCohenMacaulay
+ localize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ mem_smul_top_of_range_le_smul_top
+ moduleDepth
+ moduleDepth_eq_depth_of_supp_eq
+ moduleDepth_eq_find
+ moduleDepth_eq_iff
+ moduleDepth_eq_moduleDepth_shrink
+ moduleDepth_eq_of_iso_fst
+ moduleDepth_eq_of_iso_snd
+ moduleDepth_eq_sSup_length_regular
+ moduleDepth_eq_sup_nat
+ moduleDepth_eq_top_iff
+ moduleDepth_eq_zero_of_hom_nontrivial
+ moduleDepth_ge_depth_sub_dim
+ moduleDepth_ge_min_of_shortExact_fst_fst
+ moduleDepth_ge_min_of_shortExact_fst_snd
+ moduleDepth_ge_min_of_shortExact_snd_fst
+ moduleDepth_ge_min_of_shortExact_snd_snd
+ moduleDepth_ge_min_of_shortExact_trd_fst
+ moduleDepth_ge_min_of_shortExact_trd_snd
+ moduleDepth_lt_top_iff
+ moduleDepth_quotSMulTop_succ_eq_moduleDepth
+ moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth
+ nontrivial_ring_of_nontrivial_module
+ of_ringEquiv
+ of_spanFinrank_maximalIdeal_le
+ projectiveDimension_eq_iSup_localizedModule_maximal
+ projectiveDimension_eq_iSup_localizedModule_prime
+ projectiveDimension_le_projectiveDimension_of_isLocalizedModule
+ projectiveDimension_ne_top_of_isRegularLocalRing
+ quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay
+ quotSMulTop_isLocalizedModule_map
+ quotSMulTop_nontrivial
+ quotient_isRegularLocalRing_tfae
+ quotient_prime_ringKrullDim_ne_bot
+ quotient_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_sequence_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_smul_top_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_smul_top_lt_of_le_smul_top
+ quotient_span_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_span_singleton
+ ringKrullDim_le_spanFinrank_maximalIdeal
+ ring_depth_invariant
+ ring_depth_uLift
+ smul_prod_of_smul
+ smul_top_eq_comap_smul_top_of_surjective
+ spanFinrank_eq_finrank_quotient
+ spanFinrank_eq_of_ringEquiv
+ spanFinrank_le_of_surjective
+ spanFinrank_maximalIdeal_eq_finrank_cotangentSpace
+ spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg
+ subsingleton_of_pi
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.
Increase in tech debt: (relative, absolute) = (25.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 13104 | 25 | backward.isDefEq |
Current commit c0d6e13485
Reference commit 52b9aaf523
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
This pull request has conflicts, please merge |
mathlib4-merge-conflict-bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib4-merge-conflict-bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
merge-conflict
github-actions
bot
added
the
large-import
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
…dimension-eq-sup-localization
…ension-of-Regular-Local-Ring
…ension-of-Regular-Ring
…sion-of-Regular-Ring
…-Theorem-(Projective)
…orem-(Projective)
4 participants
In this PR, we proved for field
k,MvPolynomial (Fin n) khas global dimensionn.