Quinn La Fond

Stream: new members

[Quinn La Fond]

Hi All,

My name is Quinn La Fond, I am currently a PhD student at the University of Oregon primarily interested in algebraic geometry. I know very little about lean but want to get involved. Any suggestions on where/how to get started would be greatly appreciated!

Best,

Quinn

[Yaël Dillies]

Hey, nice to meet you Quinn! There are many resources to get you started. Given your interests, here are the main two:

• The Natural Number Game, if you haven't done it already
• Mathematics in Lean: #mil

[Quinn La Fond]

Thank you for the resources Yael, I will look into them

[Yaël Dillies]

There are a few ongoing algebraic geometry community projects at the moment:

• #FLT to formalise the proof of Fermat's Last Theorem, run by @Kevin Buzzard
• #toric to formalise the theory of toric varieties, run by @Michał Mrugała and myself

[Yaël Dillies]

You can look into them once you are done with the above resources :slight_smile:

[Quinn La Fond]

Thank you this very helpful!

[Michał Mrugała]

Something tells me Toric might be exciting to work on in the near future, call it intuition

[Andrew Yang]

Welcome! We are definitely low on algebraic geometry contributors :grinning:. Aside from the big ones above, there are also some more smaller but self contained directions that might be interesting and I am happy to talk about/collaborate on them.

• Quasi-finite morphisms & Generically finite morphisms
• Normal schemes & Regular schemes
• Segre embedding & Veronese map etc.
• EGA VI 8 (e.g. stacks#01ZC)
• A weak form of Zariski main theorem following Qing Liu
• Showing that a presheaf of modules $M$ is a quasi-coherent sheaf if and only if $M(D(f)) = M(U)_f$ for every affine open $U$.
• Algebraic groups & abelian varieties etc

(I found this list somewhere in some DMs that I sent and I think this list should be public anyways)

[Quinn La Fond]

Hi Andrew,

These look like exciting topics, particularly the first two. I finished the natural number game, do you have advice on what to do next?

Best,

Quinn

[Kenny Lau]

@Quinn La Fond if you feel like it, maybe you could try... playing NNG in term mode

[Quinn La Fond]

What do you mean? Like using the editor?

[Kenny Lau]

but also it's really like, you can just do whatever you want, say pick something simple that might interest you, or maybe pick something that is already in mathlib and try to do it yourself and then compare, etc. etc.

[Kenny Lau]

Quinn La Fond said:

What do you mean? Like using the editor?

-- term mode
example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c :=
  Eq.trans h₁ h₂

-- tactic mode
example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
  rw [h₁, h₂]

[Kenny Lau]

term mode means that you have to actually construct the term corresponding to the proof (for comparison, a term of the type Nat is mathematically a natural number)

[Kenny Lau]

term mode is the default mode, you use by to go from term mode to tactic mode, and exact to go from tactic mode to term mode

[Kenny Lau]

tactic mode allows you to use tactics (i.e. programs) to generate proofs

[Kenny Lau]

-- tactic mode
theorem foo (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
  rw [h₁, h₂]
#print foo
/-
theorem foo : ∀ (a b c : Nat), a = b → b = c → a = c :=
fun a b c h₁ h₂ =>
  Eq.mpr (id (congrArg (fun _a => _a = c) h₁)) (Eq.mpr (id (congrArg (fun _a => _a = c) h₂)) (Eq.refl c))
-/

[Kenny Lau]

For example, if you name your theorem foo and prove it in tactic mode, and then run the command #print foo, then you can see the term mode proof that the tactics actually generated

[Kenny Lau]

in some sense, only term mode proofs are "real" proofs, the tactics are only programs to generate term mode proofs

[Kenny Lau]

which is why they call it metaprogramming

[Kenny Lau]

a program (tactics) to write a program (the term)

[Kenny Lau]

also i have to say, all of this heavily depends on what you actually want to do

[Quinn La Fond]

I see, so I should get used to using term mode?

[Kenny Lau]

it would be a good thing to know some term mode

[Quinn La Fond]

Ok great, on it! Thank you

[Kenny Lau]

for example, it's recommended that you define data using term mode, because otherwise it would be a bit difficult to reason about them later

[Kenny Lau]

(data means anything that is not a proposition, e.g. if you define fib n for n : Nat)

[Kenny Lau]

theorems do not have the same problem because proofs are never unfolded

[Kenny Lau]

#new members > Quinn La Fond @ 💬
if you look back at this, it doesn't really matter that the short by rw [h1, h2] program generated a larger term, because that large term is never unfolded, so you never have to reason about it

[Luigi Massacci]

Quinn La Fond said:

Hi Andrew,

These look like exciting topics, particularly the first two. I finished the natural number game, do you have advice on what to do next?

Best,

Quinn

I think the standard (and probably best) advice for mathematicians is to read a bit of #mil afterwards

[Andrew Yang]

It highly depends on what's your preferred way of learning is. Mathematics in lean is a fantastic book and is a great intro especially if you enjoy reading. Alternatively if you want a more practical hands on approach I am also happy to work on some of the items above with you.

[Kevin Buzzard]

We currently have a (bad) definition of an elliptic curve over a ring (bad because it's the nonsingular plane cubic definition and there are some elliptic curves over rings which aren't elliptic curves in our sense). A better definition would be to define an elliptic curve E over a scheme S as a scheme over S and a section such that S has a cover by open affines over each of which E is isomorphic to the curve corresponding to a plane cubic. That would be an interesting project

[Kenny Lau]

(I'm currently in the process of making the projective space and it's been taking me almost a week now)

[Junyan Xu]

Are you building a graded algebra structure on MvPolynomial (I think there's some mathlib3 PR?) or glueing affine spaces / tori (is this in the toric project yet?) or something else

[Quinn La Fond]

Kenny Lau said:

(I'm currently in the process of making the projective space and it's been taking me almost a week now)

As in lean currently does have the Proj construction?

[Kenny Lau]

@Junyan Xu @Quinn La Fond Lean does have Proj, and there is also a grading on MvPolynomial, and gluing also exists (so pullbacks exist), but nobody has actually built concretely the space P^n, and it's actually more complicated than one might first think

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/kckennylau/projective/Mathlib/AlgebraicGeometry/ProjectiveSpace.lean

[Kenny Lau]

for reference, this is the code I have, and it reveals that there are some lemmas missing to make the construction, and the preamble actually takes up 3x the space of the actual content

[Michał Mrugała]

Junyan Xu said:

Are you building a graded algebra structure on MvPolynomial (I think there's some mathlib3 PR?) or glueing affine spaces / tori (is this in the toric project yet?) or something else

Could you clarify what are you referring to with (is this in toric yet)?

[Junyan Xu]

I mean the functor from fans to schemes

[Michał Mrugała]

Still far away from that

[Junyan Xu]

https://github.com/leanprover-community/mathlib4/blob/kckennylau/projective/Mathlib/AlgebraicGeometry/ProjectiveSpace.lean

Looks like you've identified certain basic opens in the projective space with affine spaces, and their pairwise intersections with complements of hyperplanes, which are nice and a lot more than just writing down the definition.

[Junyan Xu]

It seems you haven't showed (and it's not in the to-do list) that the projective space over Spec S is isomorphic to the Proj of the graded MvPolynomial algebra over S.

[Kenny Lau]

Junyan Xu said:

It seems you haven't showed (and it's not in the to-do list) that the projective space over Spec S is isomorphic to the Proj of the graded MvPolynomial algebra over S.

it’s actually the biggest goal, called SpecIso there and i also wrote a huge comment above it to explain my plan