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] [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] [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)