English
A natural transformation from the left and right whiskerings induces a natural transformation between the original functors.
Русский
Естественное преобразование между левой и правой обёртками индуцирует естественное преобразование между исходными функторными
LaTeX
$$natTransOfWhiskerLeftInlInr {F G : A ⊕ A' ⥤ B} (η₁ : Sum.inl_ A A' ⋙ F ⟶ Sum.inl_ A A' ⋙ G) (η₂ : Sum.inr_ A A' ⋙ F ⟶ Sum.inr_ A A' ⋙ G) : F ⟶ G$$
Lean4
/-- A consequence of `functorEquiv`: we can construct a natural transformation of functors
`A ⊕ A' ⥤ B` from the data of natural transformations of their whiskering with `inl_` and `inr_`. -/
@[simps!]
def natTransOfWhiskerLeftInlInr {F G : A ⊕ A' ⥤ B} (η₁ : Sum.inl_ A A' ⋙ F ⟶ Sum.inl_ A A' ⋙ G)
(η₂ : Sum.inr_ A A' ⋙ F ⟶ Sum.inr_ A A' ⋙ G) : F ⟶ G :=
(Sum.functorEquiv A A' B).unit.app F ≫
(Sum.functorEquiv A A' B).inverse.map ((η₁, η₂) :) ≫ (Sum.functorEquiv A A' B).unitInv.app G
