Commit 2024-07-15 20:56 72f3c598

View on Github →

feat(RingTheory/Smooth): define standard smooth algebras (#14325) We define the notion of a submersive presentation and predicates when such a presentation is standard smooth. An algebra is called standard smooth if it admits a standard smooth presentation. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth

added theorem Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_apply

added theorem Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det

added structure Algebra.PreSubmersivePresentation

added structure Algebra.SubmersivePresentation

added def RingHom.IsStandardSmooth

added theorem RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth

added def RingHom.IsStandardSmoothOfRelativeDimension