associator_hom_left_fst — Mathlib

English

The left component of the associator morphism in Over X satisfies a commutation relation with the fst projection, expressing that moving the left projection through the associator yields the expected fst projection.

Русский

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

LaTeX

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

Lean4

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

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