right_of_tensor_of_field — Mathlib

English

Let K be a field and B, C be K-algebras. If B ⊗_K C is central over K and B is nontrivial, then C is central over K.

Русский

Пусть K — поле, B и C — K-алгебры. Если B ⊗_K C централизовано над K и B не тривиальна, то C централизована над K.

LaTeX

$$$( \\operatorname{IsCentral}(K, B \\otimes_K C) ) \\land ( \\operatorname{Nontrivial}(B) ) \\Rightarrow \\operatorname{IsCentral}(K, C)$$$

Lean4

/-- Let `B` and `C` be two algebras over a field `K`, if `B ⊗[K] C` is central and `B` is
  non-trivial, then `C` is central. -/
theorem right_of_tensor_of_field (K B C : Type*) [Field K] [Ring B] [Ring C] [Nontrivial B] [Algebra K B] [Algebra K C]
    [IsCentral K (B ⊗[K] C)] : IsCentral K C :=
  right_of_tensor K B C <| FaithfulSMul.algebraMap_injective K B

Похожие утверждения