introducing myself: Perry

Stream: new members

[Perry]

Hi everyone, I’m Perry. I was a math major in college, learning Lean right now and looking forward to contributing to mathlib!

Lately I’ve been interested the relationship between combinatorial group theory and category theory, and I’m hoping to eventually make some contributions to mathlib on this topic.

Here are informal statements of what I’m thinking about contributing. Part of the work (fun) for me would be getting a better grasp on the formalism here through attempting to write them in Lean:

—

1) Viewing Grp as a full sub-2-category of Cat, natural transformations between functors f,g: G—>H correspond to elements x \in G satisfying xf(G)x^-1 = g(G).

And the corollaries that, in Grp as defined above…

2) Nat(Id_G,Id_G) \iso Inn(G),

where Id_G is the identity homomorphism on G, and Inn(G) is the inner automorphism group on G.

3) HNN extensions are coinserters in Grp.

—

Since this is a somewhat obscure topic, it’d be great to know if anyone thinks this is outside the scope of mathlib before I start working on this. It seems like I'd be possible to fill up mathlib with tons of categorifications of classical results, which I think are cool in-and-of themselves, but I can't tell if that's the type of thing that the community wants.

Also, if anyone has ideas about what an outline of the work would be to prove these, I’d love to hear it!

I’ll also mention that I’m interested in adding classical theorems from combinatorial group theory too. It’s a little hard to tell what’s already in there right now, but as far as I can tell this topic hasn't made it into mathlib yet. Hoping someone will correct me if I’m wrong :)

Nice to meet you!