The opposite isomorphism A ⊗[K] Aᵐᵒᵖ ≃ₐ[K] Mₙ(K) #
Let A be a finite-dimensional central simple algebra over a field K, of dimension n over K.
This file proves that the Azumaya map
AlgHom.mulLeftRight K A : A ⊗[K] Aᵐᵒᵖ →ₐ[K] Module.End K A, a ⊗ₜ b ↦ (x ↦ a * x * b.unop),
is an isomorphism, and combines it with a choice of K-basis of A to write
A ⊗[K] Aᵐᵒᵖ ≃ₐ[K] Matrix (Fin n) (Fin n) K.
This is the fact that makes the class of Aᵐᵒᵖ the inverse of the class of A in the Brauer group:
the tensor product of A with its opposite is a full matrix algebra, hence Brauer-trivial.
The matrix size is n = Module.finrank K A, not the degree: for a central simple algebra of
degree d one has Module.finrank K A = d ^ 2, so this is Matrix (Fin (d ^ 2)) (Fin (d ^ 2)) K.
The dimension and degree counts this rests on are general facts about A ⊗[K] Aᵐᵒᵖ and live with
the rest of the degree API, as TauCeti.Algebra.finrank_tensorProduct_mulOpposite and
TauCeti.Algebra.deg_tensorProduct_mulOpposite.
The proof #
Both halves of bijectivity are cheap once the right facts are in place, and neither is a computation with the map.
Injectivity is simplicity: Aᵐᵒᵖ is simple because A is, so A ⊗[K] Aᵐᵒᵖ is simple by
TauCeti.IsSimpleRing.tensorProduct (this is where centrality of A enters), and a ring
homomorphism out of a simple ring into a nontrivial ring is injective (RingHom.injective).
No finite-dimensionality is used here, and the half is stated on its own as
TauCeti.IsSimpleRing.mulLeftRight_injective.
Surjectivity is a dimension count: A ⊗[K] Aᵐᵒᵖ and Module.End K A both have dimension n ^ 2
over K, so an injective K-linear map between them is surjective. This is the only place
finite-dimensionality is needed, and it is essential: for an infinite-dimensional central simple
algebra the Azumaya map is injective but need not be surjective.
Centrality enters only through the first half, and it cannot be dropped there. Take A = ℂ over
K = ℝ, which is simple and finite-dimensional but not central. Then ℂ ⊗[ℝ] ℂᵐᵒᵖ is not simple:
multiplication a ⊗ₜ b ↦ a * b is an ℝ-algebra map onto ℂ whose kernel contains the nonzero
element Complex.I ⊗ₜ 1 - 1 ⊗ₜ Complex.I. Injectivity genuinely fails, and so does the conclusion:
because ℂ is commutative the Azumaya map has image the scalar multiplications, a 2-dimensional
subalgebra of the 4-dimensional Module.End ℝ ℂ.
Main results #
TauCeti.IsSimpleRing.mulLeftRight_injective: the Azumaya map of a central simple algebra is injective, with no finiteness hypothesis, andTauCeti.IsSimpleRing.mulLeftRight_bijective: for a finite-dimensional one it is bijective, with its packagingTauCeti.IsSimpleRing.isAzumaya: such an algebra is an Azumaya algebra over its base field.TauCeti.Algebra.tensorOpAlgEquivEnd: the resulting isomorphismA ⊗[K] Aᵐᵒᵖ ≃ₐ[K] Module.End K A.TauCeti.Algebra.tensorOpAlgEquivMatrix: the opposite isomorphismA ⊗[K] Aᵐᵒᵖ ≃ₐ[K] Matrix (Fin n) (Fin n) Kfor anynwithModule.finrank K A = n.
The last two are stated for [IsAzumaya K A], which is all their construction uses: bijectivity of
the Azumaya map is the field IsAzumaya.bij, and the finiteness the matrix half needs is the
Module.Finite K A that IsAzumaya extends. Over a field this is not a wider class -- an Azumaya
K-algebra is exactly a finite-dimensional central simple one -- but it is the hypothesis the
construction actually reads, and the one already carried by an algebra known to be Azumaya for some
other reason (Mathlib's IsAzumaya.matrix, IsAzumaya.of_AlgEquiv). For a central simple A the
way in is TauCeti.IsSimpleRing.isAzumaya, installed with haveI.
TauCeti.Algebra.tensorOpAlgEquivEnd uses nothing else, so it is stated over the commutative
semiring K and semiring A that IsAzumaya itself is defined over. Only the matrix half needs a
field, to read the isomorphism off a basis.
The real quaternions run all of this concretely in
TauCeti/Algebra/CentralSimple/Quaternion.lean.
Implementation notes #
TauCeti.IsSimpleRing.isAzumaya is deliberately not an instance. Mathlib's
Algebra.IsCentral.instIsAzumaya goes the other way, deducing Algebra.IsCentral K A from
IsAzumaya K A; registering the converse as an instance would let typeclass search cycle between
the two. Apply it with haveI where an IsAzumaya hypothesis is wanted, as the worked example at
the end of this file does:
haveI := TauCeti.IsSimpleRing.isAzumaya K A
TauCeti.Algebra.tensorOpAlgEquivMatrix K A hn
TauCeti.Algebra.tensorOpAlgEquivMatrix takes the matrix size as a parameter n together with a
proof Module.finrank K A = n, rather than using Module.finrank K A itself. Instantiating n at
Module.finrank K A and hn at rfl recovers the unparametrized form, while the parametrized one
is what makes the quaternion example (where the dimension is 4 on the nose) come out without
reindexing. Its second half is TauCeti.Algebra.endAlgEquivMatrix, which involves neither an
algebra structure nor central simplicity and so lives with the linear algebra, in
TauCeti/LinearAlgebra/Matrix/ToLin.lean; nothing downstream should depend on which basis it
chooses.
References #
This implements the fourth bullet of Layer 4 ("The opposite isomorphism") of the semisimple algebras roadmap, which also lists it among the Brauer-triviality prerequisites of Layer 6. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.4, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 12.
The Azumaya map is bijective #
The Azumaya map of a central simple algebra is injective: A ⊗[K] Aᵐᵒᵖ is a simple ring
(TauCeti.IsSimpleRing.tensorProduct, which is where centrality of A enters), and a ring
homomorphism out of a simple ring into a nontrivial ring is injective.
No finite-dimensionality is used, and none should be added: this half of
TauCeti.IsSimpleRing.mulLeftRight_bijective holds for an infinite-dimensional central simple
algebra too, where the Azumaya map is injective but need not be surjective.
The Azumaya map of a finite-dimensional central simple algebra is bijective: for A central
simple and finite-dimensional over a field K, the map
AlgHom.mulLeftRight K A : A ⊗[K] Aᵐᵒᵖ →ₐ[K] Module.End K A, a ⊗ₜ b ↦ (x ↦ a * x * b.unop),
is a bijection.
Injectivity is TauCeti.IsSimpleRing.mulLeftRight_injective, which holds for any central simple
A, finite-dimensional or not. Finite-dimensionality is used only for surjectivity, where it makes
the two sides equidimensional K-vector spaces.
A finite-dimensional central simple algebra is an Azumaya algebra over its base field.
This is not an instance. Mathlib's Algebra.IsCentral.instIsAzumaya deduces Algebra.IsCentral K A
from IsAzumaya K A, so making the converse an instance would let typeclass search cycle between
the two; use haveI := TauCeti.IsSimpleRing.isAzumaya K A where an IsAzumaya hypothesis is
wanted.
The opposite isomorphism #
The Azumaya map of an Azumaya algebra, promoted to an isomorphism
A ⊗[K] Aᵐᵒᵖ ≃ₐ[K] Module.End K A. Its value on a pure tensor is
TauCeti.Algebra.tensorOpAlgEquivEnd_tmul_apply.
Bijectivity is the field IsAzumaya.bij, so this needs no hypothesis beyond IsAzumaya K A, and in
particular no field and no finiteness: it is stated over the commutative semiring K that
IsAzumaya itself is defined over. For a finite-dimensional central simple A over a field the
hypothesis is TauCeti.IsSimpleRing.isAzumaya K A, which is not an instance and has to be installed
by hand: haveI := TauCeti.IsSimpleRing.isAzumaya K A.
Equations
Instances For
The Azumaya isomorphism TauCeti.Algebra.tensorOpAlgEquivEnd sends a pure tensor a ⊗ₜ b to
the endomorphism x ↦ a * x * b.unop, since it is AlgHom.mulLeftRight underneath. Pure tensors
span A ⊗[K] Aᵐᵒᵖ, so this determines the isomorphism, and it is the only computation rule it
needs.
The opposite isomorphism. An Azumaya K-algebra A of dimension n -- over a field, a
finite-dimensional central simple algebra -- satisfies A ⊗[K] Aᵐᵒᵖ ≃ₐ[K] Matrix (Fin n) (Fin n) K:
the tensor product of a central simple algebra with its opposite is a full matrix algebra, which is
what makes the Brauer class of Aᵐᵒᵖ the inverse of that of A. The finiteness needed to read a
matrix off is the Module.Finite K A that IsAzumaya extends; for a central simple A, install
the hypothesis with haveI := TauCeti.IsSimpleRing.isAzumaya K A.
The size is the dimension n = Module.finrank K A, not the degree TauCeti.Algebra.deg K A;
the two are related by TauCeti.Algebra.deg_sq, and the resulting degree count is
TauCeti.Algebra.deg_tensorProduct_mulOpposite. The dimension is taken as a parameter so that a
caller who already knows it as a numeral, as in
TauCeti.Quaternion.tensorSelfAlgEquivMatrix, gets that numeral back with no reindexing.
This is TauCeti.Algebra.tensorOpAlgEquivEnd followed by TauCeti.Algebra.endAlgEquivMatrix, as
recorded by TauCeti.Algebra.tensorOpAlgEquivMatrix_apply.
Equations
Instances For
The opposite isomorphism is the Azumaya isomorphism TauCeti.Algebra.tensorOpAlgEquivEnd
followed by TauCeti.Algebra.endAlgEquivMatrix. This is the only handle on it: which basis
TauCeti.Algebra.endAlgEquivMatrix chooses is deliberately opaque, so there is no lemma computing
matrix entries. Together with TauCeti.Algebra.tensorOpAlgEquivEnd_tmul_apply it identifies the
image of a pure tensor as the matrix of x ↦ a * x * b.unop.