leftUnitor'_inv — Mathlib

English

Let K be a homological complex in a monoidal category. The i-th component of the inverse of the left unitor acting on K is given by the explicit composite built from the left unitor on K.X_i, the unit of the tensor, and the canonical whiskering with K.X_i. In particular, (leftUnitor' K)^{-1}_i equals the composite of the inverse of the usual left unitor at K.X_i with the unit-correcting whisker and the unit insertion.

Русский

Пусть K — гомологический комплекс в мономодульной категории. i-й компонент обратного левого унитора, действующего на K, задаётся явным композитом, построенным из обратного обычного левого унитора на K.X_i, единичного тензорного модуля и стандартной обрезки через тензорный блок. То есть (leftUnitor' K)^{-1}_i выражается как композиция λ_{K.X_i}^{-1} с whiskering и вставкой тензорной единицы.

LaTeX

$$$\\bigl(\\mathrm{leftUnitor}' K\\bigr)^{-1}_i = (\\lambda_{K.X_i})^{-1} \\;\\circ\\; \\bigl((\\mathrm{singleObjXSelf} \\; c \\; 0 \\; \\mathrm{Id}_C)^{-1} \\; \\triangleright\\; (K.X_i)\\bigr) \\;\\circ\\; \\iota_{\\otimes}( \\mathrm{tensorUnit} \\, C \\, c) \\; K \\\\ 0 \\\\ i \\\\ i \\\\ (0 + i) $$$

Lean4

theorem leftUnitor'_inv (i : I) :
    (leftUnitor' K).inv i =
      (λ_ (K.X i)).inv ≫
        ((singleObjXSelf c 0 (𝟙_ C)).inv ▷ (K.X i)) ≫ ιTensorObj (tensorUnit C c) K 0 i i (zero_add i) :=
  by
  dsimp [leftUnitor']
  rw [GradedObject.Monoidal.leftUnitor_inv_apply, assoc, assoc, Iso.cancel_iso_inv_left,
    GradedObject.Monoidal.ι_tensorHom]
  dsimp
  rw [tensorHom_id, ← comp_whiskerRight_assoc]
  congr 2
  rw [← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom, Iso.hom_inv_id_assoc]
  dsimp [tensorUnitIso]
  rw [dif_pos rfl]
  rfl

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