comm_comp_map — Mathlib

English

The composition with restrictScalars and includeRight equals includeRight after restricting scalars.

Русский

Композиция с restrictScalars и includeRight эквивалентна includeRight после ограничения скалярами.

LaTeX

$$$ ((\\mathrm{map}\\; f\\; g).\\mathrm{restrictScalars}\\; R) \\circ \\mathrm{includeRight} = \\mathrm{includeRight} \\circ g $$$

Lean4

theorem comm_comp_map (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
    (TensorProduct.comm R C D : C ⊗[R] D →ₐ[R] D ⊗[R] C).comp (Algebra.TensorProduct.map f g) =
      (Algebra.TensorProduct.map g f).comp (TensorProduct.comm R A B).toAlgHom :=
  by ext <;> rfl

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