associator_eqToHom_hom — Mathlib

English

If f=f', g=g', h=h' then the associator is compatible with these equalities: its hom component is equal to the corresponding composition of α_ and eqToHom adjustments.

Русский

Если f=f', g=g', h=h', то ассоциатор совместим с ними: компоненту-гачHom равен соответствующей композиции α и eqToHom корректировок.

LaTeX

$$$\\big(\\alpha_f g h).\\mathrm{hom} = (\\text{eqToHom}) \\cdot ... \\cdot (\\alpha_{f' g' h'}).\\mathrm{hom}$$$

Lean4

@[reassoc]
theorem associator_eqToHom_hom {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) :
    (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).hom =
      (eqToHomTransIso e₁ e₂).inv ▷ eqToHom e₃ ≫
        (eqToHomTransIso (e₁.trans e₂) e₃).inv ≫
          (eqToHomTransIso e₁ (e₂.trans e₃)).hom ≫ eqToHom e₁ ◁ (eqToHomTransIso e₂ e₃).hom :=
  by
  subst_vars
  simp

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