tensorδ_tensorμ — Mathlib

English

A simplified form of the functorial behavior of braiding under a braided functor, highlighting the compatibility through δ and μ.

Русский

Упрощённая форма поведения braiding под браидированным функтором через δ и μ.

LaTeX

$$$$ F.map (β_{X,Y}) = δ_{F X F Y} \circ (β_{F X F Y}) \circ μ_{Y,X}. $$$$

Lean4

@[reassoc (attr := simp)]
theorem tensorδ_tensorμ (X₁ X₂ Y₁ Y₂ : C) : tensorδ X₁ X₂ Y₁ Y₂ ≫ tensorμ X₁ X₂ Y₁ Y₂ = 𝟙 _ := by
  simp only [tensorδ, ← whiskerLeft_comp_assoc, tensorμ, assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc,
    inv_hom_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp, Iso.hom_inv_id]

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