The Brauer group of a universe lift #
For a field K : Type u, the lift ULift.{w} K is a field in the larger universe max u w, and
its Brauer group is formed from central simple algebras in that larger universe. This file
identifies it with the Brauer group of K:
TauCeti.BrauerGroup.uliftEquiv K : BrauerGroup K ≃* BrauerGroup (ULift.{w} K).
The map is scalar extension A ↦ ULift K ⊗[K] A along the field isomorphism K → ULift K
(TauCeti.BrauerGroup.uliftEquiv_mk). The same-universe homomorphism
TauCeti.BrauerGroup.baseChange cannot be used, because it binds both fields to one universe so
that the base field can serve as the identity class; here the tensor product lands in the universe
of ULift K, which is where its Brauer group lives.
Injectivity is the splitting criterion: an algebra split by ULift K is a matrix algebra over
ULift K, hence over K. Surjectivity needs a model of a central simple ULift K-algebra B in
the smaller universe: B regarded as a K-algebra is finite-dimensional over K, hence small,
and its shrinking Shrink.{u} B is a central simple K-algebra whose scalar extension is B
again.
The universe lift is an actual field in a larger universe, not a field postulated to be
equivalent to one in a smaller universe, so no smallness hypothesis on K is involved.
References #
- P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, §2.4.
The Brauer group of a universe lift: scalar extension along the field isomorphism
K → ULift K identifies the Brauer group of K : Type u with the Brauer group of
ULift.{w} K, formed from central simple algebras in the universe max u w.
Instances For
TauCeti.BrauerGroup.uliftEquiv sends the class of A to the class of its scalar extension
ULift K ⊗[K] A.