Commit 2024-10-01 17:04 c9ef6fe0

View on Github →

feat(RingTheory/StandardSmooth): composition and localization (#16827) Constructs submersive presentations for composition and localization away from one element. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.aeval_sum_elim

added theorem MvPolynomial.comp_aeval_apply

Modified Mathlib/Algebra/MvPolynomial/PDeriv.lean

added theorem MvPolynomial.aeval_sum_elim_pderiv_inl

added theorem MvPolynomial.pderiv_rename

Modified Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Presentation.comp_aeval_relation_inl

added theorem Algebra.Presentation.comp_relation_inr

deleted theorem Algebra.Presentation.comp_relation_map

modified theorem Algebra.Presentation.localizationAway_dimension_zero

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.IsStandardSmooth.localization_away

added theorem Algebra.IsStandardSmooth.trans

added theorem Algebra.IsStandardSmoothOfRelativeDimension.localization_away

added theorem Algebra.IsStandardSmoothOfRelativeDimension.trans

added theorem Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian

added theorem Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

added theorem Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix

added theorem Algebra.PreSubmersivePresentation.localizationAway_jacobian