mapWhisker_exchange — Mathlib

English

One can interchange mapWhiskerLeft and mapWhiskerRight with suitable arguments.

Русский

Можно поменять местами mapWhiskerLeft и mapWhiskerRight с подходящими аргументами.

LaTeX

$$$ mapWhiskerLeft F α \;\circ\; mapWhiskerRight β G = mapWhiskerRight α F \;\circ\; mapWhiskerLeft G β $$$

Lean4

/-- One can exchange `mapWhiskerLeft` and `mapWhiskerRight`. -/
theorem mapWhisker_exchange (Fₗ : C ⥤ E) (Gₗ : C ⥤ E) (Fᵣ : D ⥤ E') (Gᵣ : D ⥤ E') (αₗ : Fₗ ⟶ Gₗ) (αᵣ : Fᵣ ⟶ Gᵣ) :
    mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ = mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ :=
  by
  ext
  cat_disch

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