Commit 2025-11-06 18:48 4b805205

chore(RingTheory): redefine FormallySmooth in terms of Ω[S⁄R] and H¹(L_{S/R}) (#30876) Previously FormallySmooth was defined in terms of an infinitesimal lifting criterion, which involved quantifying over all algebras in an universe. We also showed that this is equivalent to Ω[S⁄R] being projective and H¹(L_{S/R}) = 0. We change the definition to switch to the latter so that we do not need to quantify over types. As a plus we can generalize the universes of FormallySmooth and by extension Smooth, Etale etc.