English
Two cancellation formulas show that inserting an isomorphism in the middle commutes with enrichment and composition in two dual forms.
Русский
Две формулы отмены показывают, что вставка изоморфизма посередине коммутирует обогащение и композицию двумя симметричными способами.
LaTeX
$$$eHomWhiskerLeft\,V\,X\,\alpha.hom \; \gg\; _ \; \llcorner \; eHomWhiskerRight\,V\,\alpha.inv\, Z \; \gg\; eComp\,V\,X\,Y\,Z = eComp\,V\,X\,Y\,Z$ и дополнительная симпатичная форма.$$
Lean4
/-- Given an isomorphism `α : Y ≅ Y₁` in C, the enriched composition map
`eComp V X Y Z : (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z)` factors through the `V`
object `(X ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z)` via the map defined by whiskering in the
middle with `α.hom` and `α.inv`. -/
@[reassoc]
theorem eHom_whisker_cancel {X Y Y₁ Z : C} (α : Y ≅ Y₁) :
eHomWhiskerLeft V X α.hom ▷ _ ≫ _ ◁ eHomWhiskerRight V α.inv Z ≫ eComp V X Y₁ Z = eComp V X Y Z :=
by
dsimp [eHomWhiskerLeft, eHomWhiskerRight]
simp only [MonoidalCategory.whiskerLeft_comp_assoc, whisker_assoc_symm, triangle_assoc_comp_left_inv_assoc, e_assoc',
assoc]
simp only [← comp_whiskerRight_assoc]
change (eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ _ ≫ _ = _
simp [← eHomWhiskerLeft_comp]
