transform_map_rightUnitor — Mathlib

English

Analogous to the left case, the right unitor yields a canonical factorization through transformObjComp and whiskering with a rightUnitor.

Русский

Аналогично слева, правый единичный мopфизм образует каноническую факторизацию через transformObjComp и взвешивание правого единичного.

LaTeX

$$$ (transform X).map (\rho_ ψ).hom = (transformObjComp X ψ (.id F₁ G₁)).hom \circ whiskerLeft (transform X |>.obj ψ) (transformObjId X F₁ G₁).hom \circ (transform X |>.obj ψ).rightUnitor.hom $$$

Lean4

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

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