lift_includeLeft_includeRight — Mathlib

English

For simple tensors, the lift takes a ⊗ b to f(a) g(b) in the target algebra.

Русский

Для простого тензора a ⊗ b лифт обрабатывает его в виде f(a) g(b) в целевой алгебре.

LaTeX

$$$\\mathrm{lift}\ f\ g\ hfg\\; (a \\otimes b) = f(a) \\; g(b) \\quad (a\\in A,\; b\\in B).$$$

Lean4

@[simp]
theorem lift_includeLeft_includeRight :
    lift includeLeft includeRight (fun _ _ => (Commute.one_right _).tmul (Commute.one_left _)) = .id S (A ⊗[R] B) := by
  ext <;> simp

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