lift_comp_map — Mathlib

English

The lift operation commutes with tensor-product mapping: applying lift after map is the same as lifting the map after composing with the outer map.

Русский

Операция подъёма (lift) коммутирует с отображением тензорного произведения: применение подъёма после отображения равно подъёму отображения после композиции с внешним отображением.

LaTeX

$$$(\\mathrm{lift}\\ i) \\circ (\\mathrm{map}\\ f g) = \\mathrm{lift}\\ ((i \\circ f) \\mathbin{.} (\\_ . g))$$$

Lean4

theorem lift_comp_map (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (lift i).comp (map f g) = lift ((i.comp f).compl₂ g) :=
  ext' fun _ _ => rfl

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