Commit 2025-12-09 15:53 d8cc48cc

View on Github →

feat(RingTheory): smooth algebras have smooth Noetherian models (#25143) Co-authored by: Judith Ludwig ludwig@mathi.uni-heidelberg.de

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

added theorem MvPolynomial.eval₂_map_comp_C

added theorem MvPolynomial.map_eval

Modified Mathlib/Data/Finsupp/Weight.lean

added theorem Finsupp.range_single_one

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem AlgHom.kerSquareLift_mk

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem Ideal.mem_span_iff_exists_isHomogeneous

added theorem Ideal.mem_span_pow_iff_exists_isHomogeneous

added theorem Ideal.span_eq_map_homogeneousSubmodule

added theorem Ideal.span_pow_eq_map_homogeneousSubmodule

added theorem MvPolynomial.IsHomogeneous.of_map

added theorem MvPolynomial.homogeneousSubmodule_one_eq_span_X

added theorem MvPolynomial.homogeneousSubmodule_one_pow

added theorem MvPolynomial.homogeneousSubmodule_zero

added theorem MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

added theorem MvPolynomial.IsWeightedHomogeneous.C_mul

added theorem MvPolynomial.IsWeightedHomogeneous.induction_on

Created Mathlib/RingTheory/Smooth/NoetherianDescent.lean

added theorem Algebra.Smooth.DescentAux.coeffs_h_subset

added theorem Algebra.Smooth.DescentAux.coeffs_p_subset

added theorem Algebra.Smooth.DescentAux.coeffs_q_subset

added theorem Algebra.Smooth.DescentAux.exists_kerSquareLift_comp_eq_id

added def Algebra.Smooth.DescentAux.subalgebra

added structure Algebra.Smooth.DescentAux