Commit 2024-10-17 09:39 d8ceed52

feat(AlgebraicGeometry): smooth morphisms of schemes (#14161) We say a morphism of schemes is smooth (of relative dimension n) if for every point of the source there exist affine open neighborhoods of the point and its image such that the induced ring map is standard smooth (of relative dimension n). These notions are local on the source and the target and satisfy the standard stability properties. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.