Monogenic Extensions of Regular Local Rings

Stream: new members

[George Peykanu]

Hello everyone! My name is George Peykanu, and I am an undergraduate researcher at the University of Washington's Math AI Lab, headed by Professor Jarod Alper, working on one of several formalization projects hosted here at the UW. Our group has formalized several results in Ring Theory and Commutative Algebra, and are seeking to soon make a Mathlib PR! One such result is that if a finite extension (R --> S) between two regular local rings, R, S, is etale, then it is monogenic (that is, a single element of the larger ring, S, can be adjoined to R to extend R to the whole of S). Another is a soon-forthcoming formalization of a generalization of this theorem: that if there is a height-one prime ideal, q, such that the extension (R-->S), filtered through the quotient R/(q \cap R) --> S is etale, then the extension from R --> S is monogenic. Along the way, we have generated several useful lemmas, which we are also interested in pushing to Mathlib! Our work closely follows the recent work of our team lead: Professor Bianca Viray, and her recently-published work which can be found at : https://arxiv.org/pdf/2503.07846.