Jujian Zhang: Formalising Brauer Group and Group Cohomology in Lean4 (20 Feb 2025) скачать в хорошем качестве

Jujian Zhang: Formalising Brauer Group and Group Cohomology in Lean4 (20 Feb 2025)

In Jujian's talk we had a small technical difficulty which means that the correct slide isn't showing during the first few minutes of the video. His slides can be found here: https://github.com/Whysoserioushah/Br... Abstract: The concept of Brauer Groups, originally developed to classify division algebras, has now found many uses in scheme theory and class field theory. Brauer Groups over a field k is defined as the collection of central simple algebras over k modulo certain equivalence relations and this project is set out to formalise the correspondence between the Brauer groups and the second Galois cohomology groups Br(k) ≅ H²(Gal(k_sep/k) , k ⃰_sep). In this talk, we give a complete formalisation between the relative Brauer group of a finite dimensional field extension Br(K/k) and the second group cohomology H²(Gal (K/k) , K ⃰) as the first step.