tensorHom_inv_inv_mul — Mathlib

English

The map (ι_A ⊗ ι_A) composed with μ equals the braiding: (β_{A,A})^{hom} ∘ μ ∘ ι.

Русский

Отображение (ι_A ⊗ ι_A) ∘ μ равно перекрещиванию: (β_{A,A})^{hom} ∘ μ ∘ ι.

LaTeX

$$$(\iota_A \otimes \iota_A) \circ \mu = (\beta_{A,A})^{\mathrm{hom}} \circ \mu \circ \iota$$$

Lean4

@[reassoc]
theorem tensorHom_inv_inv_mul [BraidedCategory C] (A : C) [GrpObj A] : (ι[A] ⊗ₘ ι[A]) ≫ μ = (β_ A A).hom ≫ μ ≫ ι := by
  rw [mul_inv A, SymmetricCategory.symmetry_assoc]

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