Commit 2024-07-24 16:47 465e6f3d

View on Github →

feat(RingTheory.MvPolynomial.WeightedHomogeneous): add graded algebra structure (#14225) Given a weight w : σ → M, where M is an additive and commutative monoid, we endow the ring of multivariate polynomials MvPolynomial σ R with the structure of a graded algebra

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

added theorem DirectSum.coeAddMonoidHom_eq_dfinsupp_sum

added theorem DirectSum.finite_support

added theorem DirectSum.mk_apply_of_mem

added theorem DirectSum.mk_apply_of_not_mem

added theorem DirectSum.support_subset

Modified Mathlib/Algebra/DirectSum/Decomposition.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.coeLinearMap_eq_dfinsupp_sum

Modified Mathlib/Algebra/Lie/DirectSum.lean

Modified Mathlib/Data/Finsupp/Weight.lean

modified theorem Finsupp.degree_eq_weight_one

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.HomogeneousSubmodule.gradedMonoid

added theorem MvPolynomial.decomposition.decompose'_apply

added theorem MvPolynomial.decomposition.decompose'_eq

deleted theorem MvPolynomial.homogeneousComponent_homogeneous_polynomial

added theorem MvPolynomial.homogeneousComponent_mem

added theorem MvPolynomial.homogeneousComponent_of_mem

added theorem MvPolynomial.totalDegree_eq_zero_iff

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

added theorem MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum

added theorem MvPolynomial.DirectSum.coeLinearMap_eq_dfinsupp_sum

added theorem MvPolynomial.DirectSum.coeLinearMap_eq_finsum

added theorem MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid

added def MvPolynomial.decompose'

added theorem MvPolynomial.decompose'_apply

added theorem MvPolynomial.weightedDecomposition.decompose'_apply

added theorem MvPolynomial.weightedDecomposition.decompose'_eq

added def MvPolynomial.weightedDecomposition

added def MvPolynomial.weightedGradedAlgebra

added theorem MvPolynomial.weightedHomogeneousComponent_directSum

added theorem MvPolynomial.weightedHomogeneousComponent_eq_zero_of_not_mem

added theorem MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne

added theorem MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_same

added theorem MvPolynomial.weightedHomogeneousComponent_of_mem

deleted theorem MvPolynomial.weightedHomogeneousComponent_weighted_homogeneous_polynomial