Documentation

TauCeti.Algebra.BrauerGroup.Trivial

Brauer triviality #

Two finite-dimensional central simple K-algebras are Brauer equivalent when they become isomorphic after passing to matrix algebras over them (Mathlib's IsBrauerEquivalent), and BrauerGroup K is the quotient of CSA K by that relation. Mathlib stops there: the quotient carries no group structure yet, and TauCeti/Algebra/BrauerGroup/Basic.lean supplies the constructors and the two moves that leave a Brauer class unchanged. This file builds the part of the theory the identity element of that group will rest on -- which algebras are Brauer trivial, that is, equivalent to K itself -- and reads off the first two computations of a Brauer group.

The engine is a single observation. An algebra split by K, in the sense of TauCeti.Algebra.IsSplittingField, is a matrix algebra Mₚ(K), and any two matrix algebras over K become isomorphic after one more round of matrices: Mᵩ(Mₚ(K)) and Mₚ(Mᵩ(K)) are both the matrix algebra over K indexed by a product of Fin p and Fin q, in the two orders, and transposing the two factors matches them up. So the algebras split by K form a single Brauer class, and each of the three named Brauer-trivial algebras is trivial because it is already known to be a matrix algebra over K: a full matrix algebra Mₙ(K) by definition, the endomorphism algebra End_K V of a nonzero finite-dimensional vector space by a choice of basis (TauCeti.Algebra.endAlgEquivMatrix), and A ⊗[K] Aᵐᵒᵖ for a finite-dimensional central simple A by the Azumaya isomorphism (TauCeti.Algebra.tensorOpAlgEquivMatrix).

The last of these is why the Brauer group will have inverses: it says the class of Aᵐᵒᵖ is inverse to the class of A, once the multiplication induced by ⊗[K] is known to descend to classes.

Main definitions #

Main results #

Implementation notes #

TauCeti.IsBrauerTrivial compares an algebra with TauCeti.CSA.base K, so it is stated for a CSA.{u, u} K, an algebra in the universe of its own base field. That is not a restriction on the mathematics -- a finite-dimensional K-algebra has a model in Type u -- but Mathlib's IsBrauerEquivalent relates two algebras in one universe, and K lives in Type u. The statements that do not mention K itself as an algebra, including the two Brauer-group computations, stay at the full generality of BrauerGroup.{u, v}.

The two splitting facts TauCeti.Algebra.isSplittingField_end and TauCeti.Algebra.isSplittingField_tensorOp are proved here rather than with the rest of the splitting API, because they consume the simplicity of an endomorphism algebra and the Azumaya isomorphism, which sit above TauCeti/Algebra/CentralSimple/Splitting.lean in the import order.

The converse of TauCeti.isBrauerTrivial_of_isSplittingField -- that a Brauer-trivial algebra is split -- is not proved here, and is not a formal consequence of these lemmas: it needs the uniqueness of the Wedderburn data, which sits above this file in the import order. It is TauCeti.Algebra.isSplittingField_self_of_isBrauerTrivial, in TauCeti/Algebra/BrauerGroup/Splitting.lean. Nothing below uses it, and in particular the two Brauer-group computations go through the splitting side only.

References #

This implements the Brauer-triviality prerequisites of the first bullet of Layer 6 ("the API that the identity and inverse rest on: finite-dimensional Module.End K V is Brauer-equivalent to K; Matrix n n K is Brauer-trivial") together with the "Finite base fields" bullet ("BrauerGroup of a finite field is trivial") of the semisimple algebras roadmap. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.4, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 12.

source
@[reducible, inline]
abbrev TauCeti.IsBrauerTrivial {K : Type u} [Field K] (A : CSA K) :
Prop

A finite-dimensional central simple K-algebra is Brauer trivial when it is Brauer equivalent to the base field, that is, when its Brauer class is the one that will be the identity of BrauerGroup K.

Every algebra split by K is Brauer trivial (TauCeti.isBrauerTrivial_of_isSplittingField); the converse needs the uniqueness of the Wedderburn data and is TauCeti.Algebra.isSplittingField_self_of_isBrauerTrivial, proved in TauCeti/Algebra/BrauerGroup/Splitting.lean.

Equations
Instances For

    The algebras split by the base field form one Brauer class #

    source
    theorem TauCeti.ne_zero_of_algEquiv_matrix (K : Type u) [Field K] {A : Type v} [Ring A] [Algebra K A] [Nontrivial A] {p : ℕ} (e : A ≃ₐ[K] Matrix (Fin p) (Fin p) K) :
    p ≠ 0

    The size of a matrix presentation of a nontrivial algebra is nonzero, because a 0 × 0 matrix algebra is the zero ring.

    source
    theorem TauCeti.isBrauerEquivalent_of_isSplittingField (K : Type u) [Field K] {A B : CSA K} (hA : Algebra.IsSplittingField K (↑A.toAlgCat) K) (hB : Algebra.IsSplittingField K (↑B.toAlgCat) K) :
    IsBrauerEquivalent A B

    Two central simple algebras split by their own base field are Brauer equivalent.

    Writing A ≃ₐ Mₚ(K) and B ≃ₐ Mᵩ(K), both Mᵩ(A) and Mₚ(B) are the matrix algebra over K indexed by a product of Fin p and Fin q, in the two orders, and transposing the two factors matches them up.

    The Brauer-trivial algebras #

    source
    theorem TauCeti.isBrauerTrivial_matrix (K : Type u) [Field K] (n : ℕ) [NeZero n] :
    IsBrauerTrivial (CSA.of K (Matrix (Fin n) (Fin n) K))

    A full matrix algebra over K is Brauer trivial. It is Mₙ of the base field, so this is the matrix move TauCeti.isBrauerEquivalent_matrix applied to the class of K itself.

    source
    theorem TauCeti.isBrauerTrivial_of_isSplittingField (K : Type u) [Field K] {A : Type u} [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (hA : Algebra.IsSplittingField K A K) :
    IsBrauerTrivial (CSA.of K A)

    An algebra split by its own base field is Brauer trivial: it is isomorphic to a full matrix algebra over K, so the two class-preserving moves compose to a Brauer equivalence with K.

    Over an algebra in the universe of K this is the statement wanted downstream; the version for two algebras in an arbitrary universe, which cannot pass through TauCeti.CSA.base K because K lives in Type u, is TauCeti.isBrauerEquivalent_of_isSplittingField.

    source
    theorem TauCeti.Algebra.isSplittingField_end (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [FiniteDimensional K V] :
    IsSplittingField K (Module.End K V) K

    End_K V is split by K: a choice of basis of V presents it as the matrix algebra of size Module.finrank K V.

    source
    theorem TauCeti.isBrauerTrivial_end (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Nontrivial V] :
    IsBrauerTrivial (CSA.of K (Module.End K V))

    The endomorphism algebra of a nonzero finite-dimensional vector space is Brauer trivial.

    This is the form in which triviality gets used downstream: the identity Brauer class is not only the class of the abstract matrix algebras but the class of every End_K V, and End_K A is what A ⊗[K] Aᵐᵒᵖ is isomorphic to.

    source
    theorem TauCeti.Algebra.isSplittingField_tensorOp (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] :
    IsSplittingField K (TensorProduct K A Aᵐᵒᵖ) K

    A ⊗[K] Aᵐᵒᵖ is split by K: it is the matrix algebra of size Module.finrank K A, by the Azumaya isomorphism TauCeti.Algebra.tensorOpAlgEquivMatrix.

    source
    theorem TauCeti.isBrauerTrivial_tensorOp (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] :
    IsBrauerTrivial (CSA.of K (TensorProduct K A Aᵐᵒᵖ))

    A ⊗[K] Aᵐᵒᵖ is Brauer trivial.

    This is what will make the class of Aᵐᵒᵖ inverse to the class of A: once the tensor product is known to descend to a multiplication of Brauer classes, this says the product of those two classes is the identity.

    Fields with trivial Brauer group #

    source
    theorem TauCeti.subsingleton_brauerGroup_of_forall_isSplittingField (K : Type u) [Field K] (h : ∀ (A : CSA K), Algebra.IsSplittingField K (↑A.toAlgCat) K) :
    Subsingleton (BrauerGroup K)

    A field that splits every central simple algebra over it has trivial Brauer group.

    Any two such algebras are Brauer equivalent by TauCeti.isBrauerEquivalent_of_isSplittingField, so there is only one Brauer class. This is the common content of the two triviality criteria below; each supplies the splitting hypothesis from a different property of K.

    source
    theorem TauCeti.subsingleton_brauerGroup_of_isAlgClosed (K : Type u) [Field K] [IsAlgClosed K] :
    Subsingleton (BrauerGroup K)

    The Brauer group of an algebraically closed field is trivial. Every finite-dimensional central simple algebra over an algebraically closed field is a matrix algebra over it (TauCeti.Algebra.isSplittingField_of_isSepClosed, with the extension taken to be the base field itself), so there is only one Brauer class.

    source
    theorem TauCeti.subsingleton_brauerGroup_of_finite (K : Type u) [Field K] [Finite K] :
    Subsingleton (BrauerGroup K)

    The Brauer group of a finite field is trivial. A finite division ring is a field (little Wedderburn), so the Wedderburn presentation of a central simple algebra over a finite field is already a matrix algebra over that field (TauCeti.Algebra.isSplittingField_self_of_finite); again there is only one Brauer class.

    Worked example #