English
Dual to the previous, describing how the inverse of the associator interacts with unit morphisms.
Русский
Дуал к предыдущему: описывает взаимодействие обратного ассоциатора с единичными отображениями.
LaTeX
$$$(\\text{associator}^{-1} F G H)_{(x⊗y,z)} \\circ (\\text{unit } F G)_{(x,y)} = (\\text{unit } (F ⊛ G) H)_{(x⊗y,z)} \\circ (\\text{unit } F G)_{(x,y)}$$$
Lean4
/-- Characterizing the forward direction of the associator isomorphism
with respect to the unit transformations. -/
@[reassoc (attr := simp)]
theorem associator_hom_unit_unit (x y z : C) :
(unit F G).app (x, y) ▷ (H.obj z) ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ (associator F G H).hom.app ((x ⊗ y) ⊗ z) =
(α_ _ _ _).hom ≫
(F.obj x ◁ (unit G H).app (y, z)) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (F ⊛ G ⊛ H).map (α_ _ _ _).inv :=
by
have :=
congrArg (fun t ↦ t.app ((x, y), z)) <|
(corepresentableBy₂' F G H).homEquiv.rightInverse_symm <|
(corepresentableBy₂ F G H |>.ofIso (associatorCorepresentingIso F G H).symm |>.homEquiv (𝟙 _))
dsimp [associator, Coyoneda.fullyFaithful, corepresentableBy₂, corepresentableBy₂', Functor.CorepresentableBy.ofIso,
corepresentableBy₂, Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢
simp only [whiskerLeft_id, Category.comp_id, Category.assoc] at this
simp only [Category.assoc, this]
simp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity]
