Logarithmic Geometry

Stream: mathlib4

[Amine Koubaa]

I want to write the basics of log geometry. The focus won't be on fs log geometry, but rather more general log geometry, e.g. over valuation rings and their extension

[Christian Merten]

Hi Amine, nice to see you here! Do you already have something specific in mind?

[Amine Koubaa]

Hi Christian. Thanks you too. I was thinking about basing it on some chapters of Ogus book. https://www.cambridge.org/core/books/lectures-on-logarithmic-algebraic-geometry/70AF7196462F4CEC018E2DABA49475F6
I do not know how much interest you have in log schemes, but my objective is checking a proof I did in my phd about the existence of the Cartier operator on valuation rings with log structure.

[Amine Koubaa]

For that specific proof, I only need log rings first. But I think log schemes are interesting for a more general population (e.g. for tropical geometry, tori etc.)
Anyways, I probably need to familiarize myself with monoids in lean. They are defined, but their definition is under Algebra.rings which is quite annoying.

[Kevin Buzzard]

@Amine Koubaa note that we're still struggling with quasicoherent sheaves of modules right now, I suspect that log schemes will be quite a challenge! But maybe I'm being pessimistic?

[Amine Koubaa]

@Kevin Buzzard Then maybe I ll then start with logarithmic rings anyway. I think for the definitions over schemes I do not need quasi-coherence.
But then for any reasonable theorem in algebraic geometry, one needs the concept of quasi-coherence! What is the main hurdle for quasi-coherent sheaves?

[Kevin Buzzard]

There is no technical problem, it's just that we're building mathematics from scratch and nobody is being paid to do it for their job so it can go slowly

[Kevin Buzzard]

Actually I guess I'm being paid to do it but I don't need sheaves right now :-)