leftUnitor_inv_comp_tensorHom — Mathlib

English

For f: 𝟙_C → Y and g: X → Z, the relation (λ_X).inv ≫ (f ⊗ₘ g) = g ≫ (λ_Z).inv ≫ f ▷ Z holds.

Русский

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

LaTeX

$$$ (\\lambda_X).inv \\circ (f \\otimes_{\\mathrm{⊗}} g) = g \\circ (\\lambda_Z).inv \\circ (f \\triangleright Z) $$$

Lean4

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

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