Notes and formalizations around Vakil’s The Rising Sea.

Presently, High Tide also uses an as-yet unreleased version of Atlas so it will look quite strange if you’re familiar with Lean.

It’ll look quite strange even if you’re not, but that’s AlgGeo for you.