Central Simple
Results named in Tau Ceti's TauCeti.Algebra.CentralSimple modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremArtin--Wedderburn over a separably closed field#
A finite-dimensional central simple
K-algebra is a full matrix algebra over K.
IsSimpleRing.exists_algEquiv_matrix_of_isSepClosed.{u, u_1} (K : Type u_1) [Field K] [IsSepClosed K]
(A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A]
[FiniteDimensional K A] :
∃ n, ∃ (_ : NeZero n), Module.finrank K A = n ^ 2 ∧ Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) K)
Lean
Formalized in Tau Ceti as IsSimpleRing.exists_algEquiv_matrix_of_isSepClosed.
Sources
Uses 1 · Used by 9
Spin₅ is a twisted form of Sp₄ · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · TauCeti.brauer2EquivH2_baseChange · The comparison isomorphism · The Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local fieldTheoremThe centralizer theorem#
For a central simple K-subalgebra B of a finite-dimensional
simple K-algebra A, the dimensions of B and of its centralizer are complementary:
finrank K B * finrank K C_A(B) = finrank K A.
This is the dimension count of
TauCeti.finrank_mul_finrank_centralizer_of_isSimpleRing_tensorProduct_mulOpposite, whose one
algebraic hypothesis — simplicity of B ⊗[K] Aᵐᵒᵖ — IsSimpleRing.tensorProduct supplies
from B central simple and Aᵐᵒᵖ simple.
TauCeti.finrank_mul_finrank_centralizer.{u_1, u_2} {K : Type u_1} {A : Type u_2} [Field K] [Ring A]
[Algebra K A] [IsSimpleRing A] [FiniteDimensional K A] (B : Subalgebra K A)
[Algebra.IsCentral K ↥B] [IsSimpleRing ↥B] :
Module.finrank K ↥B * Module.finrank K ↥(Subalgebra.centralizer K ↑B) = Module.finrank K A
TheoremThe dimension count behind the centralizer theorem, asking only for what it uses#
that A
is finite-dimensional and nonzero over the field K — so that the factor of finrank K A cancelled
at the end is nonzero — and that the ring R = B ⊗[K] Aᵐᵒᵖ acting on A is simple. Then
finrank K B * finrank K C_A(B) = finrank K A.
Simplicity of R is the only algebraic hypothesis on B and on A, and there is more than one way
to supply it: TauCeti.finrank_mul_finrank_centralizer has it from B central simple and A
simple, while TauCeti.finrank_mul_finrank_centralizer_of_isField has it from B a subfield and
A central simple.
TauCeti.finrank_mul_finrank_centralizer_of_isSimpleRing_tensorProduct_mulOpposite.{u_1, u_2}
{K : Type u_1} {A : Type u_2} [Field K] [Ring A] [Nontrivial A] [Algebra K A]
[FiniteDimensional K A] (B : Subalgebra K A) [IsSimpleRing (TensorProduct K (↥B) Aᵐᵒᵖ)] :
Module.finrank K ↥B * Module.finrank K ↥(Subalgebra.centralizer K ↑B) = Module.finrank K A
Lean
Formalized in Tau Ceti as TauCeti.finrank_mul_finrank_centralizer_of_isSimpleRing_tensorProduct_mulOpposite.
Sources
Used by 3
TheoremFrobenius' theorem#
A finite-dimensional division algebra over ℝ with centre ℝ is
ℝ-isomorphic either to ℝ or to the Hamilton quaternions ℍ[ℝ].
This is the classification to use when nothing is known about D beyond the hypotheses. If
finrank ℝ D = 4 is already in hand, TauCeti.nonempty_algEquiv_quaternion_of_finrank_eq_four
gives the quaternion isomorphism directly, with no disjunction to discharge.
TauCeti.nonempty_algEquiv_real_or_quaternion.{u_1} (D : Type u_1) [DivisionRing D] [Algebra ℝ D]
[Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] :
Nonempty (D ≃ₐ[ℝ] ℝ) ∨ Nonempty (D ≃ₐ[ℝ] Quaternion ℝ)
TheoremThe Skolem-Noether theorem#
Two K-algebra homomorphisms f g : B →ₐ[K] A from a
finite-dimensional central simple K-algebra B to a finite-dimensional simple K-algebra
A are conjugate: there is a unit u of A with g x = u * f x * u⁻¹ for all x : B.
Finite-dimensionality of B is not among the hypotheses: it follows from them, because f is
injective, B being simple and A nontrivial. The proof does use it, to make B ⊗[K] Aᵐᵒᵖ
Artinian, and with it the classification of modules that produces the conjugating isomorphism.
TauCeti.skolemNoether.{u_1, u_2, u_3} (K : Type u_1) {A : Type u_2} {B : Type u_3} [Field K]
[Ring A] [Algebra K A] [Ring B] [Algebra K B] [IsSimpleRing A] [FiniteDimensional K A]
[Algebra.IsCentral K B] [IsSimpleRing B] (f g : B →ₐ[K] A) : ∃ u, ∀ (x : B), g x = ↑u * f x * ↑u⁻¹
Used by 7
H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local fieldTheoremWedderburn-Artin for central simple algebras#
A finite-dimensional central simple
K-algebra A is isomorphic to a matrix algebra over a finite-dimensional central division
K-algebra D, and then finrank K A = n ^ 2 * finrank K D.
Mathlib's IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite supplies everything except the
centrality of D, which comes from TauCeti.Algebra.IsCentral.of_matrix.
IsSimpleRing.exists_algEquiv_matrix_centralDivisionRing.{u, u_1} (K : Type u_1) [Field K]
(A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A]
[FiniteDimensional K A] :
∃ n,
∃ (_ : NeZero n),
∃ D x x_1,
∃ (_ : Algebra.IsCentral K D) (_ : FiniteDimensional K D),
Module.finrank K A = n ^ 2 * Module.finrank K D ∧
Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) D)
Lean
Formalized in Tau Ceti as IsSimpleRing.exists_algEquiv_matrix_centralDivisionRing.
Sources
Used by 8
H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local fieldLoading dependency explorer…
The dependency explorer needs JavaScript and its graph data.