associator_inv_left_fst_snd — Mathlib

English

The inverse associator satisfies a relation connecting its left projection with fst and snd projections in Over X.

Русский

Обратный ассоциатор удовлетворяет соотношению между левой проекцией и fst/snd-прокциями в Over X.

LaTeX

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

Lean4

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

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