leftUnitor_inv_one_tensor_mul — Mathlib

English

For any morphism f: X → M, the inverse left unitor interacts with η to recover f: (λ_M)^{-1} ∘ (η ⊗ f) ∘ μ = f.

Русский

Для любого отображения f: X → M обратный левый унитор взаимодействует с η так, чтобы вернуть f: (λ_M)^{-1} ∘ (η ⊗ f) ∘ μ = f.

LaTeX

$$$ (\lambda_M)^{-1} \circ (\eta \otimes f) \circ \mu = f $$$

Lean4

@[reassoc (attr := mon_tauto)]
theorem leftUnitor_inv_one_tensor_mul (f : X₁ ⟶ M) : (λ_ _).inv ≫ (η ⊗ₘ f) ≫ μ = f := by simp [tensorHom_def']

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