Zulip Chat Archive

Stream: general

Topic: Presentation by Corentin Cornou

Johan Commelin (Jul 18 2024 at 13:21):

Next week, 2024-07-24T15:00:00+02:00, there will be an online talk by @Corentin Cornou about his internship in Utrecht on the topic of formalizing aspects of finite groups of Lie type. Everyone interested in this topic is welcome to attend the presentation.

Title: A step towards the formalization of the finite groups of Lie type

Abstract: The classification of finite simple groups (CFSG) is one of the most important achievements of 20th century mathematics. It states that every finite simple group either is a cyclic group of prime order, an alternating group of degree at least 5, a finite group of Lie type or one of the 26 sporadic groups.
The complexity of the statement of the CFSG makes it a perfect candidate for formalization. Most of the groups of the classification being groups of Lie type, formalizing them marks a first step towards the more
general formalization of the whole classification.
The length and complexity of the definition of a group of Lie type raise difficulties concerning its formalization. However, all the finite groups of Lie type are endowed with a BN-pair structure that can be used to characterize
them. The concept of BN-pair (or Tits system) is, in itself, pretty simple and is a formidable tool that can be used to prove nontrivial results or serve as foundation for the formalization of the theory of finite groups of Lie type.
In this talk, we will introduce a formalization in the Lean proof assistant of the notion of BN-pairs, as well as some properties of groups possessing such structure. In particular, we present a framework that can be used to
show the simplicity of simple groups with a BN-pair, and apply it to the case of the projective special linear group over a field. Additionally, we will use the example of the general linear group to give illustrations of the results throughout
the talk.

Join meeting:

https://teams.microsoft.com/l/meetup-join/19%3ameeting_ZmFhYjZjMjctMzc2YS00Mjg4LTk2YzYtNzRiZWM3N2RhOGJl%40thread.v2/0?context=%7b%22Tid%22%3a%22d72758a0-a446-4e0f-a0aa-4bf95a4a10e7%22%2c%22Oid%22%3a%221b1832e2-2ac0-437c-b4a8-4128da4efb97%22%7d

Meeting ID: 343 175 558 530
Passcode: dua9Kn