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⟧ (i.e. A and B are Brauer-equivalent) and K ⊆ B and dim_F B = (dim_F K)²

@[reducible, inline]

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

The relative Brauer group Br(K/F) is the kernel of the 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.carrier K ↔ BrauerGroupHom.BaseChange (Quotient.mk'' A) = 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.carrier K

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

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

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.carrier ≃ₐ[K] Matrix (Fin m) (Fin m) D) ∧ Nonempty (B.carrier ≃ₐ[K] Matrix (Fin n) (Fin n) D)