associator_hom_left_snd_snd — Mathlib

English

The left component of the associator morphism in Over X satisfies a similar fst/snd compatibility with the snd projection as in the previous left-fst case.

Русский

Левый компонент ассоциатора в Over X удовлетворяет аналогичной совместимости с snd-прокцией, подобно предыдущему случаю с fst.

LaTeX

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

Lean4

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

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