Splitting central simple algebras

This file ports the upstream splitting-field infrastructure for central simple algebras.

@[implicit_reducible]

noncomputable instance moduleOverOver (k : Type u) [Field k] (A : CSA k) (I : TwoSidedIdeal ↑A.toAlgCat) : Module k ↥I

Equations

• moduleOverOver k A I = Module.compHom (↥I) (algebraMap k ↑A.toAlgCat)

theorem is_simple_A (k A K : Type u) [Field k] [Field K] [Algebra k K] [Ring A] [Algebra k A] [IsSimpleRing (TensorProduct k K A)] : IsSimpleRing A

theorem central_over_extension_iff_subsingleton (k A K : Type u) [Field k] [Field K] [Algebra k K] [Ring A] [Algebra k A] [Subsingleton A] [FiniteDimensional k A] [FiniteDimensional k K] : Algebra.IsCentral k A ↔ Algebra.IsCentral K (TensorProduct k K A)

theorem isSimple_over_extension_iff_subsingleton (k A K : Type u) [Field k] [Field K] [Algebra k K] [Ring A] [Algebra k A] [Subsingleton A] [FiniteDimensional k A] [FiniteDimensional k K] : IsSimpleRing A ↔ IsSimpleRing (TensorProduct k K A)

theorem centralSimple_over_extension_iff_nontrivial (k A K : Type u) [Field k] [Field K] [Algebra k K] [Ring A] [Algebra k A] [Nontrivial A] [FiniteDimensional k A] [FiniteDimensional k K] : Algebra.IsCentral k A ∧ IsSimpleRing A ↔ Algebra.IsCentral K (TensorProduct k K A) ∧ IsSimpleRing (TensorProduct k K A)

theorem centralsimple_over_extension_iff (k A K : Type u) [Field k] [Field K] [Algebra k K] [Ring A] [Algebra k A] [FiniteDimensional k A] [FiniteDimensional k K] : Algebra.IsCentral k A ∧ IsSimpleRing A ↔ Algebra.IsCentral K (TensorProduct k K A) ∧ IsSimpleRing (TensorProduct k K A)

noncomputable def extensionCSA (k K : Type u) [Field k] [Field K] [Algebra k K] (A : CSA k) : CSA K

Scalar extension of a central simple algebra is again a central simple algebra.

Equations

• extensionCSA k K A = { toAlgCat := AlgCat.of K (TensorProduct k K ↑A.toAlgCat), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

noncomputable def extensionInv (k A K : Type u) [Field k] [Field K] [Algebra k K] [Ring A] [Algebra k A] [FiniteDimensional k A] [Algebra.IsCentral K (TensorProduct k K A)] [IsSimpleRing (TensorProduct k K A)] [FiniteDimensional K (TensorProduct k K A)] [FiniteDimensional k K] : CSA k

Descend a central simple algebra structure from a finite scalar extension.

Equations

• extensionInv k A K = { toAlgCat := AlgCat.of k A, isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

theorem CSA_iff_exist_split (k A : Type u) [Field k] [Ring A] [Algebra k A] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] [hA : FiniteDimensional k A] : Algebra.IsCentral k A ∧ IsSimpleRing A ↔ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (L : Type u) (x : Field L) (x_1 : Algebra k L) (_ : FiniteDimensional k L), Nonempty (TensorProduct k L A ≃ₐ[L] Matrix (Fin n) (Fin n) L)

theorem dim_is_sq (k A : Type u) [Field k] [Ring A] [Algebra k A] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] [Algebra.IsCentral k A] [IsSimpleRing A] [FiniteDimensional k A] : IsSquare (Module.finrank k A)

noncomputable def deg (k : Type u) [Field k] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] (A : CSA k) : ℕ

The degree of a central simple algebra, defined by the square root of its dimension.

Equations

• deg k k_bar A = Exists.choose ⋯

theorem deg_sq_eq_dim (k : Type u) [Field k] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] (A : CSA k) : deg k k_bar A ^ 2 = Module.finrank k ↑A.toAlgCat

instance deg_pos (k : Type u) [Field k] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] (A : CSA k) : NeZero (deg k k_bar A)

structure split (k : Type u) [Field k] (A : CSA k) (K : Type u_1) [Field K] [Algebra k K] : Type (max u_1 u_2)

Data witnessing that a field extension splits a central simple algebra.

• n : ℕ

  The matrix size after scalar extension.

• hn : NeZero self.n
• iso : TensorProduct k K ↑A.toAlgCat ≃ₐ[K] Matrix (Fin self.n) (Fin self.n) K

  The scalar-extended algebra is a matrix algebra over the extension field.

noncomputable def isSplit (k A : Type u) [Field k] [Ring A] [Algebra k A] (L : Type u) [Field L] [Algebra k L] : Prop

A field extension splits an algebra if the scalar extension is a matrix algebra.

Equations

• isSplit k A L = ∃ (n : ℕ) (_ : NeZero n), Nonempty (TensorProduct k L A ≃ₐ[L] Matrix (Fin n) (Fin n) L)

noncomputable def splitByAlgClosure (k : Type u) [Field k] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] (A : CSA k) : split k A k_bar

Any algebraic closure splits a central simple algebra.

Equations

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

noncomputable def extensionOverSplit (k : Type u) [Field k] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar] (A : CSA k) (L L' : Type u) [Field L] [Field L'] [Algebra k L] (hA : split k A L) [Algebra L L'] [Algebra k L'] [IsScalarTower k L L'] : split k A L'

Splitting is preserved after extending the splitting field.

Equations

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

theorem extensionOverSplit' (k : Type u) [Field k] (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] (A : Type u) [Ring A] [IsSimpleRing A] [Algebra k A] [Algebra.IsCentral k A] [FiniteDimensional k A] (L L' : Type u) [Field L] [Field L'] [Algebra k L] (hA : isSplit k A L) [Algebra L L'] [Algebra k L'] [IsScalarTower k L L'] : isSplit k A L'

Splitting of an algebra is preserved after extending the splitting field.