Base change preserves central simplicity

Let A be a central simple algebra over a field K and let L / K be a field extension. This file assembles the statement that the scalar extension L ⊗[K] A is central simple over L, and adds the degree bookkeeping that goes with it.

Both halves are already available. Simplicity is a statement about L ⊗[K] A as a ring, so TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right applies with L the simple factor and A the central simple one; centrality over L is TauCeti.Algebra.IsCentral.baseChange, in TauCeti/Algebra/Central/BaseChange.lean. Both are instances, so instance search sees L ⊗[K] A as a central simple L-algebra with no glue at all.

Main results

• TauCeti.Algebra.deg_baseChange: base change preserves the degree, deg L (L ⊗[K] A) = deg K A.
• TauCeti.IsSimpleRing.of_baseChange: base change detects simplicity: if L ⊗[K] A is a simple ring for some faithfully flat K-algebra L (for instance any nontrivial L when K is a field), then A is a simple ring.
• TauCeti.isSimpleRing_baseChange_iff: for a central K-algebra A over a field K and a simple K-algebra L, simplicity passes both ways along the scalar extension, IsSimpleRing (L ⊗[K] A) ↔ IsSimpleRing A. With TauCeti.Algebra.isCentral_baseChange_iff this makes central simplicity of A over K equivalent to central simplicity of L ⊗[K] A over a field extension L.

Together with the centrality of TauCeti/Algebra/Central/BaseChange.lean and the two compatibility equivalences of TauCeti/Algebra/TensorProduct/BaseChange.lean, both re-exported here, this is what will let base change descend to a homomorphism of Brauer groups: the centrality and the simplicity say the class of L ⊗[K] A is defined, and the two equivalences say the assignment respects the multiplication and the inversion of classes.

Implementation notes

TauCeti.Algebra.deg_baseChange is read off Module.finrank_baseChange through the transport lemma TauCeti.Algebra.deg_eq_of_finrank_eq, so it never unfolds TauCeti.Algebra.deg. It asks nothing of A beyond being a K-algebra: both degrees are the integer square root of the same dimension, so the equality does not depend on that dimension being a square, and central simplicity is what makes it one rather than what makes the two agree.

The worked examples at the end check both directions on the two standard test cases: ℂ ⊗[ℝ] ℍ[ℝ] is central simple over ℂ of degree 2, while ℂ ⊗[ℝ] ℂ is not central over ℂ, because ℂ is not central over ℝ. The second is the failure TauCeti.Algebra.IsCentral.of_baseChange detects, and it is the reason the centrality hypothesis on A cannot be dropped from the forward direction.

References

This completes, apart from the homomorphism itself, the Base change preserves central simplicity, then is a homomorphism bullet of Layer 6 of the semisimple algebras roadmap. The induced homomorphism of Brauer groups waits on the group structure of BrauerGroup K, a separate bullet of the same layer. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 12.

The degree of a scalar extension

@[simp]

theorem TauCeti.Algebra.deg_baseChange (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (A : Type u_3) [Ring A] [Algebra K A] : deg L (TensorProduct K L A) = deg K A

Base change preserves the degree: the scalar extension L ⊗[K] A has the same dimension over L that A has over K, and the degree is the integer square root of the dimension.

No hypothesis on A is needed. For a finite-dimensional central simple A the common dimension is a square and both sides are the honest degree (TauCeti.Algebra.deg_sq); in general the two sides are equal because they are Nat.sqrt of the same number.

Base change detects simplicity

theorem TauCeti.IsSimpleRing.of_baseChange {K : Type u_1} [CommRing K] {L : Type u_2} [Ring L] [Algebra K L] [Module.FaithfullyFlat K L] {A : Type u_3} [Ring A] [Algebra K A] [IsSimpleRing (TensorProduct K L A)] : IsSimpleRing A

Base change detects simplicity. If the scalar extension L ⊗[K] A of a K-algebra A along a faithfully flat K-algebra L is a simple ring, then A is a simple ring. Neither L nor A needs to be commutative. When K is a field every nontrivial L is faithfully flat, so the hypothesis is automatic there.

This is the converse of TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right, with no centrality hypothesis at all. Together with TauCeti.Algebra.IsCentral.of_baseChange it says that central simplicity over K is detected by central simplicity of L ⊗[K] A over L.

Simplicity passes both ways

@[simp]

theorem TauCeti.isSimpleRing_baseChange_iff (K : Type u_1) (L : Type u_2) (A : Type u_3) [Field K] [Ring L] [IsSimpleRing L] [Algebra K L] [Ring A] [Algebra K A] [Algebra.IsCentral K A] : IsSimpleRing (TensorProduct K L A) ↔ IsSimpleRing A

Simplicity passes both ways along a scalar extension. Over a field K, a central K-algebra A is simple exactly when its scalar extension along a simple K-algebra L (for instance a field extension) is simple. The forward direction is the instance TauCeti.IsSimpleRing.tensorProduct_of_isCentral_right and the converse is TauCeti.IsSimpleRing.of_baseChange; this is the companion of TauCeti.Algebra.isCentral_baseChange_iff.

Worked examples