Algebraický seminář
Liran Shaul (MFF UK): Formalization in Lean of faithfully flat descent of projectivity
Abstract: Let R \to S be a faithfully flat map of (not necessarily noetherian) commutative rings, and let P be an arbitrary R-module. Then P is projective over R if and only if S\otimes_R P is projective over S. In this talk we discuss the history and importance of this result, and how we recently formalized it, using Lean.
March 23 - Marc Stephan (MPI-CBG and TU Dresden): Regular sequences and level inequalities
The Algebra Seminar was founded by Vladimir Korinek in the early 1950's and continued by Karel Drbohlav until 1981. The seminar resumed its activities in 1990 under the guidance of Jaroslav Jezek and Tomas Kepka. Since 1994, the seminar is headed by Jan Trlifaj.
Presently, the seminar is supported by GACR. It serves primarily as a platform for presentation of recent research of the visitors to the Department of Algebra as well as members of the Department and their students.
