left_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 C is nontrivial, then B is central over K.

Русский

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

LaTeX

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

Lean4

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

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