mulMap_map_comp_eq — Mathlib

English

For a homomorphism f: S →ₐ[R] T, the product map after mapping A and B by f equals the composition f ∘ mulMap A B after applying algebra-tensor-product mapping on A,B via f.subalgebraMap.

Русский

Для гомоморфизма f: S →ₐ[R] T произведение в тензопрочте после отображения A и B по f равно композиции f ∘ mulMap A B после применения отображения в тензорном произведении через f.subalgebraMap.

LaTeX

$$$(mulMap (A.map f) (B.map f)) \circ (Algebra.TensorProduct.map (f.subalgebraMap A) (f.subalgebraMap B)) = f \circ (mulMap A B)$$$

Lean4

theorem mulMap_map_comp_eq (f : S →ₐ[R] T) :
    (mulMap (A.map f) (B.map f)).comp (Algebra.TensorProduct.map (f.subalgebraMap A) (f.subalgebraMap B)) =
      f.comp (mulMap A B) :=
  by ext <;> simp

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