natTransOfWhiskerLeftInlInr_comp — Mathlib

English

Composition distributes over the whisker construction: composing inl/inr whiskers commutes with the whisker of sums.

Русский

Сложение через whiskerLeftInlInr композиционно распределяется: композиция через inl/inr совместима с whiskerLeft для суммы.

LaTeX

$$natTransOfWhiskerLeftInlInr (η₁ ≫ ν₁) (η₂ ≫ ν₂) = natTransOfWhiskerLeftInlInr η₁ η₂ ≫ natTransOfWhiskerLeftInlInr ν₁ ν₂$$

Lean4

@[simp]
theorem natTransOfWhiskerLeftInlInr_comp {F G H : A ⊕ A' ⥤ B} (η₁ : Sum.inl_ A A' ⋙ F ⟶ Sum.inl_ A A' ⋙ G)
    (η₂ : Sum.inr_ A A' ⋙ F ⟶ Sum.inr_ A A' ⋙ G) (ν₁ : Sum.inl_ A A' ⋙ G ⟶ Sum.inl_ A A' ⋙ H)
    (ν₂ : Sum.inr_ A A' ⋙ G ⟶ Sum.inr_ A A' ⋙ H) :
    natTransOfWhiskerLeftInlInr (η₁ ≫ ν₁) (η₂ ≫ ν₂) =
      natTransOfWhiskerLeftInlInr η₁ η₂ ≫ natTransOfWhiskerLeftInlInr ν₁ ν₂ :=
  by cat_disch

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