Zulip Chat Archive

Hi, I'm relatively new to Lean. Currently, I'm working with @Moritz Firsching and @Fabian Kruse on Stirling's formula. Mathematically, I'm mostly interested in Algebraic Geometry and related topics.
I'd like to ask for access to non-master mathlib branches. My Github username is nick-kuhn.

Bolton Bailey (Jun 17 2022 at 15:03):

@maintainers

Bryan Gin-ge Chen (Jun 17 2022 at 15:28):

Invite sent! https://github.com/leanprover-community/mathlib/invitations

Kevin Buzzard (Jun 17 2022 at 17:20):

Hi Nick! A really important project which needs doing in algebraic geometry is defining all the standard predicates on morphisms (for example being locally of finite type or smooth or proper or flat etc)

Kevin Buzzard (Jun 17 2022 at 17:22):

There should be some general abstraction where you put in some predicate of ring morphisms (for example flatness) and then prove some basic properties about it and the abstraction spits out a predicate on morphisms of schemes which extends the ring predicate

Kevin Buzzard (Jun 17 2022 at 17:22):

"Define in Lean what it means for a morphism of schemes to be flat" is a very accessible and fun-looking project

Kevin Buzzard (Jun 17 2022 at 17:23):

My PhD student Jujian has defined projective schemes. You could be a consumer of his work and define projective morphisms.

Nikolas Kuhn (Jun 22 2022 at 21:18):

Kevin Buzzard said:

There should be some general abstraction where you put in some predicate of ring morphisms (for example flatness) and then prove some basic properties about it and the abstraction spits out a predicate on morphisms of schemes which extends the ring predicate

Thanks for the suggestion! It might indeed be fun to implement e.g. the "affine communication Lemma" (as Ravi Vakil calls it), and apply it to some properties. I might give this a try.