whiskeringLeft_obj_preimage_app — Mathlib

English

For τ and P, the app of the preimage under whiskeringLeft equals F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p.

Русский

Для τ и P, значение на приложении предварительного образа под whiskeringLeft равно F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p.

LaTeX

$$whiskeringLeft_obj_preimage_app {F G : Karoubi C ⥤ D} (τ : toKaroubi _ ⋙ F ⟶ toKaroubi _ ⋙ G) (P : Karoubi C) :\n (((whiskeringLeft _ _ _).obj (toKaroubi _)).preimage τ).app P =\n F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p$$

Lean4

theorem whiskeringLeft_obj_preimage_app {F G : Karoubi C ⥤ D} (τ : toKaroubi _ ⋙ F ⟶ toKaroubi _ ⋙ G) (P : Karoubi C) :
    (((whiskeringLeft _ _ _).obj (toKaroubi _)).preimage τ).app P =
      F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p :=
  by
  rw [natTrans_eq]
  congr 2
  rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).map_preimage τ) P.X]
  dsimp
  congr

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