Formalising math behind module-action in cryptography

Stream: general

[Gareth Ma]

tldr: Would algebra/cat-theory results from https://eprint.iacr.org/2024/1556.pdf e.g. Section 2, Section 3 and Appendix A be interesting to the Mathlib community?

Background: This paper by Damien gives a framework and a construction in isogeny-based cryptography while also unifies several other constructions in the past, so it has some significance there. (Not sure how much cryptography I should mention here but I can elaborate if needed.)

Mathematically speaking, he constructs a symmetric monoidal action of [a bunch of quantifiers here] R-modules acting on [a bunch of quantifiers here] abelian varieties (and group schemes too), see Theorem 4.9. But to do that, he first develops this theory with category of abelian varieties replaced by an R-oriented abelian category (Section 3.4 and 3.5). From the perspective of Lean, this would be perfect, since (afaik) this is just (non-)commutative algebra and category theory now.

For a concrete example, see the proof of Theorem 3.7. It's purely category theory and commutative algebra, so I would imagine it fits Mathlib pretty well. What do people think?

[Notification Bot]

This topic was moved here from #general > About Hermitian Modules and Similitudes by Gareth Ma.

[Gareth Ma]

Not sure what to name this thread or where to put it :sweat:

[Yaël Dillies]

How related is it to things we've been developing in Toric? Eg group schemes here or actions

[Gareth Ma]

I am very sorry for not replying. I was forced to go out last night and I’m slightly busy now, so I’ll check out your Toric project then reply soon-ish

[Gareth Ma]

I am very sorry for not replying. I was forced to go out last night and I’m slightly busy now, so I’ll check out your Toric project then reply soon-ish

[Gareth Ma]

Did I send it twice or is my client bugging

image.png

[Gareth Ma]

Either way, Zulip is bugging. Anyways

[Gareth Ma]

Let me split the crypto(graphy) paper into three parts: the "R-modules acting on R-oriented abelian category (a symmetric monoidal functor)" part (Section 2-3), the "use the abelian category of <insert qualifiers here> group scheme, then prove nice stuff about the orbit" (Section 4), and "crypto" (Section 6).

I was more immediately interested in Section 2-3 because it's just algebra, which to my understanding Mathlib is good at. For that, (AFAIK) Toric project isn't very relevant.

But for section 4, instantiating the functor construction with category of commutative proper group schemes, I believe the Toric project will be more closely related. I assume the main result needed ("category of commutative proper of group schemes is an abelian category") will become easier as your project develops?

[Gareth Ma]

I also assume algebraic geometry people would want to do that eventually, something something Grothendieck and AB5 and derived functors. IDK geometry.

[Gareth Ma]

By the way, I just spoke to the author of the paper, as I found some issues with it, and he agrees there are several issues, so if there's any interest in this at all it will probably still have to wait for a bit for him to update it

[Gareth Ma]

(Very easy issue in Lemma 2.1: the Ext_R(...) should be Ext_{\overline{R}}(...) using his definition of dual module, but that may cause issues later on regarding orientation)

[Kevin Buzzard]

Category of proper group schemes over a general base isn't an abelian category, it's not even true for finite group schemes, there are problems with quotients

[Gareth Ma]

What about over a field? (and commutative)

[Gareth Ma]

https://www.numdam.org/article/SB_1960-1961__6__99_0.pdf (Grothendieck, Corollary 7.4) constructs quotients/cokernels apparently

[Kevin Buzzard]

LGTM

[Kevin Buzzard]

We're a long way from formalising this stuff though

[Jon Eugster]

Gareth Ma said:

Did I send it twice or is my client bugging

(side note, it's a known Zulip "feature" that messages can be sent multiple times when sent from unstable internet connections, happens fairly often)