The centralizer of a central simple subalgebra #
Let K be a field, let A be a finite-dimensional simple K-algebra and let B ⊆ A be a
central simple K-subalgebra. The centralizer theorem says that
C = C_A(B) = {c : A | c commutes with every element of B}
is again a simple K-algebra, and that its dimension is the complementary one:
finrank K B * finrank K C = finrank K A.
The dimension formula is sharpened here to a decomposition: multiplication B ⊗[K] C → A is an
algebra isomorphism, because its source is simple, so that the map is injective, and the two sides
have the same dimension. When A is moreover central simple, the decomposition forces C to be
central as well, since a tensor product of algebras over a field is central only if both factors
are; so C is central simple in turn, the centralizer theorem applies to it, and comparing the two
dimension formulas gives the double centralizer C_A(C) = B.
The proof is the module-theoretic one, and it reuses the bimodule of the Skolem-Noether theorem. The
inclusion B.val : B →ₐ[K] A makes A a module over R = B ⊗[K] Aᵐᵒᵖ
(TauCeti.Bimodule), with b ⊗ₜ op a acting by x ↦ b * x * a. Because B is central simple and
Aᵐᵒᵖ is simple, R is a simple ring (TauCeti.IsSimpleRing.tensorProduct), finite-dimensional
over K. Now an R-linear endomorphism of A is in particular linear for the right action of A,
hence is multiplication on the left by some c : A, and its linearity for the left action of B is
exactly the statement that c commutes with B. So
C ≃ₐ[K] End_R A,
and both conclusions are read off the general facts about the endomorphism algebra of a module over
a simple Artinian algebra proved in TauCeti/RingTheory/Semisimple/EndAlgebra.lean: such an algebra
is simple, and finrank K (End_R A) * finrank K R = (finrank K A)². Since
finrank K R = finrank K B * finrank K A, dividing by finrank K A leaves the dimension formula.
Main results #
TauCeti.centralizerAlgEquivEnd: the identificationC_A(B) ≃ₐ[K] End_{B ⊗[K] Aᵐᵒᵖ} A, by left multiplication. It needs no hypothesis beyondBbeing a subalgebra.TauCeti.centralizer_isSimpleRing: the centralizer of a central simple subalgebra is simple.TauCeti.finrank_mul_finrank_centralizer: the centralizer theorem,finrank K B * finrank K C_A(B) = finrank K A.TauCeti.finrank_mul_finrank_centralizer_of_isField: the same dimension formula for a subfield of a central simple algebra, where centrality is asked of the ambient algebra instead of the subalgebra.TauCeti.tensorCentralizerAlgEquiv: the tensor decompositionB ⊗[K] C_A(B) ≃ₐ[K] A, by multiplication.TauCeti.centralizer_isCentral: the centralizer of a central simple subalgebra of a central simple algebra is central, so thatC_A(B)is central simple again.TauCeti.centralizer_centralizer: the double centralizer theorem,C_A(C_A(B)) = B.TauCeti.deg_mul_deg_centralizer: the degree form of the dimension formula,deg K B * deg K C_A(B) = deg K A.
Implementation notes #
TauCeti.centralizerAlgEquivEnd is stated for an arbitrary subalgebra B of an arbitrary
K-algebra A over a commutative semiring K: neither simplicity nor finite-dimensionality nor
the field structure plays any part in identifying the endomorphism algebra, they enter only when
that algebra is analysed. Keeping the two apart is what makes the identification reusable, for
instance for the double centralizer. The equivalence is characterised on both sides, by
TauCeti.centralizerAlgEquivEnd_apply and TauCeti.centralizerAlgEquivEnd_symm_apply, and the
algebra homomorphism and bijectivity proof it is assembled from are private to this file.
Centrality is asked of B and not of A, exactly as in
TauCeti/Algebra/CentralSimple/SkolemNoether.lean, and for the same reason: what the proof needs is
that B ⊗[K] Aᵐᵒᵖ is simple, which TauCeti.IsSimpleRing.tensorProduct gets from B central
simple and A simple. The roadmap's central simple form is the case Algebra.IsCentral K A, which
these statements cover. Centrality of B cannot be dropped: for K = ℝ, A = ℂ and B = A, the
centralizer is all of ℂ, so finrank ℝ B * finrank ℝ C = 4 ≠ 2 = finrank ℝ A; the worked example
at the end of the file records this.
Because simplicity of B ⊗[K] Aᵐᵒᵖ is all the dimension formula uses, the count itself is proved
once and separately, in
TauCeti.finrank_mul_finrank_centralizer_of_isSimpleRing_tensorProduct_mulOpposite;
TauCeti.finrank_mul_finrank_centralizer is the case of it where that simplicity comes from B
central simple and A simple, and TauCeti.finrank_mul_finrank_centralizer_of_isField the case
where it comes instead from B a subfield of a central simple A.
That last statement asks for IsField ↥L and not for the weaker IsSimpleRing ↥L, which is all
its proof uses. The restriction is a scope boundary and not a mathematical one: stated for a merely
simple subalgebra it is the centralizer theorem for a non-central simple subalgebra, which the
Layer 5 bullet of the roadmap referenced below defers — "the general form for a merely simple
subalgebra B (center Z(B) ⊋ K) ... is a later target, not this one" — to be taken up
together with the description of the centralizer's centre. Nothing is lost in generality by it:
the count itself is stated at the level its proof works at, and a caller with a merely simple L
can use it directly.
Centrality of A, on the other hand, is asked only of the last three statements, and there it
cannot be dropped either: for K = ℝ, A = ℂ and B = ⊥, which is central simple, the centralizer
of B is all of ℂ and so is its centralizer in turn, which is not ⊥. The second worked example
records this.
TauCeti.deg_mul_deg_centralizer is stated here rather than beside the other degree lemmas in
TauCeti/Algebra/CentralSimple/Degree.lean, so that the degree file stays free of the centralizer
machinery: it is a statement about a centralizer, whose only degree input is
TauCeti.Algebra.deg_tensorProduct.
References #
This implements the Layer 5 targets centralizer_isSimpleRing, finrank_mul_finrank_centralizer
and centralizer_centralizer of the
semisimple algebras roadmap.
See R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, and P. Gille, T. Szamuely, Central
Simple Algebras and Galois Cohomology, Chapter 2.
The centralizer of a subalgebra B ⊆ A is the endomorphism algebra of A as a
B ⊗[K] Aᵐᵒᵖ-module, by left multiplication.
No hypothesis on A or B is needed here; the centralizer theorem below is what happens when the
right-hand side is analysed under the hypotheses that make B ⊗[K] Aᵐᵒᵖ simple Artinian.
Equations
Instances For
The forward direction of TauCeti.centralizerAlgEquivEnd: c goes to left multiplication
by c.
The inverse direction of TauCeti.centralizerAlgEquivEnd: an endomorphism is recovered by
evaluating it at 1.
Multiplication B ⊗[K] C_A(B) → A, as a K-algebra homomorphism.
An element of the centralizer commutes with every element of B by definition, which is exactly the
hypothesis under which the universal property of the tensor product of algebras turns the two
inclusions into a single homomorphism out of the tensor product. Like
TauCeti.centralizerAlgEquivEnd it asks nothing of A or B; it becomes an isomorphism under the
hypotheses of the centralizer theorem (TauCeti.tensorCentralizerAlgEquiv).
Equations
Instances For
The 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.
The dimension of the centralizer of a subfield of a central simple algebra is the complementary one:
finrank K L * finrank K C_A(L) = finrank K A.
This is TauCeti.finrank_mul_finrank_centralizer with the centrality hypothesis moved from the
subalgebra to the ambient algebra. The shared dimension count is
TauCeti.finrank_mul_finrank_centralizer_of_isSimpleRing_tensorProduct_mulOpposite, whose one
algebraic hypothesis — that L ⊗[K] Aᵐᵒᵖ be simple —
TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right supplies here from the simplicity of the
field L and the central simplicity of Aᵐᵒᵖ; L itself is not central over K unless it is K,
so the orientation used by TauCeti.finrank_mul_finrank_centralizer does not apply.
The centralizer of a central simple subalgebra of a simple algebra is a simple ring. It is
the endomorphism algebra of A as a module over the simple Artinian algebra B ⊗[K] Aᵐᵒᵖ.
The 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ᵐᵒᵖ — TauCeti.IsSimpleRing.tensorProduct supplies
from B central simple and Aᵐᵒᵖ simple.
The tensor decomposition along a central simple subalgebra: for a central simple
K-subalgebra B of a finite-dimensional simple K-algebra A,
B ⊗[K] C_A(B) ≃ₐ[K] A,
by multiplication. It is TauCeti.tensorCentralizerAlgHom, which a private lemma of this file
shows to be bijective: the source is simple, so the map is injective, and the centralizer theorem
makes the two sides equidimensional, so it is surjective too.
Equations
Instances For
Centrality of the centralizer, and the double centralizer #
The three statements below need A itself to be central simple, and not merely simple. This is
the first point in the file where that is so: the dimension formula and the tensor decomposition
hold over K without assuming that A is central, but C_A(C_A(B)) = B genuinely fails when A
has a larger center, as the second worked example at the end of the file records.
The centralizer of a central simple subalgebra of a central simple algebra is central.
Together with TauCeti.centralizer_isSimpleRing this says that C_A(B) is again central simple, so
that the centralizer theorem may be applied to it in turn.
The proof is the tensor decomposition B ⊗[K] C_A(B) ≃ₐ[K] A transported: the tensor product is
central because A is, and a tensor product of algebras over a field is central only if each factor
is, provided the other one is nontrivial (Algebra.IsCentral.right_of_tensor_of_field); here B is
nontrivial because it is simple.
The double centralizer theorem for a central simple subalgebra. For a central simple
K-subalgebra B of a finite-dimensional central simple K-algebra A,
C_A(C_A(B)) = B.
One inclusion is formal. For the other, C = C_A(B) is itself central simple
(TauCeti.centralizer_isSimpleRing and TauCeti.centralizer_isCentral), so the centralizer theorem
applies to C as well and gives finrank K C * finrank K C_A(C) = finrank K A, while for B it
gives finrank K B * finrank K C = finrank K A. Cancelling finrank K C, which is positive, leaves
finrank K C_A(C) = finrank K B, and a subalgebra containing B with the dimension of B is B.
The inner centralizer is written as the Set.centralizer of ↑B, which is what
Subalgebra.coe_centralizer (a simp lemma) turns the coerced subalgebra into, so that the
left-hand side is in simp normal form; Subalgebra.centralizer_centralizer_centralizer is stated
the same way.
The degree is multiplicative along a central simple subalgebra:
deg K B * deg K C_A(B) = deg K A.
This is the dimension formula with square roots taken, the degree being the square root of the
dimension (TauCeti.Algebra.deg_sq), and it is the shape in which the centralizer theorem is
usually quoted. It is a statement about the degree of C_A(B), so it needs C_A(B) to be
central simple, which is TauCeti.centralizer_isCentral together with
TauCeti.centralizer_isSimpleRing; given that, it is the tensor decomposition read through
TauCeti.Algebra.deg_tensorProduct.