English
Let K be a commutative semiring and B, C be K-algebras. If the map K → C is injective, B is flat as a K-module, and the tensor product B ⊗_K C is central over K, then B is central over K.
Русский
Пусть K — коммутативное полукольцо и B, C — K-алгебры. Если отображение K → C инъективно, B плоско как K-модуль, а тензорное произведение B ⊗_K C центрально над K, то B является центральной над K.
LaTeX
$$$\\big( \\operatorname{IsCentral}(K, B \\otimes_K C) \\big) \\land \\big( \\inj : \\operatorname{Injective}(\\operatorname{algebraMap}\\, K\\, C) \\big) \\land \\big( \\text{Flat}_K(B) \\big) \\Rightarrow \\operatorname{IsCentral}(K, B)$$$
Lean4
theorem left_of_tensor (inj : Function.Injective (algebraMap K C)) [Module.Flat K B]
[hbc : Algebra.IsCentral K (B ⊗[K] C)] : IsCentral K B where
out :=
(Subalgebra.map_le.mp ((includeLeft_map_center_le K B C).trans hbc.1)).trans fun _ ⟨k, hk⟩ ↦
⟨k, includeLeft_injective (S := K) inj hk⟩
