The Brauer group of a field is a commutative group

Two finite-dimensional central simple K-algebras are Brauer equivalent when they become isomorphic after passing to matrix algebras over them (Mathlib's IsBrauerEquivalent), and BrauerGroup K is the quotient of CSA K by that relation. Mathlib defines that quotient and records making it a group as a TODO; TauCeti/Algebra/BrauerGroup/Basic.lean supplies the constructors, the two moves that leave a Brauer class unchanged, and the behaviour of ⊗[K] under them, and TauCeti/Algebra/BrauerGroup/Trivial.lean supplies the class that will be the identity. This file assembles those pieces into the group.

The multiplication is induced by the tensor product: it is well defined on classes because TauCeti.isBrauerEquivalent_tensorProduct_congr says ⊗[K] respects Brauer equivalence, and associative, commutative and unital because TauCeti.isBrauerEquivalent_tensorProduct_assoc, TauCeti.isBrauerEquivalent_tensorProduct_comm and TauCeti.isBrauerEquivalent_tensorProduct_base say so already at the level of algebras -- in each case up to an actual isomorphism, which is a Brauer equivalence. The one law that is not inherited from an isomorphism of algebras is the existence of inverses: the inverse of the class of A is the class of the opposite algebra Aᵐᵒᵖ, and the reason A ⊗[K] Aᵐᵒᵖ is trivial is the Azumaya isomorphism A ⊗[K] Aᵐᵒᵖ ≃ₐ[K] M_{finrank K A}(K) behind TauCeti.isBrauerTrivial_tensorOp. The new ingredient this file has to supply for that is that Aᵐᵒᵖ is a move on classes at all, TauCeti.isBrauerEquivalent_op_congr.

The universe

The group structure is stated for BrauerGroup.{u, u} K, the classes of central simple algebras living in the same universe as K. This is not incidental: the identity of the group is the class of K itself, so the identity is available exactly when the algebras are allowed to live in the universe of K. The universe-polymorphic statements about BrauerGroup.{u, v} K that do not mention the identity -- for instance the two Subsingleton results of TauCeti/Algebra/BrauerGroup/Trivial.lean -- are unaffected, and TauCeti.BrauerGroup.mk itself is stated in the universe-polymorphic form.

Main definitions and results

• TauCeti.CSA.op: the opposite of a central simple algebra, again a central simple algebra.
• TauCeti.isBrauerEquivalent_op_congr: passing to the opposite algebra respects Brauer equivalence, so it descends to the classes.
• TauCeti.BrauerGroup.mk: the Brauer class of a central simple algebra, with TauCeti.BrauerGroup.inductionOn its elimination principle.
• TauCeti.BrauerGroup.instCommGroup: the Brauer group of a field is a commutative group, with multiplication induced by ⊗[K], identity the class of K, and the class of Aᵐᵒᵖ inverse to the class of A.
• TauCeti.BrauerGroup.mk_eq_one_iff: a class is the identity exactly when its algebras are Brauer trivial; with TauCeti.BrauerGroup.mk_eq_one_of_isSplittingField and TauCeti.BrauerGroup.mk_end as the two standard sources of identity classes.
• TauCeti.BrauerGroup.orderOf_mk_dvd_two: an algebra Brauer equivalent to its own opposite has a class of order dividing 2, with TauCeti.BrauerGroup.orderOf_mk_eq_two the sharp form for a class that is not the identity. The real quaternions are the worked example in TauCeti/Algebra/BrauerGroup/Quaternion.lean.

What is not proved here

The converse of TauCeti.BrauerGroup.mk_eq_one_of_isSplittingField -- that an algebra whose class is the identity is split by K -- needs the uniqueness of the Wedderburn data, which sits above this file in the import order; it is TauCeti.BrauerGroup.mk_eq_one_iff_isSplittingField, in TauCeti/Algebra/BrauerGroup/Splitting.lean. It is also what supplies, in an example such as ℍ[ℝ], the nonidentity hypothesis that TauCeti.BrauerGroup.orderOf_mk_eq_two needs to sharpen the divisibility orderOf (mk (CSA.of ℝ ℍ[ℝ])) ∣ 2 to the equality = 2. The functoriality of BrauerGroup under base change is not taken here either, but it is on record one file up: TauCeti.BrauerGroup.baseChange in TauCeti/Algebra/BrauerGroup/BaseChange.lean, whose kernel is described there as the classes that become Brauer trivial over the extension (TauCeti.BrauerGroup.mk_mem_ker_baseChange_iff). The converse above, one field up, is assembled in TauCeti.BrauerGroup.mk_mem_ker_baseChange_iff_isSplittingField, which identifies that kernel with the classes split by the extension.

References

This is the second bullet of Layer 6 ("The Brauer group as a group") of the semisimple algebras roadmap, pinned there as brauerCommGroup, together with the Brauer-group half of its Hamilton-quaternion worked example. It also settles the first TODO of Mathlib's Mathlib/Algebra/BrauerGroup/Defs.lean. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §2.4, and R. S. Pierce, Associative Algebras, Springer GTM 88 (1982), Chapter 12.

The opposite algebra as a move on Brauer classes

@[reducible, inline]

abbrev TauCeti.CSA.op {K : Type u} [Field K] (A : CSA K) : CSA K

The opposite of a finite-dimensional central simple K-algebra, again a finite-dimensional central simple K-algebra: centrality and simplicity are both stable under ᵐᵒᵖ (instances in Mathlib's Algebra/Central/Basic.lean and RingTheory/SimpleRing/Basic.lean), and so is the dimension.

This is the constructor for the inverse of the group law on BrauerGroup K (TauCeti.BrauerGroup.mk_op); the reason it is an inverse is TauCeti.isBrauerTrivial_tensorOp.

Equations

• TauCeti.CSA.op A = TauCeti.CSA.of K (↑A.toAlgCat)ᵐᵒᵖ

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

Passing to the opposite algebra respects Brauer equivalence, so it descends to a map of Brauer classes.

The witness is the one of the hypothesis, in the same two sizes: transposition identifies Mₙ(Aᵐᵒᵖ) with Mₙ(A)ᵐᵒᵖ (Mathlib's AlgEquiv.mopMatrix), and an isomorphism Mₙ(A) ≃ₐ[K] Mₘ(B) opposes to Mₙ(A)ᵐᵒᵖ ≃ₐ[K] Mₘ(B)ᵐᵒᵖ.

Brauer classes

@[reducible, inline]

abbrev TauCeti.BrauerGroup.mk {K : Type u} [Field K] (A : CSA K) : BrauerGroup K

The Brauer class of a finite-dimensional central simple K-algebra.

Mathlib's BrauerGroup K is the quotient of CSA K by Brauer.CSA_Setoid K, which is a def and not an instance, so the quotient notation ⟦A⟧ is unavailable; this is the name for the projection that the lemmas below are stated in terms of.

Equations

• TauCeti.BrauerGroup.mk A = ⟦A⟧

theorem TauCeti.BrauerGroup.inductionOn {K : Type u} [Field K] {motive : BrauerGroup K → Prop} (x : BrauerGroup K) (h : ∀ (A : CSA K), motive (mk A)) : motive x

To prove a property of every Brauer class, it suffices to prove it for the class of every finite-dimensional central simple algebra.

@[simp]

theorem TauCeti.BrauerGroup.mk_eq_mk_iff {K : Type u} [Field K] {A B : CSA K} : mk A = mk B ↔ IsBrauerEquivalent A B

Two algebras have the same Brauer class exactly when they are Brauer equivalent.

theorem TauCeti.BrauerGroup.mk_eq_mk_of_algEquiv {K : Type u} [Field K] {A B : CSA K} (e : ↑A.toAlgCat ≃ₐ[K] ↑B.toAlgCat) : mk A = mk B

Isomorphic algebras have the same Brauer class.

@[simp]

theorem TauCeti.BrauerGroup.mk_matrix {K : Type u} [Field K] (A : CSA K) (n : ℕ) [NeZero n] : mk (CSA.matrix A n) = mk A

Passing to matrices does not change the Brauer class.

The group structure

@[instance_reducible]

instance TauCeti.BrauerGroup.instCommGroup {K : Type u} [Field K] : CommGroup (BrauerGroup K)

The Brauer group of a field is a commutative group.

Multiplication is induced by the tensor product over K, which respects Brauer equivalence (TauCeti.isBrauerEquivalent_tensorProduct_congr); the identity is the class of K itself; and the inverse of the class of A is the class of Aᵐᵒᵖ, which respects Brauer equivalence by TauCeti.isBrauerEquivalent_op_congr and is an inverse by TauCeti.isBrauerTrivial_tensorOp. Associativity, commutativity and the unit law hold already for the algebras, up to isomorphism.

The universe is pinned at BrauerGroup.{u, u} K because the identity is the class of K, which lives in Type u; see the module docstring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.BrauerGroup.mk_tensorProduct {K : Type u} [Field K] (A B : CSA K) : mk (CSA.tensorProduct A B) = mk A * mk B

The class of a tensor product is the product of the classes: the defining property of the multiplication of BrauerGroup K.

@[simp]

theorem TauCeti.BrauerGroup.mk_base {K : Type u} [Field K] : mk (CSA.base K) = 1

The class of K is the identity of BrauerGroup K.

@[simp]

theorem TauCeti.BrauerGroup.mk_op {K : Type u} [Field K] (A : CSA K) : mk (CSA.op A) = (mk A)⁻¹

The class of the opposite algebra is the inverse class: the defining property of the inversion of BrauerGroup K.

Identity classes

@[simp]

theorem TauCeti.BrauerGroup.mk_eq_one_iff {K : Type u} [Field K] {A : CSA K} : mk A = 1 ↔ IsBrauerTrivial A

A class is the identity exactly when its algebras are Brauer trivial.

This is the definition of TauCeti.IsBrauerTrivial read in the group: it is the statement that the identity class is the class of the split algebras, and every recognition of an identity class below goes through it.

theorem TauCeti.BrauerGroup.mk_eq_one_of_isSplittingField {K : Type u} [Field K] {A : Type u} [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (h : Algebra.IsSplittingField K A K) : mk (CSA.of K A) = 1

An algebra split by its own base field has identity Brauer class.

The converse is not available here: it needs the uniqueness of the division algebra in a Brauer class. See the module docstring.

theorem TauCeti.BrauerGroup.mk_end {K : Type u} [Field K] (V : Type u) [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] : mk (CSA.of K (Module.End K V)) = 1

The endomorphism algebra of a nonzero finite-dimensional vector space has identity Brauer class. Every full matrix algebra over K is such an End_K V up to isomorphism, and this is the form in which the identity class gets used downstream: A ⊗[K] Aᵐᵒᵖ is an End_K A.

Classes of order two

theorem TauCeti.BrauerGroup.inv_mk_eq_mk_of_isBrauerEquivalent_op {K : Type u} [Field K] {A : CSA K} (h : IsBrauerEquivalent A (CSA.op A)) : (mk A)⁻¹ = mk A

An algebra Brauer equivalent to its own opposite has a self-inverse Brauer class.

theorem TauCeti.BrauerGroup.inv_mk_eq_mk_of_algEquiv_op {K : Type u} [Field K] {A : CSA K} (e : ↑A.toAlgCat ≃ₐ[K] (↑A.toAlgCat)ᵐᵒᵖ) : (mk A)⁻¹ = mk A

An algebra isomorphic to its own opposite has a self-inverse Brauer class.

This is the Brauer-group reading of an isomorphism A ≃ₐ[K] Aᵐᵒᵖ: since the class of Aᵐᵒᵖ is the inverse class, such an isomorphism says the class of A is its own inverse, equivalently that A ⊗[K] A is Brauer trivial.

theorem TauCeti.BrauerGroup.orderOf_mk_dvd_two {K : Type u} [Field K] {A : CSA K} (h : IsBrauerEquivalent A (CSA.op A)) : orderOf (mk A) ∣ 2

An algebra Brauer equivalent to its own opposite has a class of order dividing 2.

The order is exactly 2 unless the class is the identity, that is, unless A is Brauer trivial (TauCeti.BrauerGroup.orderOf_mk_eq_two); ruling that out is a separate matter, discussed in the module docstring.

theorem TauCeti.BrauerGroup.orderOf_mk_dvd_two_of_algEquiv_op {K : Type u} [Field K] {A : CSA K} (e : ↑A.toAlgCat ≃ₐ[K] (↑A.toAlgCat)ᵐᵒᵖ) : orderOf (mk A) ∣ 2

An algebra isomorphic to its own opposite has a class of order dividing 2.

theorem TauCeti.BrauerGroup.orderOf_mk_eq_two {K : Type u} [Field K] {A : CSA K} (h : IsBrauerEquivalent A (CSA.op A)) (h1 : mk A ≠ 1) : orderOf (mk A) = 2

A self-opposite Brauer class other than the identity has order exactly 2. This is the sharp form of TauCeti.BrauerGroup.orderOf_mk_dvd_two.

theorem TauCeti.BrauerGroup.orderOf_mk_eq_two_of_algEquiv_op {K : Type u} [Field K] {A : CSA K} (e : ↑A.toAlgCat ≃ₐ[K] (↑A.toAlgCat)ᵐᵒᵖ) (h1 : mk A ≠ 1) : orderOf (mk A) = 2

An algebra isomorphic to its own opposite, but not split, has a class of order exactly 2.

Worked examples