LeanPool.BrauerGroupNew.Subfield.Splitting #
Imported Lean Pool material for LeanPool.BrauerGroupNew.Subfield.Splitting.
theorem
exists_embedding_of_isSplit
(K F : Type u)
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
(A : CSA F)
(split : isSplit F (↑A.toAlgCat) K)
:
∃ (B : CSA F),
Quotient.mk'' A * Quotient.mk'' B = 1 ∧ ∃ (x : K →ₐ[F] ↑B.toAlgCat), Module.finrank F K ^ 2 = Module.finrank F ↑B.toAlgCat
A splitting field embeds into a Brauer-equivalent central simple algebra of square dimension.
theorem
isSplit_iff_dimension
(K F : Type u)
[Field K]
[Field F]
[Algebra F K]
[FiniteDimensional F K]
(A : CSA F)
:
isSplit F (↑A.toAlgCat) K ↔ ∃ (B : CSA F),
Quotient.mk'' A = Quotient.mk'' B ∧ ∃ (x : K →ₐ[F] ↑B.toAlgCat), Module.finrank F K ^ 2 = Module.finrank F ↑B.toAlgCat
A splitting criterion in terms of a Brauer-equivalent algebra containing the splitting field.
theorem
isSplit_of_isMax
(F : Type u)
[Field F]
(D : Type u)
[DivisionRing D]
[Algebra F D]
[FiniteDimensional F D]
[Algebra.IsCentral F D]
[IsSimpleRing D]
(L : SubField F D)
(hL : IsMax L)
:
isSplit F D ↥L
A maximal subfield of a central division algebra splits it.