English
Let K be a commutative semiring and B, C be K-algebras. If the map K → B is injective, C is flat as a K-module, and B ⊗_K C is central over K, then C is central over K.
Русский
Пусть K — коммутативное полукольцо и B, C — K-алгебры. Если отображение K → B инъективно, C плоско над K и B ⊗_K C центрально над K, то C центрально над K.
LaTeX
$$$\\big( \\operatorname{IsCentral}(K, B \\otimes_K C) \\big) \\land \\big( \\inj : \\operatorname{Injective}(\\operatorname{algebraMap}\\, K\\, B) \\big) \\land \\big( \\text{Flat}_K(C) \\big) \\Rightarrow \\operatorname{IsCentral}(K, C)$$$
Lean4
theorem right_of_tensor (inj : Function.Injective (algebraMap K B)) [Module.Flat K C] [Algebra.IsCentral K (B ⊗[K] C)] :
IsCentral K C :=
have : IsCentral K (C ⊗[K] B) := IsCentral.of_algEquiv K _ _ <| Algebra.TensorProduct.comm _ _ _
left_of_tensor K C B inj
