Definition of Brauer group of a field K

We introduce the definition of Brauer group of a field K, which is the quotient of the set of all finite-dimensional central simple algebras over K modulo the Brauer Equivalence where two central simple algebras A and B are Brauer Equivalent if there exist n, m ∈ ℕ+ such that Mₙ(A) ≃ₐ[K] Mₘ(B).

TODOs

1. Prove that the Brauer group is an abelian group where multiplication is defined as tensorproduct.
2. Prove that the Brauer group is a functor from the category of fields to the category of groups.
3. Prove that over a field, being Brauer equivalent is the same as being Morita equivalent.

References

• [Algebraic Number Theory, J.W.S Cassels][cassels1967algebraic]

Tags

Brauer group, Central simple algebra, Galois Cohomology

structure CSA (K : Type u) [Field K] extends AlgCat K : Type (max u (v + 1))

CSA is the set of all finite dimensional central simple algebras over field K, for its generalisation over a CommRing please find IsAzumaya in Mathlib/Algebra/Azumaya/Defs.lean.

• carrier : Type v
• isRing : Ring ↑self.toAlgCat
• isAlgebra : Algebra K ↑self.toAlgCat
• isCentral : Algebra.IsCentral K ↑self.toAlgCat

  Any member of CSA is central.

• isSimple : IsSimpleRing ↑self.toAlgCat

  Any member of CSA is simple.

• fin_dim : FiniteDimensional K ↑self.toAlgCat

  Any member of CSA is finite-dimensional.

instance instCoeSortCSAType {K : Type u} [Field K] : CoeSort (CSA K) (Type v)

Equations

• instCoeSortCSAType = { coe := fun (x : CSA K) => ↑x.toAlgCat }

@[reducible, inline]

abbrev IsBrauerEquivalent {K : Type u} [Field K] (A : CSA K) (B : CSA K) : Prop

Two finite dimensional central simple algebras A and B are Brauer Equivalent if there exist n, m ∈ ℕ+ such that the Mₙ(A) ≃ₐ[K] Mₙ(B).

Equations

• IsBrauerEquivalent A B = ∃ (n : ℕ) (m : ℕ), n ≠ 0 ∧ m ≠ 0 ∧ Nonempty (Matrix (Fin n) (Fin n) ↑A.toAlgCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgCat)

theorem IsBrauerEquivalent.refl {K : Type u} [Field K] (A : CSA K) : IsBrauerEquivalent A A

theorem IsBrauerEquivalent.symm {K : Type u} [Field K] {A : CSA K} {B : CSA K} (h : IsBrauerEquivalent A B) : IsBrauerEquivalent B A

theorem IsBrauerEquivalent.trans {K : Type u} [Field K] {A : CSA K} {B : CSA K} {C : CSA K} (hAB : IsBrauerEquivalent A B) (hBC : IsBrauerEquivalent B C) : IsBrauerEquivalent A C

theorem IsBrauerEquivalent.is_eqv {K : Type u} [Field K] : Equivalence IsBrauerEquivalent

def Brauer.CSA_Setoid (K : Type u) [Field K] : Setoid (CSA K)

CSA equipped with Brauer Equivalence is indeed a setoid.

Equations

• Brauer.CSA_Setoid K = { r := IsBrauerEquivalent, iseqv := ⋯ }

@[reducible, inline]

abbrev BrauerGroup (K : Type u) [Field K] : Type (max u (u_1 + 1))

BrauerGroup is the set of all finite-dimensional central simple algebras quotient by Brauer Equivalence.

Equations

• BrauerGroup K = Quotient (Brauer.CSA_Setoid K)