11 Brauer Groups

Chapter 11 of the Stacks Project, Brauer Groups, Tag 073W: the 7 sections of its 8 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 33 tags are carried by 45 declarations of the repository (all in StacksCore) and 19 registered declarations.

Section11.2 Noncommutative algebras#

Section 11.2 of the Stacks Project, Tag 073Y. 5 tags here are carried by 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 073Z, a definition

Tag 073Z in the Stacks Project.

Declarations registered for the tag:

  • Module.finrank registered with add_to_stacks in StacksCore/LinearAlgebra/Dimension/Finrank.lean, line 13 (StacksCore). References: EGA 0 (21.9.5); EGA 0 (22.4.1); EGA I (6.4.5); EGA II (6.4.2); SGA 1 I (7.5), “more general”; SGA 1 IV (4.4); SGA 3 XXI (1.1.6); SGA 3 XXII (5.3.1); SGA 6 0 (2.3.Corollary2), “affine clause”; SGA 6 I (6.11), “special case”.
  • Module.Finite registered with add_to_stacks in StacksCore/RingTheory/Finiteness/Defs.lean, line 13 (StacksCore). References: EGA 0 (10.3.1.2); EGA 0 (1.0.5); EGA II (6.3.1); EGA III (4.4.7); EGA III (7.4.6); EGA III (7.9.1); EGA IV (6.1.3); EGA IV (7.2.4); EGA IV (14.5.5); EGA IV (2.5.3); EGA IV (18.3.2.1); SGA 1 I (2.1); SGA 3 VIII (3.4); SGA 3 XXI (1.1.1), “partial”; SGA 4 VI (5.6), “special case”; SGA 4 XVII (5.5.6.3); SGA 4½ Rapport (4.11); SGA 5 X (3.1), “partial”; SGA 6 I (1.2), “special case”; SGA 6 I (1.3), “special case”; SGA 6 I (2.8), “special case”; SGA 6 II (2.2.10).
Tag 0740, a definition

Tag 0740 in the Stacks Project.

Declarations registered for the tag:

Tag 0741, a definition

Tag 0741 in the Stacks Project.

Declarations registered for the tag:

Tag 0742, a definition

Tag 0742 in the Stacks Project.

Declarations registered for the tag:

Tag 0743, a definition

Tag 0743 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.finrank · Module.Finite · DivisionRing · Algebra.IsCentral · IsSimpleModule · IsSimpleRing · MulOpposite

Section11.3 Wedderburn's theorem#

Section 11.3 of the Stacks Project, Tag 0744. 2 tags here are carried by 3 declarations of the repository (all in StacksCore) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0746, a lemma

Tag 0746 in the Stacks Project.

exists_simple_submod, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Artinian/Module.lean, line 27. The attribute's comment: “(2)”.

lemma exists_simple_submod (A M : Type*) [Ring A] [Nontrivial M] [AddCommGroup M]
    [Module A M] [IsArtinianRing A] : ∃ (p : Submodule A M), IsSimpleModule A p

exists_simple_submod_algebra, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Artinian/Module.lean, line 39. The attribute's comment: “(1)”.

lemma exists_simple_submod_algebra (A : Type u) [Ring A] [Nontrivial A] [IsArtinianRing A] :
    ∃ (M : Type u) (_ : AddCommGroup M) (_ : Module A M), IsSimpleModule A M

Module.finite_of_simple_tower, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Artinian/Module.lean, line 45. The attribute's comment: “(3)”.

lemma Module.finite_of_simple_tower (k A M : Type*) [CommSemiring k] [Ring A] [Algebra k A]
    [Module.Finite k A] [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M]
    [IsSimpleModule A M] : Module.Finite k M

Declarations registered for the tag:

Tag 0747, a theorem

Tag 0747 in the Stacks Project.

Declarations registered for the tag:

Sources
Leanexists_simple_submod · exists_simple_submod_algebra · Module.finite_of_simple_tower · Module.End.instDivisionRing · IsSimpleRing.exists_algEquiv_matrix_divisionRing

Section11.4 Lemmas on algebras#

Section 11.4 of the Stacks Project, Tag 0748. 10 tags here are carried by 20 declarations of the repository (all in StacksCore) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0749, a lemma

Tag 0749 in the Stacks Project.

centralizer_tensor_centralizer, a lemma in StacksCore (human-reviewed), declared in StacksCore/Algebra/Algebra/Subalgebra/Centralizer.lean, line 73.

lemma centralizer_tensor_centralizer :
    Subalgebra.centralizer F (A := A ⊗[F] A') (Algebra.TensorProduct.map B.val B'.val).range =
    (Algebra.TensorProduct.map (centralizer F B).val (centralizer F B').val).range
Tag 074A, a lemma

Tag 074A in the Stacks Project.

Declarations registered for the tag:

Tag 074B, a lemma

Tag 074B in the Stacks Project.

TwoSidedIdeal.map_comap_includeRight, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/TensorProduct.lean, line 136.

Let A be a central simple K-algebra and B any K-algebra. Then every two-sided ideal of A ⊗[K] B is generated by its intersection with 1 ⊗ B.

This is a slightly different version of the statement in the stacks project, where K (which is a central division algebra there) is generalized to a central simple algebra, and W (a two-sided sub-vector space there) is specialized to a two-sided ideal of A ⊗ B.

lemma map_comap_includeRight (I : TwoSidedIdeal (A ⊗[K] B)) :
    (I.comap (includeRight : B →ₐ[K] A ⊗[K] B)).map includeRight = I
Tag 074C, a lemma

Tag 074C in the Stacks Project.

TwoSidedIdeal.orderIsoMapIncludeRight, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/TensorProduct.lean, line 178. The attribute's comment: “part 1”.

This is a generalized version of stacks 074C part 1.

def orderIsoMapIncludeRight : TwoSidedIdeal B ≃o TwoSidedIdeal (A ⊗[K] B)

Algebra.TensorProduct.isSimpleRing, an instance in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/TensorProduct.lean, line 192. The attribute's comment: “part 2”.

The tensor product of a central simple algebra and a simple algebra is simple. This is slightly more general than the statement in the stacks project, which requires A to be a skew field rather than merely a simple ring.

instance Algebra.TensorProduct.isSimpleRing [IsSimpleRing A] [Algebra.IsCentral K A]
    [IsSimpleRing B] : IsSimpleRing (A ⊗[K] B)
Tag 074D, a lemma

Tag 074D in the Stacks Project.

Declarations registered for the tag:

Tag 074E, a lemma

Tag 074E in the Stacks Project.

Module.End.matAlgEquiv, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/End.lean, line 104. The attribute's comment: “(4) second part”.

The k-algebra isomorphism between End D D and End Mₙ(D) Dⁿ induced by the Morita equivalence between D and Mₙ(D).

noncomputable def Module.End.matAlgEquiv (n : ℕ) [NeZero n] (D : Type w)
    [DivisionRing D] [Algebra k D] :
    Module.End D D ≃ₐ[k] Module.End (Matrix (Fin n) (Fin n) D) (Fin n → D)

endSimpleModOfWedderburn, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/End.lean, line 113. The attribute's comment: “(3) first part”.

noncomputable def endSimpleModOfWedderburn (n : ℕ) [NeZero n] (D : Type w) [DivisionRing D]
    [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) :
    let _ : Module A (Fin n → D) := Module.compHom _ wdb.toRingEquiv.toRingHom
    Module.End A (Fin n → D) ≃ₐ[k] Dᵐᵒᵖ

end_simple_mod_finite, an instance in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/End.lean, line 141. The attribute's comment: “(5) part 2”.

instance end_simple_mod_finite (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M]
    [Module k M] [IsScalarTower k A M] : Module.Finite k (Module.End A M)

endEndIso, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/End.lean, line 258. The attribute's comment: “(6)”.

noncomputable def endEndIso
    (M : Type v) [AddCommGroup M]
    [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] :
    A ≃ₐ[k] Module.End (Module.End A M) M

end_end_center_equiv, a private def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/End.lean, line 266. The attribute's comment: “(5) part 3”.

private noncomputable def end_end_center_equiv (M : Type v) [AddCommGroup M]
    [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] :
    Subalgebra.center k (Module.End (Module.End A M) M) ≃ₐ[k] Subalgebra.center k A

finrank_mul_finrank_end, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/End.lean, line 293. The attribute's comment: “(5) part 4”.

theorem finrank_mul_finrank_end (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M]
    [Module k M] [IsScalarTower k A M] :
    Module.finrank k A * Module.finrank k (Module.End A M) = Module.finrank k M ^ 2

simple_mod_of_wedderburn, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/Matrix.lean, line 20. The attribute's comment: “(4) first part”.

lemma simple_mod_of_wedderburn (k A : Type*) [Field k] [Ring A] [Algebra k A] {n : ℕ} [NeZero n]
    (D : Type w) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) :
    let : Module A (Fin n → D) := Module.compHom _ wdb.toRingEquiv.toRingHom
    IsSimpleModule A (Fin n → D)

linearEquiv_of_isSimpleModule_over_simple_ring, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/SimpleRing.lean, line 37. The attribute's comment: “(1)”. References: EGA IV (2.5.8.9), “special case”.

lemma linearEquiv_of_isSimpleModule_over_simple_ring [IsArtinianRing A] (M N : Type w)
    [AddCommGroup M] [AddCommGroup N] [Module A M] [Module A N] [IsSimpleModule A M]
    [IsSimpleModule A N] : Nonempty (M ≃ₗ[A] N)

directSum_simple_module_over_simple_ring, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/SimpleRing.lean, line 53. The attribute's comment: “(2)”. References: EGA IV (2.5.8.9), “partial”.

lemma directSum_simple_module_over_simple_ring [IsArtinianRing A] (M : Type v) [AddCommGroup M]
    [Module A M] : ∃ (S : Type v) (_ : AddCommGroup S) (_ : Module A S) (_ : IsSimpleModule A S)
    (ι : Type v), Nonempty (M ≃ₗ[A] (ι →₀ S))

directSum_simple_module_over_simple_algebra, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/SimpleRing.lean, line 75. The attribute's comment: “(2)”. References: EGA IV (2.5.8.9), “partial”.

lemma directSum_simple_module_over_simple_algebra (M : Type v) [AddCommGroup M]
    [Module A M] : ∃ (S : Type v) (_ : AddCommGroup S) (_ : Module k S)
    (_ : Module A S) (_ : IsScalarTower k A S) (_ : IsSimpleModule A S) (ι : Type v),
    Nonempty (M ≃ₗ[A] (ι →₀ S))

linearEquiv_iff_finrank_eq_over_simple_ring, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Morita/SimpleRing.lean, line 104. The attribute's comment: “(3)”. References: EGA IV (2.5.8.9), “more general”.

lemma linearEquiv_iff_finrank_eq_over_simple_ring
    (M N : Type v) [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [Module k M]
    [Module k N] [IsScalarTower k A M] [IsScalarTower k A N] [Module.Finite A M]
    [Module.Finite A N] : Nonempty (M ≃ₗ[A] N) ↔ Module.finrank k M = Module.finrank k N
Tag 074F, a lemma

Tag 074F in the Stacks Project.

Algebra.TensorProduct.isSimpleRing, an instance in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/TensorProduct.lean, line 192. The attribute's comment: “the first algebra is finite and central”.

The tensor product of a central simple algebra and a simple algebra is simple. This is slightly more general than the statement in the stacks project, which requires A to be a skew field rather than merely a simple ring.

instance Algebra.TensorProduct.isSimpleRing [IsSimpleRing A] [Algebra.IsCentral K A]
    [IsSimpleRing B] : IsSimpleRing (A ⊗[K] B)

Algebra.TensorProduct.isSimpleRing', an instance in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/TensorProduct.lean, line 204. The attribute's comment: “the second algebra is finite and central”.

The tensor product of a simple algebra and a central simple algebra is simple.

instance Algebra.TensorProduct.isSimpleRing' [IsSimpleRing B] [Algebra.IsCentral K B]
    [IsSimpleRing A] : IsSimpleRing (A ⊗[K] B)
Tag 074G, a lemma

Tag 074G in the Stacks Project.

An instance with no name in StacksCore (human-reviewed), declared in StacksCore/Algebra/Central/TensorProduct.lean, line 41. The attribute's comment: “part 2”.

instance [Algebra.IsCentral k A] [Algebra.IsCentral k A'] : Algebra.IsCentral k (A ⊗[k] A')

Declarations registered for the tag:

Tag 074H, a lemma

Tag 074H in the Stacks Project.

Algebra.IsCentral.baseChange, an instance in StacksCore (human-reviewed), declared in StacksCore/Algebra/Central/TensorProduct.lean, line 45. The attribute's comment: “part 2”.

instance Algebra.IsCentral.baseChange (L : Type*) [Field L] [Algebra k L] [Algebra.IsCentral k A] :
    Algebra.IsCentral L (L ⊗[k] A)

Declarations registered for the tag:

Tag 074I, a lemma

Tag 074I in the Stacks Project.

centralSimpleTensorOp, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/BrauerGroup/Basic.lean, line 44.

noncomputable def centralSimpleTensorOp (n : ℕ) [IsSimpleRing A] [Algebra.IsCentral k A]
    (hn : Module.finrank k A = n) : A ⊗[k] Aᵐᵒᵖ ≃ₐ[k] Matrix (Fin n) (Fin n) k
Sources
Leancentralizer_tensor_centralizer · Subalgebra.algebra · Subalgebra.isScalarTower_mid · FiniteDimensional.finiteDimensional_subalgebra · IsSimpleRing.isField_center · TwoSidedIdeal.map_comap_includeRight · TwoSidedIdeal.orderIsoMapIncludeRight · Algebra.TensorProduct.isSimpleRing

Section11.5 The Brauer group of a field#

Section 11.5 of the Stacks Project, Tag 074J. 4 tags here are carried by 4 declarations of the repository (all in StacksCore) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 074K, a lemma

Tag 074K in the Stacks Project.

IsSimpleRing.wedderburn_artin_divisionring_unique, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleModule/WedderburnArtin.lean, line 25. The attribute's comment: “part (ii) and (iii)”.

theorem wedderburn_artin_divisionring_unique {n n' : ℕ} [NeZero n] [NeZero n']
    {D : Type w} [DivisionRing D] [Algebra k D] {D' : Type w} [DivisionRing D'] [Algebra k D']
    (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) (wdb' : A ≃ₐ[k] Matrix (Fin n') (Fin n') D') :
    Nonempty (D ≃ₐ[k] D')

Declarations registered for the tag:

Tag 074L, a definition

Tag 074L in the Stacks Project.

BrauerGroup.instCommGroup, an instance in StacksCore (human-reviewed), declared in StacksCore/Algebra/BrauerGroup/Basic.lean, line 214. References: SGA 4½ Arcata (3.1), “abelian group structure”.

instance instCommGroup : CommGroup (BrauerGroup k)
Tag 074M, a lemma

Tag 074M in the Stacks Project.

BrauerGroup.instUniqueOfIsAlgClosed, an instance in StacksCore (human-reviewed), declared in StacksCore/Algebra/BrauerGroup/AlgClosed.lean, line 28. References: SGA 4½ Arcata (3.2.2), “special case”.

instance instUniqueOfIsAlgClosed : Unique (BrauerGroup k)
Tag 074N, a lemma

Tag 074N in the Stacks Project.

Algebra.IsCentralSimple.isSquare_finrank, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/Basic.lean, line 155.

The dimension of a central simple algebra is a perfect square.

theorem isSquare_finrank [IsSimpleRing A] [Algebra.IsCentral K A] [FiniteDimensional K A] :
    IsSquare (Module.finrank K A)
Sources
LeanIsSimpleRing.wedderburn_artin_divisionring_unique · IsBrauerEquivalent · BrauerGroup.instCommGroup · BrauerGroup.instUniqueOfIsAlgClosed · Algebra.IsCentralSimple.isSquare_finrank

Section11.6 Skolem-Noether#

Section 11.6 of the Stacks Project, Tag 074P. 2 tags here are carried by 2 declarations of the repository (all in StacksCore), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 074Q, a theorem

Tag 074Q in the Stacks Project.

skolemNoether, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SkolemNoether.lean, line 125. References: SGA 4½ Arcata (3.1.2), “more general”.

Skolem–Noether: two algebra homomorphisms from a simple algebra to a finite-dimensional central simple algebra are conjugate by a unit.

public theorem skolemNoether (K : Type u) (A B : Type v) [Field K] [Ring A] [Algebra K A]
    [Module.Finite K A] [Algebra.IsCentral K A] [IsSimpleRing A]
    [Ring B] [Algebra K B] [IsSimpleRing B] (f g : B →ₐ[K] A) :
    ∃ x : Aˣ, ∀ b : B, g b = x * f b * x⁻¹
Tag 074R, a lemma

Tag 074R in the Stacks Project.

skolemNoether', a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SkolemNoether.lean, line 141. References: SGA 4½ Arcata (3.1.2), “more general”.

public theorem skolemNoether' (K : Type u) (A : Type v) [Field K] [Ring A] [Algebra K A]
    [Module.Finite K A] [Algebra.IsCentral K A] [IsSimpleRing A] (e : A ≃ₐ[K] A) :
    ∃ x : Aˣ, ∀ a : A, e a = x * a * x⁻¹
Sources
LeanskolemNoether · skolemNoether'

Section11.7 The centralizer theorem#

Section 11.7 of the Stacks Project, Tag 074S. 4 tags here are carried by 7 declarations of the repository (all in StacksCore), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 074T, a theorem

Tag 074T in the Stacks Project.

Subalgebra.centralizer_isSimple, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/Centralizer.lean, line 154. The attribute's comment: “first part”.

The centralizer of a simple subalgebra of a finite-dimensional central simple algebra is simple.

theorem Subalgebra.centralizer_isSimple [FiniteDimensional F A] (B : Subalgebra F A)
    [IsSimpleRing B] :
    IsSimpleRing (Subalgebra.centralizer F (B : Set A))

Subalgebra.finrank_centralizer_mul_finrank, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/Centralizer.lean, line 170. The attribute's comment: “second part”.

The dimension of the centralizer of a simple subalgebra B of a finite-dimensional central simple algebra A satisfies dim C_A(B) * dim B = dim A.

theorem Subalgebra.finrank_centralizer_mul_finrank [FiniteDimensional F A]
    (B : Subalgebra F A) [IsSimpleRing B] :
    Module.finrank F (Subalgebra.centralizer F (B : Set A)) * Module.finrank F B =
      Module.finrank F A

Subalgebra.centralizer_centralizer, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/Centralizer.lean, line 186. The attribute's comment: “third part”.

The double centralizer theorem: in a finite-dimensional central simple algebra A, the centralizer of the centralizer of a simple subalgebra B is B itself.

theorem Subalgebra.centralizer_centralizer [FiniteDimensional F A] (B : Subalgebra F A)
    [IsSimpleRing B] :
    Subalgebra.centralizer F (Subalgebra.centralizer F (B : Set A) : Set A) = B
Tag 074U, a lemma

Tag 074U in the Stacks Project.

Subalgebra.tensorCentralizerEquiv, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/Centralizer.lean, line 201.

A finite-dimensional central simple algebra decomposes as the tensor product of any central simple subalgebra and its centralizer.

noncomputable def Subalgebra.tensorCentralizerEquiv [FiniteDimensional F A]
    (B : Subalgebra F A) [IsSimpleRing B] [Algebra.IsCentral F B] :
    A ≃ₐ[F] B ⊗[F] Subalgebra.centralizer F (B : Set A)
Tag 074V, a lemma

Tag 074V in the Stacks Project.

Subalgebra.maximal_comm_iff_self_centralizer, a lemma in StacksCore (human-reviewed), declared in StacksCore/Algebra/Algebra/Subalgebra/Lattice.lean, line 44. The attribute's comment: “(ii) ↔ (iii)”.

lemma Subalgebra.maximal_comm_iff_self_centralizer (L : Subalgebra k A) :
    Maximal (fun S : Subalgebra k A ↦ IsMulCommutative S) L ↔
      Subalgebra.centralizer k L = L

Subalgebra.isMaximal_comm_iff_finrank, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/Centralizer.lean, line 212. The attribute's comment: “(ii) ↔ (i)”.

lemma Subalgebra.isMaximal_comm_iff_finrank [Module.Finite F A] (L : Subalgebra F A)
    [IsMulCommutative L] [IsSimpleRing L] :
    Subalgebra.centralizer F (L : Set A) = L ↔
      Module.finrank F A = Module.finrank F L * Module.finrank F L
Tag 074W, a lemma

Tag 074W in the Stacks Project.

Subalgebra.isMaximal_comm_iff_finrank, a lemma in StacksCore (human-reviewed), declared in StacksCore/RingTheory/SimpleRing/Centralizer.lean, line 212.

lemma Subalgebra.isMaximal_comm_iff_finrank [Module.Finite F A] (L : Subalgebra F A)
    [IsMulCommutative L] [IsSimpleRing L] :
    Subalgebra.centralizer F (L : Set A) = L ↔
      Module.finrank F A = Module.finrank F L * Module.finrank F L
Sources
LeanSubalgebra.centralizer_isSimple · Subalgebra.finrank_centralizer_mul_finrank · Subalgebra.centralizer_centralizer · Subalgebra.tensorCentralizerEquiv · Subalgebra.maximal_comm_iff_self_centralizer · Subalgebra.isMaximal_comm_iff_finrank

Section11.8 Splitting fields#

Section 11.8 of the Stacks Project, Tag 074X. 6 tags here are carried by 9 declarations of the repository (all in StacksCore), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 074Y, a definition

Tag 074Y in the Stacks Project.

Algebra.IsSplit, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/Basic.lean, line 34.

A field extension L of K splits a K-algebra A if L ⊗[K] A is isomorphic to a (nontrivial) matrix algebra over L.

def IsSplit (L : Type w) [CommRing L] [Algebra K L] : Prop
Tag 074Z, a theorem

Tag 074Z in the Stacks Project.

Algebra.IsSplit.exists_embedding, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/Embedding.lean, line 156. The attribute's comment: “(1) ⇒ (2)”.

Every finite splitting field embeds into a representative of the Brauer class: if a finite extension L/K splits the central simple algebra A, then the class of A has a representative B of dimension [L : K]² receiving a K-algebra embedding of L. This is the converse of Algebra.IsCentralSimple.split_of_finrank.

theorem exists_embedding {A : Type u} [Ring A] [Algebra K A] [FiniteDimensional K A]
    [IsSimpleRing A] [Algebra.IsCentral K A] [FiniteDimensional K L]
    (hs : Algebra.IsSplit K A L) :
    ∃ (B : Type u) (_ : Ring B) (_ : Algebra K B) (_ : FiniteDimensional K B)
      (_ : IsSimpleRing B) (_ : Algebra.IsCentral K B) (_ : L →ₐ[K] B),
      BrauerGroup.mk K B = BrauerGroup.mk K A ∧
      Module.finrank K B = Module.finrank K L ^ 2

Algebra.isSplit_iff_exists_similar, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/Embedding.lean, line 189.

Stacks 074Z, in full. For a finite extension L/K and a finite central simple K-algebra A, the following are equivalent:

  1. L splits A;
  2. some finite central simple algebra B similar to A contains L and has [B : K] = [L : K]².

Forwards is Algebra.IsSplit.exists_embedding. Backwards combines Algebra.IsCentralSimple.split_of_finrank — which gives that L splits the representative B it is embedded in — with Algebra.isSplit_congr, which transports splitting along the similarity B ∼ A. Note the pow_two shuffle: the tag writes the dimension as a square, split_of_finrank as a product.

theorem _root_.Algebra.isSplit_iff_exists_similar {A : Type u} [Ring A] [Algebra K A]
    [FiniteDimensional K A] [IsSimpleRing A] [Algebra.IsCentral K A] [FiniteDimensional K L] :
    Algebra.IsSplit K A L ↔
      ∃ (B : Type u) (_ : Ring B) (_ : Algebra K B) (_ : FiniteDimensional K B)
        (_ : IsSimpleRing B) (_ : Algebra.IsCentral K B) (_ : L →ₐ[K] B),
        BrauerGroup.mk K B = BrauerGroup.mk K A ∧
        Module.finrank K B = Module.finrank K L ^ 2
Tag 0750, a lemma

Tag 0750 in the Stacks Project.

DivisionRing.isSplit_of_maximal_comm, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/DivisionRing.lean, line 49.

Stacks 0750: a maximal subfield of a finite central division algebra D over k is a splitting field for D.

"Maximal subfield" is rendered as a subalgebra maximal among the commutative subalgebras. That is the same notion here: every subalgebra of a finite-dimensional division algebra is a division ring, and every commutative one is a field (Subalgebra.fieldOfIsMulCommutative), so the commutative subalgebras of D are exactly its subfields.

Maximality is stated with Maximal rather than through the numerical criterion Subalgebra.isMaximal_comm_iff_finrank; the latter is 074V/074W content, and using it here would make the statement circular with its own proof.

theorem DivisionRing.isSplit_of_maximal_comm (L : Subalgebra k D) [IsMulCommutative L]
    (hL : Maximal (fun S : Subalgebra k D ↦ IsMulCommutative S) L) :
    Algebra.IsSplit k D L
Tag 0751, a lemma

Tag 0751 in the Stacks Project.

Algebra.IsSplit.degree_dvd_finrank, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/Finrank.lean, line 194.

Stacks 0751: for a finite central division algebra D over k with d² = [D : k], the degree d divides [L : k] for every finite splitting field L of D.

Note this is genuinely stronger than d ≤ [L : k]. The divisibility is what the dimension count actually produces — the cofactor is finrank D (Fin m → L) for the column module of the splitting — so the ≤ form is the corollary, not the other way round.

The division hypothesis is essential, as for DivisionRing.split_iff_finrank: M₂(k) is split by L = k with degree k M₂(k) = 2 and finrank k k = 1, and 2 ∤ 1.

public theorem Algebra.IsSplit.degree_dvd_finrank {D : Type*} [DivisionRing D] [Algebra k D]
    [Module.Finite k D] [Algebra.IsCentral k D] [Module.Finite k L]
    (h : Algebra.IsSplit k D L) : degree k D ∣ Module.finrank k L
Tag 0752, a proposition

Tag 0752 in the Stacks Project.

DivisionRing.exists_separable_maxSubfield, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Algebra/Subalgebra/DivisionRing.lean, line 221. The attribute's comment: “the separable maximal subfield”.

Koethe's theorem: a finite-dimensional central division algebra D over a field k contains a separable maximal subfield, stated here as: there is a commutative subalgebra L that is self-centralizing — equivalently maximal commutative, by Subalgebra.maximal_comm_iff_self_centralizer — and separable over k. Commutativity of L follows from self-centralizing-ness via Subalgebra.le_centralizer_iff_isMulCommutative.

Proof strategy:

  1. By Zorn's lemma, pick L maximal among commutative separable subalgebras of D (directed suprema preserve both properties).
  2. Suppose L is not self-centralizing and let C ≠ L be its centralizer. Then C is a division ring (Subalgebra.divisionRingOfFinite), finite-dimensional over the field L (Subalgebra.fieldOfIsMulCommutative), and central over L: by the double centralizer theorem, Z(C) = C ∩ C_D(C) = C ∩ L = L (the scoped instance Subalgebra.isCentral_centralizer).
  3. By the Jacobson–Noether theorem (exists_separable_and_not_isCentral') applied to the noncommutative division algebra C over L, there is x ∈ C \ L separable over L.
  4. L' := k[L, x] is commutative (since x centralizes L) and separable over k — it is generated over L by the single separable element x, and separability is transitive in the tower k ⊆ L ⊆ L' (JacobsonNoether.adjoin_insert_mem_S).
  5. So L' is a member of the Zorn family strictly containing L, contradicting maximality.
theorem DivisionRing.exists_separable_maxSubfield [FiniteDimensional k D]
    [Algebra.IsCentral k D] :
    ∃ L : Subalgebra k D, Subalgebra.centralizer k (L : Set D) = L ∧
      Algebra.IsSeparable k L

Algebra.IsCentralSimple.exists_finite_sep_split, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/DivisionRing.lean, line 74. The attribute's comment: “in particular: every Brauer class has a finite separable splitting field”.

Stacks 0752, the "in particular" clause: every Brauer class has a finite separable splitting field. Concretely, every finite central simple k-algebra is split by a finite separable subextension of any chosen algebraic closure.

theorem Algebra.IsCentralSimple.exists_finite_sep_split :
    ∃ K : IntermediateField k k_bar, Module.Finite k K ∧
      Algebra.IsSeparable k K ∧ Algebra.IsSplit k A K
Tag 0753, a lemma

Tag 0753 in the Stacks Project.

Algebra.IsSplit.matrix_size_eq_degree, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/CentralSimple.lean, line 87. The attribute's comment: “the integer d is called the degree of A”.

Stacks 0753, closing sentence: the matrix size in any splitting of A is the degree of A. This is what licenses calling it "the" integer d — clauses (3), (4) and (5) of Algebra.isCentralSimple_tfae each quantify their own witness, and this identifies them all with Algebra.IsCentralSimple.degree k A.

No central-simple hypotheses are needed: a splitting already forces finrank k A = n * n, and degree is by definition Nat.sqrt of that. In the tag's setting A is of course central simple, but the identification of the witness does not depend on it.

theorem Algebra.IsSplit.matrix_size_eq_degree (L : Type w) [Field L] [Algebra k L]
    {n : ℕ} (e : L ⊗[k] A ≃ₐ[L] Matrix (Fin n) (Fin n) L) :
    n = Algebra.IsCentralSimple.degree k A

Algebra.isCentralSimple_tfae, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Split/CentralSimple.lean, line 112. References: SGA 4½ Arcata (3.1.1).

Stacks 0753: for a k-algebra A the following are equivalent.

  1. A is a finite central simple k-algebra.
  2. A is a finite-dimensional k-vector space, k is the centre of A, and A has no nontrivial two-sided ideal.
  3. A ⊗ k̄ is a matrix algebra over k̄.
  4. A ⊗ kˢᵉᵖ is a matrix algebra over kˢᵉᵖ.
  5. A ⊗ k' is a matrix algebra over k' for some finite Galois k'/k.
  6. A ≅ Mat(n, K) for some n ≥ 1 and some finite central division algebra K over k.

The proof is a star around (1): each of (2)–(6) is proved equivalent to (1) directly. The forward directions are the splitting constructions of §11.08; the return directions (3) ⇒ (1), (4) ⇒ (1), (5) ⇒ (1) all factor through Algebra.IsSplit.finite_central_simple.

theorem Algebra.isCentralSimple_tfae (k_bar : Type w) [Field k_bar] [Algebra k k_bar]
    [IsAlgClosed k_bar] [Algebra.IsAlgebraic k k_bar] :
    [ Module.Finite k A ∧ Algebra.IsCentral k A ∧ IsSimpleRing A,
      Module.Finite k A ∧ Subalgebra.center k A = ⊥ ∧ IsSimpleOrder (TwoSidedIdeal A),
      Algebra.IsSplit k A k_bar,
      Algebra.IsSplit k A (separableClosure k k_bar),
      ∃ K : IntermediateField k k_bar, Module.Finite k K ∧ IsGalois k K ∧ Algebra.IsSplit k A K,
      ∃ (n : ℕ) (_ : NeZero n) (D : Type v) (_ : DivisionRing D) (_ : Algebra k D)
        (_ : Module.Finite k D) (_ : Algebra.IsCentral k D),
        Nonempty (A ≃ₐ[k] Matrix (Fin n) (Fin n) D) ].TFAE
Sources
LeanAlgebra.IsSplit · Algebra.IsSplit.exists_embedding · Algebra.isSplit_iff_exists_similar · DivisionRing.isSplit_of_maximal_comm · Algebra.IsSplit.degree_dvd_finrank · DivisionRing.exists_separable_maxSubfield · Algebra.IsCentralSimple.exists_finite_sep_split · Algebra.IsSplit.matrix_size_eq_degree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.