transform_map_leftUnitor — Mathlib

English

The left unitor interacts with the transform, yielding a canonical factorization through transformObjComp with id F G, whiskering, and the leftUnitor.

Русский

Левый единичный мopфизм взаимодействует с transform, образуя каноническую факторизацию через transformObjComp с id F G, взвешивание и leftUnitor.

LaTeX

$$$ (transform X).map (\lambda_ ψ).hom = (transformObjComp X (.id F G) ψ).hom \circ whiskerRight (transformObjId X F G).hom \circ (transform X |>.obj ψ).leftUnitor.hom $$$

Lean4

theorem transform_map_leftUnitor (X : Type u₇) [Category.{v₇} X] (ψ : CatCospanTransform F G F₁ G₁) :
    (transform X).map (λ_ ψ).hom =
      (transformObjComp X (.id F G) ψ).hom ≫
        whiskerRight (transformObjId X F G).hom (transform X |>.obj ψ) ≫ (transform X |>.obj ψ).leftUnitor.hom :=
  by cat_disch

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