natIsoOfWhiskerLeftInlInr_eq — Mathlib

English

Equality of whisker left-inl/inr natural isomorphisms corresponds to a standard decomposition via unit and mapIso.

Русский

Равенство изоморофических whiskerLeftInlInr соответствует стандартному разложению через единицу и mapIso.

LaTeX

$$natIsoOfWhiskerLeftInlInr η₁ η₂ = (Sum.functorEquiv A A' B).unitIso.app F ≪≫ ((Sum.functorEquiv A A' B).inverse.mapIso (Iso.prod η₁ η₂)) ≪≫ (Sum.functorEquiv A A' B).unitIso.symm.app G$$

Lean4

theorem natIsoOfWhiskerLeftInlInr_eq {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) :
    natIsoOfWhiskerLeftInlInr η₁ η₂ =
      (Sum.functorEquiv A A' B).unitIso.app _ ≪≫
        (Sum.functorEquiv A A' B).inverse.mapIso (Iso.prod η₁ η₂) ≪≫ (Sum.functorEquiv A A' B).unitIso.symm.app _ :=
  by cat_disch

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