Formalising Brauer Group and Group Cohomology in Lean4

Add to your list(s) Download to your calendar using vCal

• Jujian Zhang (Imperial College London)
• Thursday 20 February 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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.

Slides: https://github.com/Whysoserioushah/BrauerGroup_new

Github Repository: https://github.com/Whysoserioushah/BrauerGroup_new

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.