lift_map — Mathlib

English

Lift of fst and snd after composing with morphisms equals the tensor of the components.

Русский

Лифт fst и snd после композиции эквивалентен тензору компонент.

LaTeX

$$lift (fst _ _ ≫ g) (snd _ _ ≫ g') = g ⊗ g'$$

Lean4

@[reassoc (attr := simp)]
theorem lift_map {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
    lift f g ≫ (h ⊗ₘ k) = lift (f ≫ h) (g ≫ k) := by ext <;> simp

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