Matej Penciak

Stream: new members

[Matej Penciak]

Hello everyone, my name is Matej Penciak. I'm in my last year as a postdoc at Northeastern University, and I usually think about things in the realm of algebraic geometry, representation theory, and integrable systems. I've been getting progressively more interested in Lean and Mathlib for about 2 years now (since I first heard about the liquid tensor experiment), but it was only in the last few months that I've decided to dive headfirst into it. I'm really interested in contributing, and I would love to join a team working on any of the AG parts of mathlib.

I already have a small project that's in a really rough state showing that the homotopy_category of homological_complex's of a preadditive category is preadditive. It's basically done except for a couple sorry's where I need to think through some things about zero divisors, but it's VERY far from being nice and polished.

I'm also really interested in using mathlib for teaching, and I've been running an undergraduate seminar here at Northeastern. It's something like the blind leading the blind, but I find the process of preparing for the next week's material has really helped me solidify my understanding. We're still pretty early on, but a link to seminar material is here.

[Johan Commelin]

@Matej Penciak Welcome!

[Kevin Buzzard]

I learnt the same sort of way as you; teaching an "introduction to proof" class of 300 students and not really having a clue about how to do even the most basic things when I started, but working hard to stay ahead of the problem sheets!

Did you know about the algebraic geometry project? It's here. @Andrew Yang is one of the main people working on it. He's working through basically chapter 2 of Hartshorne. @Jujian Zhang is working on defining projective space and more generally Proj of a ring (in fact he's finished, but the results aren't PR'ed yet). If you want to get more ambitious, we could do with the definition of an \'etale morphism of rings and then of schemes, for the obvious reason.

[Andrew Yang]

Welcome! For my part of the AG project, I am currently trying to define various classes of morphisms. There are a few Hartshorne exercises that needs to be sorted out if you are into them. OTOH, the commutative algebra library is also lacking and it would be great if someone can work on them. I believe we do not know what flat/smooth/etale morphisms are. And we do not know much about morphism classes in general as well, as shown in #4013

[Patrick Massot]

Matej, given your project, you should probably coordinate with @Joël Riou

[Patrick Massot]

The first thing I saw in your README can be optimized. You wrote leanproject get https://github.com/mpenciak/Lean-Seminar-Sp2022.git but leanproject get mpenciak/Lean-Seminar-Sp2022 will do the same

[Andrew Yang]

I think there is also a proof of the homotopy category being preadditive in the liquid tensor experiment.
The relevant file

[Patrick Massot]

If you want to know what Joël has been doing in mathlib you can go to https://github.com/leanprover-community/mathlib/pulls?q=+is%3Apr+author%3Ajoelriou+

[Joël Riou]

Actually, I have almost not looked at anything related to algebraic geometry in mathlib yet. My first contributions are all preliminaries to the inclusion of a proof of the Dold-Kan equivalence between chain complexes and simplicial objects in abelian categories.

[Matej Penciak]

Andrew Yang said:

Welcome! For my part of the AG project, I am currently trying to define various classes of morphisms. There are a few Hartshorne exercises that needs to be sorted out if you are into them. OTOH, the commutative algebra library is also lacking and it would be great if someone can work on them. I believe we do not know what flat/smooth/etale morphisms are. And we do not know much about morphism classes in general as well, as shown in #4013

This seems right up my alley! Before I did anything with the homotopy category I tried to prove some stuff about primary ideals, but I was having a really hard time because I wasn't quite ready yet to dive into "interesting math" (as upposed to the "uninteresting" LFTCM2020 exercises haha). I'll take some time looking into any chunks I might want to take a bite out of later.

[Patrick Massot]

Joël I mentioned you because Matej wrote: "I already have a small project that's in a really rough state showing that the homotopy_category of homological_complex's of a preadditive category is preadditive. "

[Matej Penciak]

Patrick Massot said:

The first thing I saw in your README can be optimized. You wrote leanproject get https://github.com/mpenciak/Lean-Seminar-Sp2022.git but leanproject get mpenciak/Lean-Seminar-Sp2022 will do the same

Thanks for the tip, the whole Lean toolchain is a bit of a blackbox for me so I'm still trying to figure out what I can and can't get away with.

[Patrick Massot]

This is really a tiny detail.

[Patrick Massot]

You could have learned that particular trick at https://leanprover-community.github.io/leanproject.html#getting-an-existing-lean-3-project

[Patrick Massot]

You can read that whole page if you are curious, and even push to https://leanprover-community.github.io/toolchain.html if you are very curious

[Matej Penciak]

Andrew Yang said:

I think there is also a proof of the homotopy category being preadditive in the liquid tensor experiment.
The relevant file

I have much to learn! My file is 500+ lines (to be fair, it's a lot of copy and pasting) and it was a huge slog with multiple instances of crazy applications of @quot.sound, @comp_closure and @homotopic :flushed: . I did it mostly to learn how quotients work in a real life setting.