3 papers
math.AC2026
Formalization in Lean of faithfully flat descent of projectivity
Liran Shaul
We formalize in Lean the following foundational result in commutative algebra: Let be a faithfully flat map of (not necessarily noetherian) commutative rings, and let …
math.AC2025
Openness with respect to levels in triangulated categories
Souvik Dey, Jian Liu, Liran Shaul
Given a compactly generated triangulated category equipped with an action of a graded-commutative Noetherian ring , generalizing results of Letz, we prove a genera…
math.AC2024
Finitistic dimensions over commutative DG-rings
Isaac Bird, Liran Shaul, Prashanth Sridhar +1
In this paper we study the finitistic dimensions of commutative noetherian non-positive DG-rings with finite amplitude. We prove that any DG-module of finite flat dimension ove…