Zulip Chat Archive

Stream: maths

Topic: A general theory of isomorphism

view this post on Zulip Sebastian Reichelt (Mar 14 2021 at 22:20):

I'm building a mathematical theory that, when finished, could potentially automate a lot of things that can be deduced from structure. In contrast to e.g. the "transport" tactic, it works on a mathematical rather than metamathematical level, using groupoid theory. I'm formalizing it in Lean 4 in the hope that it might help with the mathlib port, and would like to share it at this early stage to get some feedback and maybe find collaborators.

The code is at https://github.com/SReichelt/lean4-experiments, and in particular in Structure.lean you will find a description of the idea and current status. At the moment, I've formalized the basic groupoid theory and then just enough to show that the idea really works, but there is still quite a bit of work to do until I can show some examples where the theory actually automates things.

Aside from the intended practical applications, I'm also wondering which parts are mathematically novel (if any). In particular:

Last updated: May 14 2021 at 19:21 UTC