rightUnitor_inv_comp_tensorHom — Mathlib

English

For f: X → Y and g: 𝟙_C → Z, we have (ρ_X).inv ≫ (f ⊗ₘ g) = f ≫ (ρ_Y).inv ≫ Y ◁ g.

Русский

Для f: X → Y и g: 𝟙_C → Z выполняется (ρ_X).inv ≫ (f ⊗ₘ g) = f ≫ (ρ_Y).inv ≫ Y ◁ g.

LaTeX

$$$ (\\rho_X).inv \\circ (f \\otimes_{\\mathrm{⊗}} g) = f \\circ (\\rho_Y).inv \\circ (Y \\triangleleft g) $$$

Lean4

@[reassoc]
theorem rightUnitor_inv_comp_tensorHom {X Y Z : C} (f : X ⟶ Y) (g : 𝟙_ C ⟶ Z) :
    (ρ_ X).inv ≫ (f ⊗ₘ g) = f ≫ (ρ_ Y).inv ≫ Y ◁ g := by simp [tensorHom_def]

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