# 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]
[Algebra.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]
[Algebra.IsCentral K D]
{x : D}
:

x ∈ Subalgebra.center K D ↔ ∃ (a : K), x = (algebraMap K D) a

## Equations

- ⋯ = ⋯

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]
[Algebra.IsCentral k D]
:

Function.Bijective ⇑(algebraMap k K)