English
The image of the left center under includeLeft embeds into the center of B ⊗_K C.
Русский
Образ левого центра через includeLeft можно включить в центр B ⊗_K C.
LaTeX
$$$(\\operatorname{center}_K B).map(\\mathrm{includeLeft}) \\le \\operatorname{center}_K(B \\otimes_K C)$$$
Lean4
theorem includeLeft_map_center_le : (Subalgebra.center K B).map includeLeft ≤ Subalgebra.center K (B ⊗[K] C) :=
by
intro x hx
simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
obtain ⟨b, hb0, rfl⟩ := hx
intro bc
induction bc using TensorProduct.induction_on with
| zero => simp
| tmul b' c => simp [hb0]
| add _ _ _ _ => simp_all [add_mul, mul_add]