University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Formalising Brauer Group and Group Cohomology in Lean4

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Formalising Brauer Group and Group Cohomology in Lean4

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Algorithms and Complexity Seminar Robinson College, Cambridge Gatsby Room, Wolfson College, Cambridge, UK, CB3 9BB

Other talks

Beyond Hubble: Studying the Earliest Galaxies with the James Webb Space Telescope Title and abstract tba Title to be confirmed Tea and Coffee Break Discovery Investigations: Science, Empire and the Making of the British South Atlantic Together Now: Cooperation and Collaboration in Social Art Practice
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity