lmul'_comp_map — Mathlib

English

If (lmul' R) is the left-multiplication map and map f g: A ⊗ B → S is the universal bilinear map induced by AlgHoms f and g, then their composition equals the lift of f and g. In particular, (lmul' R) ∘ (map f g) = lift f g (λ _ _ → .all _ _).

Русский

Если отображение левого умножения и каноническое отображение-умножение через тензорное произведение задаются параллельно гомоморфизмам f и g, то композиция совпадает с каноническим поднятым отображением lift.

LaTeX

$$$ (lmul' \; R) \circ (TensorProduct.map\; f\; g) = \mathrm{lift}\; f\; g\; (\lambda\ _\ _ \mapsto .all\ _\ _) $$$

Lean4

theorem lmul'_comp_map (f : A →ₐ[R] S) (g : B →ₐ[R] S) : (lmul' R).comp (map f g) = lift f g (fun _ _ ↦ .all _ _) := by
  ext <;> rfl

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