Central Algebras

In this file, we prove some basic results about central algebras over a commutative ring.

Main results

• Algebra.IsCentral.center_eq_bot: the center of a central algebra over K is equal to K.
• Algebra.IsCentral.self: a commutative ring is a central algebra over itself.
• Algebra.IsCentral.baseField_essentially_unique: Let D/K/k is a tower of scalars where K and k are fields. If D is a nontrivial central algebra over k, K is isomorphic to k.

@[simp]

theorem Algebra.IsCentral.center_eq_bot (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] [h : IsCentral K D] : Subalgebra.center K D = ⊥

theorem Algebra.IsCentral.mem_center_iff (K : Type u) [CommSemiring K] {D : Type v} [Semiring D] [Algebra K D] [h : IsCentral K D] {x : D} : x ∈ Subalgebra.center K D ↔ ∃ (a : K), x = (algebraMap K D) a

instance Algebra.IsCentral.self (K : Type u) [CommSemiring K] : IsCentral K K

theorem Algebra.IsCentral.baseField_essentially_unique (k : Type u_1) (K : Type u_2) (D : Type u_3) [Field k] [Field K] [Ring D] [Nontrivial D] [Algebra k K] [Algebra K D] [Algebra k D] [IsScalarTower k K D] [IsCentral k D] : Function.Bijective ⇑(algebraMap k K)

theorem Algebra.IsCentral.of_algEquiv (K : Type u) [CommSemiring K] (D D' : Type v) [Semiring D] [Algebra K D] [h : IsCentral K D] [Semiring D'] [Algebra K D'] (e : D ≃ₐ[K] D') : IsCentral K D'

instance Algebra.IsCentral.instMulOpposite (K : Type u) [CommSemiring K] (D : Type v) [Semiring D] [Algebra K D] [h : IsCentral K D] : IsCentral K Dᵐᵒᵖ

Opposite algebra of a central algebra is central. This instance combined with the coming IsSimpleRing instance for the opposite of central simple algebra will be an inverse for an element in BrauerGroup, find out more about this in Mathlib/Algebra/BrauerGroup/Basic.lean.