natIsoOfWhiskerLeftInlInr — Mathlib

English

Given left and right whisker isomorphisms, there is a canonical isomorphism F ≅ G.

Русский

Даны изоморфизмы слева и справа, существует каноническое изоморфизм F ≅ G.

LaTeX

$$natIsoOfWhiskerLeftInlInr η₁ η₂ : F ≅ G$$

Lean4

/-- A consequence of `functorEquiv`: we can construct a natural isomorphism of functors
`A ⊕ A' ⥤ B` from the data of natural isomorphisms of their whiskering with `inl_` and `inr_`. -/
@[simps]
def natIsoOfWhiskerLeftInlInr {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
    where
  hom := natTransOfWhiskerLeftInlInr η₁.hom η₂.hom
  inv := natTransOfWhiskerLeftInlInr η₁.inv η₂.inv

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