Base change is a homomorphism of Brauer groups #
Let L / K be an extension of fields. Scalar extension sends a finite-dimensional central simple
K-algebra A to the finite-dimensional central simple L-algebra L ⊗[K] A
(TauCeti/Algebra/CentralSimple/BaseChange.lean), and this file shows that the assignment descends
to a group homomorphism
TauCeti.BrauerGroup.baseChange K L : BrauerGroup K →* BrauerGroup L.
Three things have to be checked, and each is an isomorphism of algebras that is already on record.
Well-definedness on classes is TauCeti.Algebra.matrixCoeffBaseChangeAlgEquiv, base change
commuting with forming a matrix algebra: it turns a witness Mₙ(A) ≃ₐ[K] Mₘ(B) of a Brauer
equivalence into a witness Mₙ(L ⊗[K] A) ≃ₐ[L] Mₘ(L ⊗[K] B) in the same two sizes.
Multiplicativity is TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv, distributivity of
scalar extension over ⊗. That the identity goes to the identity is
Algebra.TensorProduct.rid, L ⊗[K] K ≃ₐ[L] L.
Two compatibilities come with it, and both are equalities of homomorphisms rather than merely
isomorphisms: base change along K = K is the identity homomorphism
(TauCeti.BrauerGroup.baseChange_self), and base change composes along a tower K → L → M
(TauCeti.BrauerGroup.baseChange_comp), the latter by
TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv. They are the identity and composition laws
for scalar extension along the Algebra instances in scope; no bundled functor on a category of
fields, and no homomorphism induced by an arbitrary map of fields, is constructed here.
The kernel #
A class dies under baseChange K L exactly when its algebras become Brauer trivial over L
(TauCeti.BrauerGroup.mk_mem_ker_baseChange_iff). The Wedderburn-uniqueness consequence
TauCeti.isBrauerTrivial_iff_isSplittingField upgrades this to the promised description: a class
lies in the kernel exactly when L splits any algebra representing it, meaning that
L ⊗[K] A is a full matrix algebra over L. This is
TauCeti.BrauerGroup.mk_mem_ker_baseChange_iff_isSplittingField.
What is available unconditionally is the extreme case: over an algebraically closed L the whole
of BrauerGroup L is trivial, so baseChange K L is the trivial homomorphism
(TauCeti.BrauerGroup.baseChange_eq_one_of_isAlgClosed) and every class of BrauerGroup K is
killed by some extension.
References #
This is the Base change preserves central simplicity, then is a homomorphism bullet of Layer 6
of the
semisimple algebras roadmap,
whose first half is TauCeti/Algebra/CentralSimple/BaseChange.lean.
See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §2.2 and
§2.4, and R. S. Pierce, Associative Algebras, Springer GTM 88 (1982), Chapter 12.
The scalar extension of a central simple algebra #
The scalar extension of a central simple algebra, bundled as a term of CSA L.
That L ⊗[K] A really is a finite-dimensional central simple L-algebra is
TauCeti/Algebra/CentralSimple/BaseChange.lean: centrality is
TauCeti.Algebra.IsCentral.baseChange and simplicity is
TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right with L as the simple factor, both
instances, so there is no glue here.
The three universes are independent: the base field, the algebra and the extension field are
unrelated, and the scalar extension lands in Type (max w v) because that is where L ⊗[K] A
lives. It is TauCeti.BrauerGroup.baseChange that has to pin them together, because the identity
of BrauerGroup K is the class of K itself.
Equations
- TauCeti.CSA.baseChange L A = TauCeti.CSA.of L (TensorProduct K L ↑A.toAlgCat)
Instances For
Base change respects Brauer equivalence, so it descends to a map of Brauer classes.
The witness is the one of the hypothesis, in the same two sizes: base change commutes with forming
a matrix algebra (TauCeti.Algebra.matrixCoeffBaseChangeAlgEquiv), so extending
Mₙ(A) ≃ₐ[K] Mₘ(B) to L and moving the matrices outside gives
Mₙ(L ⊗[K] A) ≃ₐ[L] Mₘ(L ⊗[K] B).
The homomorphism #
Base change of Brauer classes: the group homomorphism
BrauerGroup K →* BrauerGroup L induced by A ↦ L ⊗[K] A.
It is well defined by TauCeti.isBrauerEquivalent_baseChange_congr, multiplicative by
TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv, and unital by
Algebra.TensorProduct.rid.
The Quotient.liftOn is an implementation detail, kept unexposed: the interface is
TauCeti.BrauerGroup.baseChange_mk, and every statement below is phrased and proved through
that.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class of the scalar extension is the base change of the class: the defining property of
TauCeti.BrauerGroup.baseChange, and the only place the Quotient.liftOn above is unfolded.
Everything below is stated and proved through this lemma, so downstream code is coupled to it
rather than to the quotient implementation.
Functoriality #
Base change along the identity is the identity: K ⊗[K] A ≃ₐ[K] A.
Base change composes along a tower K → L → M, by
TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv: extending to L and then to M is
extending to M in one step. With TauCeti.BrauerGroup.baseChange_self this is the composition
law a functor from fields to abelian groups would need; the functor itself, with its action on an
arbitrary map of fields, is not constructed here.
The kernel #
The kernel of Brauer-group base change consists exactly of the classes split by the extension field.
The forward implication is the substantive one: membership says that the scalar extension
L ⊗[K] A is Brauer trivial, and Wedderburn uniqueness identifies Brauer triviality with being a
matrix algebra over L.
Every Brauer class dies over an algebraically closed extension, so base change to one is
the trivial homomorphism: an algebraically closed field has trivial Brauer group
(TauCeti.subsingleton_brauerGroup_of_isAlgClosed), and there is nowhere else for a class to
go.