Commit 2025-04-03 10:34 3b028927

View on Github →

refactor(RingTheory/Smooth): remove universe parameters for generators and relations in Algebra.IsStandardSmooth (#23553) We ask for the existence of a presentation with generators and relations in Type and provide a constructor taking a presentation with arbitrary universe levels.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

Modified Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Presentation.dimension_reindex

Modified Mathlib/RingTheory/RingHom/StandardSmooth.lean

modified theorem RingHom.IsStandardSmooth.toAlgebra

modified theorem RingHom.isStandardSmooth_localizationPreserves

modified theorem RingHom.isStandardSmooth_respectsIso

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

modified theorem Algebra.IsStandardSmooth.trans

modified theorem Algebra.IsStandardSmoothOfRelativeDimension.trans

added theorem Algebra.SubmersivePresentation.isStandardSmooth

added theorem Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension