one_mul_hom — Mathlib

English

For any f: X → M, the associator interacts with μ to satisfy a left-hand associativity identity: (α_XMM).hom ≫ (f ⊗ μ) ≫ μ = (f ⊗ 1_M ≫ μ) ≫ 1_M ≫ μ.

Русский

Для любого f: X → M отображение ассоциатора взаимодействует с μ и удовлетворяет левому выражению ассоциативности: (α_{X M M})^{hom} ∘ (f ⊗ μ) ∘ μ = (f ⊗ 1_M ∘ μ) ∘ 1_M ∘ μ.

LaTeX

$$$ (\alpha_{X M M})^{hom} \circ (f \otimes \mu) \circ \mu = ((f \otimes \mathrm{Id}_M) \circ \mu) \circ (\mathrm{Id}_M \otimes \mathrm{Id}_M) \circ \mu $$$

Lean4

@[simp]
theorem one_mul_hom {Z : C} (f : Z ⟶ M) : (η[M] ⊗ₘ f) ≫ μ[M] = (λ_ Z).hom ≫ f := by
  rw [tensorHom_def'_assoc, one_mul, leftUnitor_naturality]

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