Subfields of a central simple algebra, and the ones that split it #
Let A be a finite-dimensional central simple algebra over a field K. A subfield of A is a
field L together with a K-algebra homomorphism f : L →ₐ[K] A; no injectivity hypothesis is
needed, because a ring homomorphism out of a field into a nontrivial ring is automatically
injective (RingHom.injective), so f really does exhibit L as a subfield of A.
This file proves the two facts about such an L that Layer 6 of the semisimple-algebra roadmap
asks for:
- its degree is bounded by the degree of the algebra,
Module.finrank K L ≤ TauCeti.Algebra.deg K A; - when that bound is attained,
LsplitsA:L ⊗[K] A ≃ₐ[L] M_{deg K A}(L).
Together these say that a subfield of degree deg K A is a maximal subfield -- nothing bigger
fits -- and that a maximal subfield of that degree is a splitting field. This is the classical
route to a splitting field that stays inside the algebra, in contrast with the algebraically
closed extension of TauCeti/Algebra/CentralSimple/Splitting.lean, which leaves it.
The module that does the work #
Both statements come from one construction. A subfield f : L →ₐ[K] A makes A into an
A-L-bimodule: A acts on the left by multiplication and L on the right through f. Because
L is commutative this right action is packaged as a left action of the scalar extension
L ⊗[K] A itself -- no opposite algebra is needed on the L side -- and the resulting module is
TauCeti.BaseChangeModule f, with l ⊗ₜ a acting by x ↦ a * x * f l.
Restricting that action along L → L ⊗[K] A makes BaseChangeModule f an L-vector space, of
dimension Module.finrank K A / Module.finrank K L by the tower law, and the action becomes an
L-algebra homomorphism
TauCeti.BaseChangeModule.toEndL f : L ⊗[K] A →ₐ[L] Module.End L (BaseChangeModule f).
It is injective, because L ⊗[K] A is a simple ring (base change of a central simple algebra)
and a nontrivial module over a simple ring is faithful
(TauCeti.faithfulSMul_of_isSimpleRing). Everything else is dimension counting: writing
n = deg K A, d = Module.finrank K L and m = Module.finrank L (BaseChangeModule f), injectivity
gives n ^ 2 ≤ m ^ 2 and the tower law gives d * m = n ^ 2, whence d ≤ n; and when d = n the
two dimensions agree, so the injection is onto and L ⊗[K] A is the endomorphism algebra
Module.End L (BaseChangeModule f), a matrix algebra of size m = n.
Main results #
TauCeti.BaseChangeModule:Aas a module over the scalar extensionL ⊗[K] A, with the actionTauCeti.BaseChangeModule.toEndand itsL-algebra formTauCeti.BaseChangeModule.toEndL.TauCeti.BaseChangeModule.toEndL_injective: the action is faithful.TauCeti.Algebra.finrank_le_deg: a subfield of a central simple algebra has degree at most the degree of the algebra.TauCeti.BaseChangeModule.algEquivEndandTauCeti.Algebra.isSplittingField_of_finrank_eq_deg: a subfield of degreedeg K AsplitsA, through the identificationL ⊗[K] A ≃ₐ[L] Module.End L (BaseChangeModule f).TauCeti.Algebra.bijective_of_finrank_eq_deg: a subfield of degreedeg K Ais maximal: any subfield ofAreceiving it does so by an isomorphism.
Implementation notes #
TauCeti.BaseChangeModule f reuses TauCeti.Bimodule from
TauCeti/Algebra/CentralSimple/Bimodule.lean with codomain Aᵐᵒᵖ and the opposite of f. Its
scalar action is transported along A ≃ₐ[K] Aᵐᵒᵖᵐᵒᵖ, giving the required orientation over
L ⊗[K] A:
l ⊗ₜ a acts by x ↦ a * x * f l. This orientation makes the conclusion land on the tensor
product occurring in TauCeti.Algebra.IsSplittingField, rather than on its opposite.
The L-module structure on TauCeti.BaseChangeModule f is defined by restricting scalars along
algebraMap L (L ⊗[K] A) rather than as a separate right-multiplication action, which is what
makes TauCeti.BaseChangeModule.toEndL available as Algebra.lsmul and the scalar towers
formal. The K-structure is the one A already has, so TauCeti.BaseChangeModule.of is the
identity linear equivalence and dimensions over K transfer by rfl-like transport.
Nothing here needs A to be a division algebra: the classical statement is about a maximal
subfield of a central division algebra, but the argument only uses simplicity of L ⊗[K] A, so
it is stated for every finite-dimensional central simple A. What a division algebra adds is the
existence of a subfield attaining the bound, which is a separate question, settled by
TauCeti.Algebra.exists_subalgebra_isField_finrank_eq_deg in
TauCeti/Algebra/CentralSimple/MaximalSubfield.lean.
References #
This is the maximal-subfield half of the fourth bullet of Layer 6 ("Splitting fields, maximal subfields, and the index") of the semisimple algebras roadmap. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 13.
The algebra as a module over its scalar extension #
A regarded as a module over the scalar extension L ⊗[K] A, along a K-algebra homomorphism
f : L →ₐ[K] A out of a commutative algebra: the pure tensor l ⊗ₜ a acts by
x ↦ a * x * f l.
Equivalently this is the A-L-bimodule A, with A acting on the left by multiplication and
L on the right through f; commutativity of L is what lets the right action be packaged as a
left action of L ⊗[K] A with no opposite algebra. It is a type synonym for A so that A itself
is left without an L ⊗[K] A-action, and so that different subfields can act at the same time.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- TauCeti.BaseChangeModule.instModule f = { toSMul := TauCeti.BaseChangeModule.instModule._aux_1 f, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
BaseChangeModule f is A again as a K-module: only the L ⊗[K] A-action is new.
Equations
Instances For
Equations
The action of L ⊗[K] A on A defining BaseChangeModule f, as a K-algebra homomorphism
into Module.End K A, transported from TauCeti.Bimodule.toEnd.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A pure tensor l ⊗ₜ a acts on x : A through toEnd f by x ↦ a * x * f l.
A scalar r : L ⊗[K] A acts on BaseChangeModule f through toEnd f. This is the defining
equation of the module structure, and the single place it is unfolded: everything else rewrites
with it instead of reasoning up to definitional equality.
A pure tensor l ⊗ₜ a acts on BaseChangeModule f by x ↦ a * x * f l.
Equations
L acts on BaseChangeModule f through its image in L ⊗[K] A. This is the defining equation
of the L-module structure; TauCeti.BaseChangeModule.lsmul_of reads it off concretely.
Concretely, L acts on BaseChangeModule f by right multiplication through f. This is
the right action the type synonym exists to carry, and the reason the pairing with the left action
of A needs L to be commutative.
Over the base field nothing has changed: BaseChangeModule f has the dimension of A.
The action of the scalar extension is faithful #
The action of the scalar extension on BaseChangeModule f is faithful.
If L has degree deg K A, then BaseChangeModule f has dimension deg K A over L.
The scalar extension by a subfield of degree deg K A is isomorphic to the algebra of
L-linear endomorphisms of BaseChangeModule f.
Equations
Instances For
The equivalence algEquivEnd f h sends a scalar-extension element to its action on
BaseChangeModule f.
Subfields, their degrees, and the splitting theorem #
A subfield of a central simple algebra has degree at most the degree of the algebra.
A subfield of degree deg K A is a splitting field of A.
If subfields L and L' of A satisfy Module.finrank K L = deg K A, then every
K-algebra homomorphism L →ₐ[K] L' is bijective.