English
Compatibility condition between comultiplication, multiplication and braiding maps in a bimodule M.
Русский
Условие совместимости между ко-множителем, умножителем и браидингом для би-модуля M.
LaTeX
$$$$ Δ[M] ⊗ Δ[M] ≫ α_{M,M,M}.hom ≫ M \\triangleleft α_{M,M} ^{−1} ≫ M \\triangleleft β_{M M} .hom ▷ M ≫ M \\triangleleft α_{M,M}^{hom} ≫ (α_{M,M,M})^{−1} ≫ (μ[M] ⊗ μ[M]) = μ[M] ≫ Δ[M] $$$$
Lean4
/-- Compatibility of the monoid and comonoid structures, in terms of morphisms in `C`. -/
@[reassoc (attr := simp)]
theorem compatibility (M : C) [BimonObj M] :
(Δ[M] ⊗ₘ Δ[M]) ≫
(α_ _ _ (M ⊗ M)).hom ≫
M ◁ (α_ _ _ _).inv ≫ M ◁ (β_ M M).hom ▷ M ≫ M ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv ≫ (μ[M] ⊗ₘ μ[M]) =
μ[M] ≫ Δ[M] :=
by simp only [BimonObj.mul_comul, tensorμ, Category.assoc]
