map_comp_includeRight — Mathlib

English

The swap map comm R C D composed with map f g equals the composition map with swapped factors, i.e., comm ∘ map f g = map g f ∘ comm.

Русский

Обменная карта после композиции с отображением эквивалентна композиции после обмена факторов: comm ∘ map f g = map g f ∘ comm.

LaTeX

$$$ (\\mathrm{comm}_{R} C D) \\circ (\\mathrm{map} f g) = (\\mathrm{map} g f) \\circ (\\mathrm{comm}_{R} A B) $$$

Lean4

@[simp]
theorem map_comp_includeRight (f : A →ₐ[R] C) (g : B →ₐ[R] D) : (map f g).comp includeRight = includeRight.comp g :=
  map_restrictScalars_comp_includeRight f g

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