BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising Brauer Group and Group Cohomology in Lean4 - Jujian Zh
 ang (Imperial College London)
DTSTART:20250220T170000Z
DTEND:20250220T180000Z
UID:TALK225613@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:The concept of Brauer Groups\, originally developed to classif
 y division algebras\, has now found many uses in scheme theory and class f
 ield theory. Brauer Groups over a field k is defined as the collection of 
 central simple\nalgebras over k modulo certain equivalence relations and t
 his project is set out to formalise the correspondence between the Brauer 
 groups and the second\nGalois cohomology groups Br(k) ≅ H²(Gal(k_sep/k)
  \, k ⃰_sep). In this talk\, we give a complete formalisation between th
 e relative Brauer group of a finite\ndimensional field extension Br(K/k) a
 nd the second group cohomology H²(Gal (K/k) \, K ⃰) as the first step.\
 n\nSlides: https://github.com/Whysoserioushah/BrauerGroup_new\n\nGithub Re
 pository: https://github.com/Whysoserioushah/BrauerGroup_new
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR