English
Another formulation of pentagon coherence for Day convolution with extended indexing, ensuring coherence for multiple levels of convolution.
Русский
Ещё одно формулирование пентагональной когерентности Day-конволюции с расширенной индексацией.
LaTeX
$$$\\text{Pentagon}_{F,G,H,K} = \\text{Pentagon}_{F,G,H,K}$$$
Lean4
/-- Characterizing the inverse direction of the associator
with respect to the unit transformations -/
@[reassoc (attr := simp)]
theorem associator_inv_unit_unit (x y z : C) :
F.obj x ◁ (unit G H).app (y, z) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (associator F G H).inv.app (x ⊗ y ⊗ z) =
(α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
(unit F G).app (x, y) ▷ H.obj z ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ ((F ⊛ G) ⊛ H).map (α_ x y z).hom :=
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) |>.homEquiv (𝟙 _))
dsimp [associator, Coyoneda.fullyFaithful, corepresentableBy₂, corepresentableBy₂', Functor.CorepresentableBy.ofIso,
corepresentableBy₂, Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢
simp only [whiskerRight_tensor, id_whiskerRight, Category.id_comp, Iso.inv_hom_id] at this
simp only [this]
simp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity]
