Documentation

TauCeti.Algebra.BrauerGroup.Splitting

A Brauer-trivial algebra is split #

TauCeti/Algebra/BrauerGroup/Trivial.lean proves that an algebra split by its own base field -- one isomorphic to a full matrix algebra Mₙ(K) -- has the identity Brauer class, and leaves the converse open: nothing there rules out an algebra that becomes a matrix algebra only after passing to matrices over it. This file closes that gap, and so identifies the identity class of BrauerGroup K exactly.

The missing ingredient is the uniqueness of the size of a matrix presentation, proved in TauCeti/RingTheory/Semisimple/MatrixDivisionRing.lean. Given Mₚ(A) ≃ₐ[K] M_q(K), write A ≃ₐ[K] M_r(D) for a central division algebra D (TauCeti.IsSimpleRing.exists_algEquiv_matrix_centralDivisionRing). Then Mₚ(A) is presented as a matrix ring over a division ring in two ways, of sizes p * r over D and q over K, so TauCeti.card_eq_of_ringEquiv_matrix forces p * r = q. Comparing dimensions, p² · dim_K A = q² = p² r², so dim_K A = r², and the Wedderburn dimension count dim_K A = r² · dim_K D collapses D to K. Hence A ≃ₐ[K] M_r(K) already.

A consequence follows for division algebras: a central division algebra has the identity Brauer class only if it is the base field, since a division ring is a matrix ring only in size one (its regular module has length one). This is the base case of the statement that each Brauer class has a unique division-algebra representative, and it is the standard source of nonidentity classes, hence of the hypothesis that TauCeti.BrauerGroup.orderOf_mk_eq_two needs to sharpen TauCeti.BrauerGroup.orderOf_mk_dvd_two; the real quaternions are the worked example, in TauCeti/Algebra/BrauerGroup/Quaternion.lean.

Main results #

Implementation notes #

Only the size half of the Wedderburn uniqueness is used, in the form TauCeti.card_eq_of_ringEquiv_matrix: the division ring is pinned here by a dimension count instead, which keeps the argument inside Module.finrank and avoids having to promote the ring isomorphism D ≃+* K that TauCeti.wedderburn_data_unique also supplies to an isomorphism of K-algebras.

The general IsBrauerTrivial equivalence is the simp normal form of TauCeti.IsBrauerTrivial. The division-algebra equivalence is deliberately not a simp lemma: after importing TauCeti.Algebra.BrauerGroup.Division, simplification instead passes through TauCeti.BrauerGroup.isBrauerEquivalent_iff_nonempty_algEquiv and Mathlib's Module.nonempty_algEquiv_iff_finrank_eq_one. The two TauCeti.BrauerGroup.mk forms are likewise not simp lemmas because TauCeti.BrauerGroup.mk_eq_one_iff already normalizes their left-hand sides.

As in TauCeti/Algebra/BrauerGroup/Trivial.lean, the statements mentioning TauCeti.CSA.base K are for a CSA.{u, u} K, an algebra in the universe of its own base field, because Mathlib's IsBrauerEquivalent relates two algebras in one universe.

References #

This completes the first bullet of Layer 6 ("the API that the identity and inverse rest on") of the semisimple algebras roadmap, whose Layer 2 asks for the Wedderburn uniqueness this consumes, and it supplies the "[ℍ] has order 2" step of that roadmap's Hamilton-quaternion worked example. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §2.4, and R. S. Pierce, Associative Algebras, Springer GTM 88 (1982), Chapter 12.

A Brauer-trivial algebra is split by its own base field #

source
theorem TauCeti.Algebra.isSplittingField_self_of_isBrauerTrivial (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (h : IsBrauerTrivial (CSA.of K A)) :
IsSplittingField K A K

A Brauer-trivial algebra is split by its own base field: if Mₚ(A) ≃ₐ[K] M_q(K) for some positive p and q, then already A ≃ₐ[K] M_r(K).

This is the converse of TauCeti.isBrauerTrivial_of_isSplittingField, and it is not formal: it needs the uniqueness of the Wedderburn data.

source
@[simp]
theorem TauCeti.isBrauerTrivial_iff_isSplittingField (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 A) ↔ Algebra.IsSplittingField K A K

Brauer triviality is exactly splitting by the base field.

This is the simp normal form of TauCeti.IsBrauerTrivial for a general central simple algebra; it is at low priority so that the sharper TauCeti.isBrauerTrivial_iff_finrank_eq_one wins on a division algebra, whose IsBrauerTrivial hypothesis matches both.

source
theorem TauCeti.BrauerGroup.mk_eq_one_iff_isSplittingField (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] :
mk (CSA.of K A) = 1 ↔ Algebra.IsSplittingField K A K

A Brauer class is the identity exactly when its algebras are split by the base field. This is the sharp form of TauCeti.BrauerGroup.mk_eq_one_of_isSplittingField.

Not a simp lemma: TauCeti.BrauerGroup.mk_eq_one_iff is one already, so simp reaches the right-hand side through it.

One-dimensional algebras #

source
theorem TauCeti.BrauerGroup.mk_eq_one_of_finrank_eq_one {K : Type u} [Field K] (A : CSA K) (h : Module.finrank K ↑A.toAlgCat = 1) :
mk A = 1

A one-dimensional central simple algebra has identity Brauer class: the structure map identifies it with the base field.

The Brauer class of a central division algebra #

source
theorem TauCeti.isBrauerTrivial_iff_finrank_eq_one (K : Type u) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] :
IsBrauerTrivial (CSA.of K D) ↔ Module.finrank K D = 1

A central division algebra is Brauer trivial exactly when it is the base field.

This is the base case of the statement that every Brauer class has a unique division-algebra representative, and it is what makes a Brauer group nontrivial in practice: exhibiting a central division algebra of dimension greater than one exhibits a nonidentity class.

Not a simp lemma: TauCeti.BrauerGroup.isBrauerEquivalent_iff_nonempty_algEquiv already rewrites the left-hand side, and Module.nonempty_algEquiv_iff_finrank_eq_one is the dimension criterion for what it leaves.

source
noncomputable def TauCeti.baseFieldAlgEquivOfIsBrauerTrivial (K : Type u) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] (h : IsBrauerTrivial (CSA.of K D)) :
D ≃ₐ[K] K

A Brauer-trivial central division algebra is the base field, as an isomorphism of K-algebras. This is the division-algebra companion of TauCeti.baseFieldAlgEquivOfFinite, with the finiteness hypothesis there replaced by triviality of the Brauer class.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.baseFieldAlgEquivOfIsBrauerTrivial_symm_apply (K : Type u) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] (h : IsBrauerTrivial (CSA.of K D)) (a : K) :
    (baseFieldAlgEquivOfIsBrauerTrivial K D h).symm a = (algebraMap K D) a

    The inverse of TauCeti.baseFieldAlgEquivOfIsBrauerTrivial is the structure map.

    source
    @[simp]
    theorem TauCeti.algebraMap_baseFieldAlgEquivOfIsBrauerTrivial (K : Type u) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] (h : IsBrauerTrivial (CSA.of K D)) (x : D) :
    (algebraMap K D) ((baseFieldAlgEquivOfIsBrauerTrivial K D h) x) = x

    TauCeti.baseFieldAlgEquivOfIsBrauerTrivial is a section of the structure map.

    source
    theorem TauCeti.BrauerGroup.mk_eq_one_iff_finrank_eq_one (K : Type u) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] :
    mk (CSA.of K D) = 1 ↔ Module.finrank K D = 1

    The Brauer class of a central division algebra is the identity exactly when the algebra is one-dimensional.

    Not a simp lemma, for the same reason as TauCeti.BrauerGroup.mk_eq_one_iff_isSplittingField.