Commit 2026-02-10 11:38 c172dd7b
View on Github →refactor(AlgebraicGeometry/Smooth): replace Locally IsStandardSmooth by Smooth (#35034)
This finally completes the journey of a reasonable definition of smooth morphisms. For historical context: The old definition was put in place around the AIM workshop on algebraic geometry in summer 2024 with the plan to eventually replace it by this definition when all the commutative algebra pre-requisites are completed. This is now the case, with the last piece being the equivalence of smooth with locally standard smooth.