Abstract
Harder-Narasimhan filtration is a classical construction in the study of vector bundles on a regular projective curve. Curiously, it has analogues in various domains of mathematics. In this talk, I will explain a joint work with Marion Jeannin, where we develop a Harder-Narasimhan theory in the framework of bounded lattices, which allows to give a unified proof of the existence and uniqueness of Harder-Narasimhan filtrations. Our result has been verified in Lean by Yijun Yuan.
