lift_lift_associator_hom — Mathlib

English

Let X, Y, Z, W be objects and f: X → Y, g: X → Z, h: X → W be morphisms. Then lifting twice and composing with the associator hom equals lifting f with the lift g h: lift(lift f g) h ≫ α_{Y,Z,W}.hom = lift f (lift g h).

Русский

Пусть X, Y, Z, W — объекты, а f: X→Y, g: X→Z, h: X→W — морфизмы. Тогда повторный лифт и затем композиция с гомоморфизмом ассоциатора равны лифту f над лифтом g h: lift(lift f g) h ≫ α_{Y,Z,W}.hom = lift f (lift g h).

LaTeX

$$$\text{lift}(\text{lift } f\ g)\ h \;\gg\; (\alpha_{Y,Z,W})^{\mathrm{hom}} = \text{lift} \! f\ (\text{lift } g\ h)$$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_lift_associator_hom {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :
    lift (lift f g) h ≫ (α_ Y Z W).hom = lift f (lift g h) := by cat_disch

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