associator_inv_left_fst_fst — Mathlib

English

A further relation holds for the left leg of the associator with fst fst structure in Over X.

Русский

Дополнительное соотношение для левой ножки ассоциатора с fst fst-структурой в Over X.

LaTeX

$$$ (\\alpha_{R,S,T})^{\\mathrm{hom}}_{\\mathrm{left}} \\circ \\mathrm{fst}(\\mathrm{fst}(R,h),S,h) = \\mathrm{fst}(R,h) \\circ \\mathrm{fst}(S,h) $$$

Lean4

@[reassoc (attr := simp)]
theorem associator_inv_left_fst_fst (R S T : Over X) :
    (α_ R S T).inv.left ≫ pullback.fst (pullback.fst _ _ ≫ _) _ ≫ pullback.fst _ _ = pullback.fst _ _ :=
  (limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _)

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