includeRight_map_center_le — Mathlib

English

The image of the right center under includeRight embeds into the center of B ⊗_K C.

Русский

Образ правого центра через includeRight вложится в центр B ⊗_K C.

LaTeX

$$$(\\operatorname{center}_K C).map(\\mathrm{includeRight}) \\le \\operatorname{center}_K(B \\otimes_K C)$$$

Lean4

theorem includeRight_map_center_le : (Subalgebra.center K C).map includeRight ≤ Subalgebra.center K (B ⊗[K] C) :=
  fun x hx ↦ by
  simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
  obtain ⟨c, hc0, rfl⟩ := hx
  intro bc
  induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

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