Relative Brauer Group

Main results

• BrauerGroup.split_iff: Let A be a CSA over F, then ⟦A⟧ ∈ Br(K/F) if and only if K splits A.
• isSplit_iff_dimension: Let A be a CSA over F, then ⟦A⟧ ∈ Br(K/F) if and only if there exists another F-CSA B such that ⟦A⟧ = ⟦B⟧, K ⊆ B, and dim_F B = (dim_F K)^2.

@[reducible, inline]

noncomputable abbrev RelativeBrGroup (K F : Type u) [Field K] [Field F] [Algebra F K] : Subgroup (BrauerGroup F)

The relative Brauer group Br(K/F) is the kernel of the base-change map Br F → Br K.

Equations

• RelativeBrGroup K F = BrauerGroupHom.BaseChange.ker

theorem BrauerGroup.split_iff (K F : Type u) [Field K] [Field F] [Algebra F K] (A : CSA F) : isSplit F (↑A.toAlgCat) K ↔ BrauerGroupHom.BaseChange (Quotient.mk'' A) = 1

A central simple algebra is split by K iff its Brauer class base-changes to 1.

theorem mem_relativeBrGroup (K F : Type u) [Field K] [Field F] [Algebra F K] (A : CSA F) : Quotient.mk'' A ∈ RelativeBrGroup K F ↔ isSplit F (↑A.toAlgCat) K

Membership in the relative Brauer group is equivalent to being split by K.

theorem split_sound (K F : Type u) [Field K] [Field F] [Algebra F K] (A B : CSA F) (h0 : IsBrauerEquivalent A B) (h : isSplit F (↑A.toAlgCat) K) : isSplit F (↑B.toAlgCat) K

Brauer-equivalent central simple algebras have the same splitting fields.

theorem split_sound' (K F : Type u) [Field K] [Field F] [Algebra F K] (A B : CSA F) (h0 : IsBrauerEquivalent A B) : isSplit F (↑A.toAlgCat) K ↔ isSplit F (↑B.toAlgCat) K

Brauer-equivalent central simple algebras are split by K simultaneously.

theorem IsBrauerEquivalent.exists_common_division_algebra (K : Type u) [Field K] (A B : CSA K) (h : IsBrauerEquivalent A B) : ∃ (D : Type u) (x : DivisionRing D) (x_1 : Algebra K D) (m : ℕ) (n : ℕ) (_ : NeZero m) (_ : NeZero n), Nonempty (↑A.toAlgCat ≃ₐ[K] Matrix (Fin m) (Fin m) D) ∧ Nonempty (↑B.toAlgCat ≃ₐ[K] Matrix (Fin n) (Fin n) D)

Brauer-equivalent central simple algebras have matrix forms over a common division algebra.