A general theory of isomorphism

Stream: maths

[Sebastian Reichelt]

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:

• There is a certain way in which all known individual definitions of isomorphism fall out of this theory as theorems, that I have not seen even e.g. in the HoTT book. It will be more obvious when everything is finished, but for now this table gives an impression: https://github.com/SReichelt/lean4-experiments/blob/900f5da532725ffa2dee8dc931f7bc915e811352/Structure/AbstractBuildingBlocks.lean#L154
• I've found an interesting fact about groupoid functors: Interpreting equivalence/isomorphism of objects in a groupoid as generalized equality, and groupoid functors as generalized functions, I define "injective", "surjective", and "bijective" in a straightforward way. Then each "bijective" functor has an inverse functor, even constructively. See here: https://github.com/SReichelt/lean4-experiments/blob/900f5da532725ffa2dee8dc931f7bc915e811352/Structure/Basic.lean#L831