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.carrier K) : ∃ (B : CSA F), Quotient.mk'' A * Quotient.mk'' B = 1 ∧ ∃ (x : K →ₐ[F] B.carrier), Module.finrank F K ^ 2 = Module.finrank F B.carrier

theorem isSplit_iff_dimension (K F : Type u) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] (A : CSA F) : isSplit F A.carrier K ↔ ∃ (B : CSA F), Quotient.mk'' A = Quotient.mk'' B ∧ ∃ (x : K →ₐ[F] B.carrier), Module.finrank F K ^ 2 = Module.finrank F B.carrier

theorem 3.3

@[reducible, inline]

noncomputable abbrev toTensorMatrix_toFun_Flinear (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : TensorProduct F K (Matrix n n A) →ₗ[F] Matrix n n (TensorProduct F K A)

Equations

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

@[simp]

theorem toTensorMatrix_toFun_Flinear_apply (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (a✝ : TensorProduct F K (Matrix n n A)) : (toTensorMatrix_toFun_Flinear K F A n) a✝ = (TensorProduct.liftAux { toFun := fun (k : K) => { toFun := fun (M : Matrix n n A) => k • M.map ⇑Algebra.TensorProduct.includeRight, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) a✝

@[reducible, inline]

noncomputable abbrev toTensorMatrix_toFun_Kliniear (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : TensorProduct F K (Matrix n n A) →ₗ[K] Matrix n n (TensorProduct F K A)

Equations

• toTensorMatrix_toFun_Kliniear K F A n = { toAddHom := (toTensorMatrix_toFun_Flinear K F A n).toAddHom, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev toTensorMatrix (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : TensorProduct F K (Matrix n n A) →ₐ[K] Matrix n n (TensorProduct F K A)

Equations

• toTensorMatrix K F A n = { toFun := (toTensorMatrix_toFun_Kliniear K F A n).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[reducible, inline]

noncomputable abbrev invFun_toFun (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (i j : n) : TensorProduct F K A →ₗ[F] TensorProduct F K (Matrix n n A)

Equations

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

@[reducible, inline]

noncomputable abbrev invFun_Klinear (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (i j : n) : TensorProduct F K A →ₗ[K] TensorProduct F K (Matrix n n A)

Equations

• invFun_Klinear K F A n i j = { toAddHom := (invFun_toFun K F A n i j).toAddHom, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev invFun_linearMap (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : Matrix n n (TensorProduct F K A) →ₗ[K] TensorProduct F K (Matrix n n A)

Equations

• invFun_linearMap K F A n = { toFun := fun (M : Matrix n n (TensorProduct F K A)) => ∑ p : n × n, (invFun_Klinear K F A n p.1 p.2) (M p.1 p.2), map_add' := ⋯, map_smul' := ⋯ }

theorem Martrix.one_eq_sum (F : Type u) [CommSemiring F] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : 1 = ∑ i : n, ∑ j : n, Matrix.stdBasisMatrix i j (if i = j then 1 else 0)

theorem left_inv (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (M : TensorProduct F K (Matrix n n A)) : (invFun_linearMap K F A n) ((toTensorMatrix K F A n) M) = M

theorem right_inv (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (M : Matrix n n (TensorProduct F K A)) : (toTensorMatrix K F A n) ((invFun_linearMap K F A n) M) = M

noncomputable def equivTensor' (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : TensorProduct F K (Matrix n n A) ≃ Matrix n n (TensorProduct F K A)

Equations

• equivTensor' K F A n = { toFun := ⇑(toTensorMatrix K F A n), invFun := ⇑(invFun_linearMap K F A n), left_inv := ⋯, right_inv := ⋯ }

noncomputable def matrixTensorEquivTensor (K F : Type u) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u) (n : Type u_1) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] : TensorProduct F K (Matrix n n A) ≃ₐ[K] Matrix n n (TensorProduct F K A)

Equations

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

theorem isSplit_if_equiv (K F : Type u) [Field K] [Field F] [Algebra F K] (A B : CSA F) (hAB : IsBrauerEquivalent A B) (hA : isSplit F A.carrier K) : isSplit F B.carrier K

theorem maxOfDivision (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 : IsMaximalSubfield F D L) : isSplit F D ↥L