includeLeft_map_center_le — Mathlib

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]

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