mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

fg graded ring

Open jjaassoonn opened this issue 2 years ago • 1 comments

  1. if $A$ is a noetherian graded ring, then $A_0$ is a noetherian subring of $A$ and $A$ is a finitely generated algebra over $A_0$, if $M$ is a finitely generated graded module over $A$, then each $M_n$ is a finitely generated module over $A_0$.

  2. Definition of additive functions over any abelian category: if $C$ is an abelian category, a function $f : C \to \mathbb Z$ is said to be additive, if $f(y) = f(x) + f(z)$ whenever $0\to x \to y \to z \to 0$ is exact. proved some basic properties such as $f(0) = 0$ and $f(x) = f(y)$ whenever $x \cong y$ and interaction of $f$ with longer exact sequences

  3. The category of finitely generated module over noetherian ring is abelian

  4. A proof of Hilbert-Serre theorem: the Poincare series is actually of the form $\frac{p}{\prod(1- X^i)}$ where $p$ is polynomial

The code works, but poorly written.

Open in Gitpod

jjaassoonn avatar Jan 17 '24 19:01 jjaassoonn

I have added a file HilbertPolynomial.lean to the folder Mathlib/Algebra/HilbertSerre. In the file, the main things I have done are:

  1. formalising the Hilbert polynomial (HilbertSerre.hilbertPolynomial), which is a one-variable polynomial with coefficients in ℚ;
  2. proving that for any large enough n : ℕ, the value of the additive function μ at ℳ n is equal to the value of the Hilbert polynomial at n;
  3. showing that the polynomial h satisfying the above property (i.e. for any large enough n : ℕ, the value of μ at ℳ n equals the value of h at n) is unique;
  4. proving a theorem HilbertSerre.natDegree_hilbertPolynomial, which tells us the specific degree of any non-zero Hilbert polynomial.

The codes have been edited to be much neater and conciser than the original draft, but may still need further improvements.

FMLJohn avatar Mar 19 '24 12:03 FMLJohn

PR summary 413e5b872a

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.GradedAlgebra.Noetherian 976 1070 +94 (+9.63%)
Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal 926 956 +30 (+3.24%)
Mathlib.RingTheory.GradedAlgebra.Radical 927 957 +30 (+3.24%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology 1029 1059 +30 (+2.92%)

Declarations diff

+ A'ZeroToAZero + A'ZeroToAZero_comp_AZeroToA'Zero + AZeroEquivA'Zero + AZeroToA'Zero + AZeroToA'Zero_comp_A'ZeroToAZero + AdditiveFunction + AdditiveFunction_eq_hilbertPolynomial_eval + Algebra.adjoin_isNoetherian + Algebra.adjoin_module_finite_of_annihilating + Algebra.adjoin_smul_def + C + COKER.descComponent + COKER.descComponent_surjective + Finset.single_le_sum' + GradeZero.distribMulAction_at_i + GradeZero.module_at_i + GradeZero.mulAction_at_i + GradeZero.smul_at_i + GradeZero.subring_isNoetherianRing_of_isNoetherianRing + GradedRing.exists_of_mem_homogeneousComponents + GradedRing.homogeneousComponents + GradedRing.homogeneousComponents_def + GradedRing.mem_homogeneousComponents_iff + GradedRing.mem_homogeneousComponents_of_ne_zero_and_exists + GradedRing.mem_homogeneousSubmonoid_of_mem_homogeneousComponents + GradedRing.ne_zero_of_mem_homogeneousComponents + HomogeneousSubmodule + HomogeneousSubmodule.ext + HomogeneousSubmodule.homogeneousHull_toSubmodule_eq_self + HomogeneousSubmodule.isHomogeneous + HomogeneousSubmodule.mem_iff + HomogeneousSubmodule.setLike + HomogeneousSubmodule.toSubmodule_homogeneousCore_eq_self + HomogeneousSubmodule.toSubmodule_injective + HomogeneousSubring + HomogeneousSubring.ext + HomogeneousSubring.isHomogeneous + HomogeneousSubring.mem_iff + HomogeneousSubring.setLike + HomogeneousSubring.toSubring_injective + Ideal.fg_iff_homogeneously_fg + Ideal.homogeneousCore'_eq_sSup + Ideal.homogeneousHull + Ideal.homogeneously_FG + Ideal.le_toSubmodule_homogeneousHull + Irrelevant + KER + KER.componentEmb + KER.componentEmb_injective + MvPowerSeries + Submodule.IsHomogeneous + Submodule.IsHomogeneous.iff_eq + Submodule.IsHomogeneous.iff_exists + Submodule.IsHomogeneous.toSubmodule_homogeneousCore_eq_self + Submodule.IsHomogeneous.toSubmodule_homogeneousHull_eq_self + Submodule.fg_iff_homogeneously_fg + Submodule.homogeneousCore + Submodule.homogeneousCore' + Submodule.homogeneousCore'_eq_sSup + Submodule.homogeneousCore'_le + Submodule.homogeneousCore'_mono + Submodule.homogeneousCore.gc + Submodule.homogeneousCore.gi + Submodule.homogeneousCore_eq_sSup + Submodule.homogeneousCore_mono + Submodule.homogeneousHull + Submodule.homogeneousHull.gc + Submodule.homogeneousHull.gi + Submodule.homogeneousHull_eq_iSup + Submodule.homogeneousHull_eq_sInf + Submodule.homogeneousHull_mono + Submodule.homogeneous_span + Submodule.homogeneously_FG + Submodule.isHomogeneous_iff_forall_subset + Submodule.isHomogeneous_iff_subset_iInter + Submodule.le_toSubmodule_homogeneousHull + Submodule.mem_homogeneousCore_of_homogeneous_of_mem + Submodule.smul_homogeneous_element_mem_of_mem + Submodule.toSubmodule_homogeneousCore_le + Submodule.toSubmodule_homogeneousHull_eq_iSup + Subring.IsHomogeneous + Subring.homogeneousCore' + Subring.homogeneousCore'_le + Subring.homogeneousCore'_mono + Subring.homogeneous_closure + Subring.isHomogeneous_iff_forall_subset + Subring.isHomogeneous_iff_subset_iInter + Top + X + X_def + X_dvd_iff + X_inj + X_pow_dvd_iff + X_pow_eq + X_pow_order_dvd + _root_.RingEquiv.toFGModuleCatEquivalence + _root_.RingEquiv.toFGModuleCatEquivalenceFunctor + _root_.RingEquiv.toFGModuleCatEquivalenceInverse + _root_.hilbert_serre + abelian_A'_zero + abelian_of_noetherian + add + addCommMonoid + addMonoid + addSemigroup + addZeroClass + add_apply + add_mul + adjoinHomogeneous + algebraMap_apply + algebraMap_apply' + algebraMap_apply'' + algebraMvPolynomial + algebraMvPowerSeries + alternating_apply_aux_of_length6 + alternating_sum_apply_eq_zero_of_zero_zero_of_length6 + alternating_sum_apply_eq_zero_of_zero_zero_of_length6' + alternating_sum_apply_eq_zero_of_zero_zero_of_length6_aux + alternating_sum_apply_of_length6 + anExactSeq + anExactSeq_complex + anExactSeq_exact + apply_eq_apply_image_add_apply_image + apply_eq_apply_kernel_add_apply_kernel + apply_image_eq_apply_ker_succ + apply_kernel_sub_apply_cokernel_eq_apply_src_sub_apply_tgt + apply_shortComplex_of_exact + apply_shortComplex_of_exact' + apply_sub_apply_succ + asHom + c_eq_algebraMap + coeToMvPowerSeries + coeToMvPowerSeries.algHom + coeToMvPowerSeries.algHom_apply + coeToMvPowerSeries.ringHom + coeToMvPowerSeries.ringHom_apply + coe_C + coe_X + coe_add + coe_bit0 + coe_bit1 + coe_def + coe_eq_one_iff + coe_eq_zero_iff + coe_inf + coe_inj + coe_injective + coe_monomial + coe_mul + coe_one + coe_pow + coe_sup + coe_zero + coeff + coeff_C + coeff_C_mul + coeff_X + coeff_X_pow + coeff_add_monomial_mul + coeff_add_mul_monomial + coeff_coe + coeff_comp_monomial + coeff_index_single_X + coeff_index_single_self_X + coeff_invOfUnit + coeff_inv_aux + coeff_map + coeff_monomial + coeff_monomial_mul + coeff_monomial_ne + coeff_monomial_same + coeff_mul + coeff_mul_C + coeff_mul_invOneSubPow_eq_hilbert_eval + coeff_mul_monomial + coeff_mul_of_lt_order + coeff_mul_one_sub_of_lt_order + coeff_mul_prod_one_sub_of_lt_order + coeff_of_lt_order + coeff_one + coeff_order + coeff_poincareSeries + coeff_prod + coeff_smul + coeff_trunc + coeff_truncFun + coeff_zero + coeff_zero_C + coeff_zero_X + coeff_zero_X_mul + coeff_zero_eq_constantCoeff + coeff_zero_eq_constantCoeff_apply + coeff_zero_mul_X + coeff_zero_one + cokernelCocone + cokernelIsColimit + cokernelIsoRangeQuotient + cokernel_π_cokernelIsoRangeQuotient_hom + cokernel_π_ext + commute_X + commute_monomial + completeLattice + constantCoeff + constantCoeff_C + constantCoeff_X + constantCoeff_comp_C + constantCoeff_invOfUnit + constantCoeff_map + constantCoeff_one + constantCoeff_zero + decomposition + degreeMonomial + degreeMonomial_zero + epi_iff_range_eq_top + epi_iff_surjective + eqCOKER + eqKER + eq_apply_image_add_apply_cokernel + eq_apply_kernel_add_apply_image + eq_bot_iff + eq_of_coeff_monomial_ne_zero + eq_of_iso + eq_top_iff + evalMonomial_homogeneous + evalMonomial_mem + evalMonomial_mem_aux + eventually_eq_zero_of_empty_generatorSet + eventually_subsingleton_of_empty_generatorSet + exact_KERComponentEmb_smulBy + exact_iff + exact_smulBy_COKERDescComponent + exact_smulBy_COKERDescComponent' + exists_coeff_ne_zero_iff_ne_zero + exists_unique_hilbert + exists_unique_hilbertPolynomial + ext_iff + finite_COKER + finite_KER + finite_adjoin_module_of_finite_module + finite_algebra_over_degree_zero_subring + finite_module_over_degree_zero_subring + forget_preservesEpimorphisms + forget_preservesMonomorphisms + forget₂CreatesLimitOfNoetherian + fromHomogeneousGeneratingSetOfIrrelevant + generatingSet' + generatingSetOverBaseRing + generatingSet_is_finite + gradedModule_COKER + gradedModule_KER + gradedRing + gradedRing_A' + gradedSMul + grading.decompose_def + greatestFactorOneSubNotDvd + greatestFactorOneSubNotDvd_ne_zero + hasCokernels_fgModuleCat + hasKernels_fgModuleCat + hilbert + hilbertPolynomial + homogeneousComponents + homogeneous_of_mem_homogeneousComponents + iInf + iInf₂ + iSup + iSup₂ + iff_quotient_mvPolynomial''' + induction + inf + instance (F : J ⥤ FGModuleCat R) : + instance (I : Ideal A) : Membership A (HomogeneousGeneratingSetOf 𝒜 I) + instance (J : Type) [Category J] [FinCategory J] : + instance (n : ℕ) : Module (𝒜 0) ((COKER.den ℳ x deg_x).quotientGrading n) + instance (p : Submodule A M) : Membership M (HomogeneousGeneratingSetOf ℳ p) + instance : Add (HomogeneousIdeal 𝒜) := inferInstanceAs <| Add <| HomogeneousSubmodule A 𝒜 + instance : Add (HomogeneousSubmodule A ℳ) + instance : AddCommGroup (𝒞 ⟹+ T) + instance : AddMonoidWithOne (MvPowerSeries σ R) + instance : AddSubgroupClass (HomogeneousSubmodule A ℳ) M + instance : Algebra (𝒜 0) A := Algebra.ofSubring (SetLike.GradeZero.subring 𝒜) + instance : Algebra R (MvPowerSeries σ A) + instance : Bot (HomogeneousIdeal 𝒜) := inferInstanceAs <| Bot <| HomogeneousSubmodule A 𝒜 + instance : Bot (HomogeneousSubmodule A ℳ) + instance : CreatesLimitsOfShape J (forget₂ (FGModuleCat R) (ModuleCat.{v} R)) + instance : DFunLike (AdditiveFunction 𝒞 T) 𝒞 (fun _ ↦ T) + instance : Decomposition A'.grading + instance : DirectSum.Decomposition (COKER.den ℳ x deg_x).quotientGrading + instance : HasFiniteLimits (FGModuleCat R) + instance : Inf (HomogeneousIdeal 𝒜) := inferInstanceAs <| Inf <| HomogeneousSubmodule A 𝒜 + instance : Inf (HomogeneousSubmodule A ℳ) + instance : InfSet (HomogeneousIdeal 𝒜) := inferInstanceAs <| InfSet <| HomogeneousSubmodule A 𝒜 + instance : InfSet (HomogeneousSubmodule A ℳ) + instance : Inv (MvPowerSeries σ k) + instance : Inv (PowerSeries k) + instance : InvOneClass (MvPowerSeries σ k) + instance : InvOneClass (PowerSeries k) + instance : IsNoetherianRing R[S] + instance : Module R[S] M + instance : Mul (MvPowerSeries σ R) + instance : One (MvPowerSeries σ R) + instance : PreservesFiniteLimits (forget₂ (FGModuleCat R) (ModuleCat.{v} R)) + instance : Semiring (MvPowerSeries σ R) + instance : SetLike.GradedMonoid A'.grading + instance : SetLike.GradedSMul 𝒜 (COKER.den ℳ x deg_x).quotientGrading + instance : SubringClass (HomogeneousSubring 𝒜𝒜) AA + instance : Sup (HomogeneousIdeal 𝒜) := inferInstanceAs <| Sup <| HomogeneousSubmodule A 𝒜 + instance : SupSet (HomogeneousIdeal 𝒜) := inferInstanceAs <| SupSet <| HomogeneousSubmodule A 𝒜 + instance : Top (HomogeneousIdeal 𝒜) := inferInstanceAs <| Top <| HomogeneousSubmodule A 𝒜 + instance : Top (HomogeneousSubmodule A ℳ) + instance [AddCommGroup R] : AddCommGroup (MvPowerSeries σ R) + instance [AddCommMonoid R] : AddCommMonoid (MvPowerSeries σ R) + instance [AddGroup R] : AddGroup (MvPowerSeries σ R) + instance [AddMonoid R] : AddMonoid (MvPowerSeries σ R) + instance [CommRing R] : CommRing (MvPowerSeries σ R) + instance [CommSemiring R] : CommSemiring (MvPowerSeries σ R) + instance [Inhabited R] : Inhabited (MvPowerSeries σ R) + instance [LocalRing R] : LocalRing (MvPowerSeries σ R) + instance [Nonempty σ] [Nontrivial R] : Nontrivial (Subalgebra R (MvPowerSeries σ R)) + instance [Nontrivial R] : Nontrivial (MvPowerSeries σ R) + instance [Ring R] : Ring (MvPowerSeries σ R) + instance [Zero R] : Zero (MvPowerSeries σ R) + instance {A S} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S] + instance {A} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (MvPowerSeries σ A) + instance {J : Type} [Finite J] (Z : J → ModuleCat R) [∀ j, Module.Finite R (Z j)] : + inv.aux + invOfUnit + invOneSubPow + invOneSubPow_eq_inv_one_sub_pow + invOneSubPow_inv_eq_one_sub_pow + invOneSubPow_val_eq_mk_choose_add + invOneSubPow_val_mul_one_sub_pow_eq_one + invOneSubPow_val_zero_eq_invUnitSub_one + inv_eq_inv_aux + irrelevant.adjoin_eq_top + irrelevant.deg_pos + irrelevant_eq + isUnit_constantCoeff + ker_eq_bot_of_mono + kernelCone + kernelIsLimit + kernelIsoKer + kernelIsoKer_hom_ker_subtype + kernelIsoKer_inv_kernel_ι + key_lemma + kth_degree_eq_span + le_order + le_order_add + map + map.isLocalRingHom + map_C + map_X + map_comp + map_id + map_monomial + map_subsingleton + map_zero + mem_A' + mem_KER_iff + mk_apply + mk_choose_add_mul_one_sub_pow_eq_one + mk_empty + mk_eq_sum_of + mk_one_pow_eq_mk_choose_add + mono_iff_injective + mono_iff_ker_eq_bot + monomial + monomial_def + monomial_finite_of_bounded_degree + monomial_mul_monomial + monomial_zero_eq_C + monomial_zero_eq_C_apply + monomial_zero_one + mul_add + mul_assoc + mul_invOfUnit + mul_one + mul_zero + natDegree_greatestFactorOneSubNotDvd_le + natDegree_hilbert + natDegree_hilbertPolynomial + natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le + nat_le_order + neg + neg_apply + noetherian_A' + noetherian_A'_zero + normalEpi + normalMono + numeratorPolynomial + numeratorPolynomial_mul_inv_poles_eq_poincareSeries + one_mul + one_sub_pow_mul_invOneSubPow_val_eq_one + one_sub_pow_mul_mk_choose_add_eq_one + order + order_X + order_X_pow + order_add_of_order_eq + order_eq + order_eq_multiplicity_X + order_eq_nat + order_eq_top + order_finite_iff_ne_zero + order_le + order_monomial + order_monomial_of_ne_zero + order_mul + order_mul_ge + order_one + order_zero + poincareSeries + poles + poles_eq_one_sub_pow_of_deg_eq_one + poles_inv_eq' + poles_val + pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq + preHilbert + preHilbert_eq_choose_sub_add + prod_sub_rootMultiplicity_coeff_eq_one + proj + proj_smul_mem_left + proj_smul_mem_right + proof' + proof.base_case + pushforward + quotientDecomposition + quotientGradedSMul + quotientGrading + quotientGrading.decompose + quotientGrading.decomposeAux + quotientGrading.decompose_apply_mkQ_of_mem + quotientGrading.decompose_apply_mkQ_of_ne + quotientGrading.decompose_leftInverse + quotientGrading.decompose_rightInverse + quotientGrading.le_decomposeAux_ker + quotientGradingEmb + range_eq_top_of_epi + range_mkQ_cokernelIsoRangeQuotient_inv + reindex + smulBy + smul_eq_C_mul + statement'_imp_statement + supSet + support_mk + toMvPowerSeries + toSubmodule_add + toSubmodule_bot + toSubmodule_iInf + toSubmodule_iInf₂ + toSubmodule_iSup + toSubmodule_iSup₂ + toSubmodule_inf + toSubmodule_sInf + toSubmodule_sSup + toSubmodule_sup + toSubmodule_top + trunc + truncFun + trunc_c + trunc_one + uniqueOfEpiZero + zero + zero_apply + zero_mul + μ' ++ C_inv ++ FG.spanningSet ++ FG.spanningSet_span_eq ++ HomogeneousGeneratingSetOf ++ X_inv ++ coeff_inv ++ constantCoeff_inv ++ deg ++ eq_inv_iff_mul_eq_one ++ eq_mul_inv_iff_mul_eq ++ evalMonomial ++ evalMonomial_zero ++ ext ++ grading ++ grading.decompose ++ grading.decompose_add ++ grading.decompose_apply ++ grading.decompose_leftInverse ++ grading.decompose_rightInverse ++ grading.decompose_zero ++ homogeneous ++ instance : Inhabited (HomogeneousSubmodule A ℳ) where default := ⊥ ++ instance : PartialOrder (HomogeneousSubmodule A ℳ) ++ inv ++ invOfUnit_eq ++ invOfUnit_eq' ++ inv_eq_iff_mul_eq_one ++ inv_eq_zero ++ inv_mul_cancel ++ mem_deg ++ mul_inv_cancel ++ mul_inv_rev ++ ne_zero ++ pow_inv_eq_inv_pow ++ smul_inv ++ sup ++ top_eq_span_monomial ++ zero_inv +-+ bot +-+ coe_bot +-+ coe_top +-+ sInf +-+ sSup +-+ top - GradeZero.isNoetherianRing - Ideal.le_toIdeal_homogeneousHull - instance : Add (HomogeneousIdeal 𝒜) - instance : Bot (HomogeneousIdeal 𝒜) - instance : Inf (HomogeneousIdeal 𝒜) - instance : InfSet (HomogeneousIdeal 𝒜) - instance : Inhabited (HomogeneousIdeal 𝒜) where default := ⊥ - instance : PartialOrder (HomogeneousIdeal 𝒜) - instance : Sup (HomogeneousIdeal 𝒜) - instance : SupSet (HomogeneousIdeal 𝒜) - instance : Top (HomogeneousIdeal 𝒜)

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

github-actions[bot] avatar Jun 28 '24 20:06 github-actions[bot]