μ_inv_natural_right — Mathlib

English

The inverse associator μ is natural with respect to right whiskering: for any morphism g: Y1 → Y2 and object X, the left side given by the inverse of μ at X,Y1 whiskered with X against g equals the whiskered image of g with X followed by the inverse of μ at X,Y2.

Русский

Обратная ассоциатор μ естественным образом учитывает правое придвижение: для любой стрелки g: Y1 → Y2 и объекта X левая часть с инверсией μ на X,Y1, затем прирост X, равна образу g через X и инверсии μ на X,Y2.

LaTeX

$$$(\\mu L W ε X Y_1).inv \\;\\gg\\; (L').\\mathrm{obj} X \\triangleleft (L').\\mathrm{map} g = (L').\\mathrm{map}(X \\triangleleft g) \\;\\gg\\; (\\mu L W ε X Y_2).inv$$$

Lean4

@[reassoc (attr := simp)]
theorem μ_inv_natural_right (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
    (μ L W ε X Y₁).inv ≫ (L').obj X ◁ (L').map g = (L').map (X ◁ g) ≫ (μ L W ε X Y₂).inv := by simp [Iso.eq_comp_inv]

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