Commit 2025-12-05 16:31 3bd1307a
View on Github →feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation (#31034)
Let S be a finitely presented R-algebra and suppose P : R[X] → S generates S with
kernel I. In this PR we show that if I/I² is free, there exists an R-presentation P' of S
extending P with kernel I', such that I'/I'² is free on the images of the relations of P'.
From Pi1.