Characteristic predicate for central simple algebras

In this file we define the predicate IsCentralSimple K D where K is a field and D is a (noncommutative) K-algebra.

Note that the predicate makes sense just for K a CommRing but it doesn't give the right definition; for a commutative ring base one should use the theory of Azumaya algebras. This adds an extra layer of complication which we don't need. In fact ideals of K immediately give rise to nontrivial quotients of D so there are no central simple algebras in this case according to our definition.

instance MatrixRing.isCentral (K : Type u) [Field K] (ι : Type) [Fintype ι] [Nonempty ι] [DecidableEq ι] : Algebra.IsCentral K (Matrix ι ι K)

instance IsCentralSimple.instAlgebraSubtypeMemSubringCenter_brauerGroup (K : Type u) [Field K] (B : Type u_1) [Ring B] [Algebra K B] : Algebra K ↥(Subring.center B)

Equations

• IsCentralSimple.instAlgebraSubtypeMemSubringCenter_brauerGroup K B = ((algebraMap K B).codRestrict (Subring.center B) ⋯).toAlgebra

theorem IsCentralSimple.TensorProduct.sum_tmul_basis_right_eq_zero' (K : Type u) [Field K] (B : Type u_1) [Ring B] [Algebra K B] (C : Type u_2) [Ring C] [Algebra K C] {ιC : Type u_3} (𝒞 : Basis ιC K C) (s : Finset ιC) (b : ιC → B) (h : ∑ i ∈ s, b i ⊗ₜ[K] 𝒞 i = 0) (i : ιC) : i ∈ s → b i = 0

theorem IsCentralSimple.TensorProduct.sum_tmul_basis_left_eq_zero' (K : Type u) [Field K] (B : Type u_1) [Ring B] [Algebra K B] (C : Type u_2) [Ring C] [Algebra K C] {ιB : Type u_3} (ℬ : Basis ιB K B) (s : Finset ιB) (c : ιB → C) (h : ∑ i ∈ s, ℬ i ⊗ₜ[K] c i = 0) (i : ιB) : i ∈ s → c i = 0

theorem IsCentralSimple.TensorProduct.left_tensor_base_sup_base_tensor_right (K : Type u_1) (B : Type u_2) (C : Type u_3) [CommRing K] [Ring B] [Algebra K B] [Ring C] [Algebra K C] : (Algebra.TensorProduct.map (AlgHom.id K B) (Algebra.ofId K C)).range ⊔ (Algebra.TensorProduct.map (Algebra.ofId K B) (AlgHom.id K C)).range = ⊤

theorem IsCentralSimple.TensorProduct.submodule_tensor_inf_tensor_submodule (K : Type u) [Field K] (B C : Type u) [AddCommGroup B] [Module K B] [AddCommGroup C] [Module K C] (b : Submodule K B) (c : Submodule K C) : LinearMap.range (TensorProduct.map b.subtype LinearMap.id) ⊓ LinearMap.range (TensorProduct.map LinearMap.id c.subtype) = LinearMap.range (TensorProduct.map b.subtype c.subtype)

theorem IsCentralSimple.center_tensorProduct (K : Type u) [Field K] (B C : Type u) [Ring B] [Algebra K B] [Ring C] [Algebra K C] : Subalgebra.center K (TensorProduct K B C) = (Algebra.TensorProduct.map (Subalgebra.center K B).val (Subalgebra.center K C).val).range

noncomputable def IsCentralSimple.centerTensorCenter (K : Type u) [Field K] (B C : Type v) [Ring B] [Algebra K B] [Ring C] [Algebra K C] : TensorProduct K ↥(Subalgebra.center K B) ↥(Subalgebra.center K C) →ₗ[K] TensorProduct K B C

Equations

• IsCentralSimple.centerTensorCenter K B C = TensorProduct.map (Subalgebra.center K B).val.toLinearMap (Subalgebra.center K C).val.toLinearMap

theorem IsCentralSimple.centerTensorCenter_injective (K : Type u) [Field K] (B C : Type v) [Ring B] [Algebra K B] [Ring C] [Algebra K C] : Function.Injective ⇑(centerTensorCenter K B C)

noncomputable def IsCentralSimple.centerTensor (K : Type u) [Field K] (B C : Type u) [Ring B] [Algebra K B] [Ring C] [Algebra K C] : TensorProduct K ↥(Subalgebra.center K B) ↥(Subalgebra.center K C) ≃ₗ[K] ↥(Subalgebra.center K (TensorProduct K B C))

Equations

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

instance IsCentralSimple.TensorProduct.isCentral (K : Type u) [Field K] (A B : Type u) [Ring A] [Algebra K A] [Ring B] [Algebra K B] [isCentral_A : Algebra.IsCentral K A] [isCentral_B : Algebra.IsCentral K B] : Algebra.IsCentral K (TensorProduct K A B)

instance IsCentralSimple.TensorProduct.nontrivial (K : Type u) [Field K] (A B : Type v) [Ring A] [Algebra K A] [Ring B] [Algebra K B] [Nontrivial A] [Nontrivial B] : Nontrivial (TensorProduct K A B)

structure IsCentralSimple.is_obtainable_by_sum_tmul {K : Type u} [Field K] {ιA : Type u_1} {A : Type u_2} {B : Type u_3} [Ring A] [Algebra K A] [Ring B] [Algebra K B] (x : TensorProduct K A B) (𝒜 : Basis ιA K A) (I : TwoSidedIdeal (TensorProduct K A B)) (n : ℕ) : Prop

a non-zero element in an ideal that can be represented as a sum of tensor products of n-terms.

• mem : x ∈ I
• ne_zero : x ≠ 0
• rep : ∃ (s : Finset ιA) (_ : s.card = n) (f : ιA → B), x = ∑ i ∈ s, 𝒜 i ⊗ₜ[K] f i

theorem IsCentralSimple.is_obtainable_by_sum_tmul.exists_minimal_element {K : Type u} [Field K] {A B : Type v} [Ring A] [Algebra K A] [Ring B] [Algebra K B] (ιA : Type u_1) (𝒜 : Basis ιA K A) (I : TwoSidedIdeal (TensorProduct K A B)) (hI : I ≠ ⊥) : ∃ (n : ℕ) (x : TensorProduct K A B), is_obtainable_by_sum_tmul x 𝒜 I n ∧ ∀ (m : ℕ) (y : TensorProduct K A B), is_obtainable_by_sum_tmul y 𝒜 I m → n ≤ m

theorem IsCentralSimple.TensorProduct.map_comap_eq_of_isSimple_isCentralSimple (K : Type u) [Field K] {A B : Type v} [Ring A] [Algebra K A] [Ring B] [Algebra K B] [isSimple_A : IsSimpleOrder (TwoSidedIdeal A)] [isCentral_B : Algebra.IsCentral K B] [isSimple_B : IsSimpleRing B] (I : TwoSidedIdeal (TensorProduct K A B)) : I = TwoSidedIdeal.span (⇑Algebra.TensorProduct.includeLeft '' ↑(TwoSidedIdeal.comap Algebra.TensorProduct.includeLeft I))

instance IsCentralSimple.TensorProduct.simple (K : Type u) [Field K] (A B : Type v) [Ring A] [Algebra K A] [Ring B] [Algebra K B] [isSimple_A : IsSimpleRing A] [isCentral_B : Algebra.IsCentral K B] [isSimple_B : IsSimpleRing B] : IsSimpleRing (TensorProduct K A B)

instance IsCentralSimple.baseChange (K : Type u) [Field K] (D L : Type u) [Ring D] [Algebra K D] [Field L] [Algebra K L] [h : Algebra.IsCentral K D] [IsSimpleRing D] : Algebra.IsCentral L (TensorProduct K L D)

theorem top_eq_ring (R : Type u_2) [Ring R] : ↑⊤ = ⊤

theorem AlgEquiv.isCentral {K : Type u_2} {B : Type u_3} {C : Type u_4} [Field K] [Ring B] [Algebra K B] [hc : Algebra.IsCentral K B] [Ring C] [Algebra K C] (e : B ≃ₐ[K] C) : Algebra.IsCentral K C

theorem CSA_implies_CSA (K : Type u_2) (B : Type u_3) [Field K] [Ring B] [Algebra K B] (n : ℕ) (D : Type u_4) [NeZero n] (h : DivisionRing D) [Algebra K D] (Wdb : B ≃ₐ[K] Matrix (Fin n) (Fin n) D) [Algebra.IsCentral K B] [IsSimpleRing B] : Algebra.IsCentral K D