noncomputable instance module_over_over (k : Type u) [Field k] (A : CSA k) (I : TwoSidedIdeal A.carrier) : Module k ↥I

Equations

• module_over_over k A I = Module.compHom (↥I) (algebraMap k A.carrier)

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 extension_CSA (k K : Type u) [Field k] [Field K] [Algebra k K] (A : CSA k) [FiniteDimensional k K] : CSA K

Equations

• extension_CSA k K A = CSA.mk (TensorProduct k K A.carrier)

noncomputable def extension_inv (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

Equations

• extension_inv k A K = CSA.mk A

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 : ℕ) (_ : NeZero n) (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) : ℕ

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.carrier

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)

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

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

Equations

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

noncomputable def split_by_alg_closure (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

Equations

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

noncomputable def extension_over_split (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'

Equations

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