Commit 2025-01-30 13:06 6f5142e8

feat(RingTheory/StandardSmooth): naive cotangent complex of a submersive presentation (#19748) We show that H¹(L_{S/R}) is trivial if S is R-standard smooth and that Ω[S⁄R] is free of rank n if S is R-standard smooth of relative dimension n. In particular this shows that standard smooth implies smooth and that standard smooth of relative dimension zero implies smooth and unramified.