functorPullback_pullback — Mathlib

English

For any functor F and X, the generate of the map of a presieve under F equals the functorPushforward of the generate presieve: generate (s.map F) = (generate s).functorPushforward F.

Русский

Порождение отображения presieve через F равно functorPushforward от порождения: generate (s.map F) = (generate s).functorPushforward F.

LaTeX

$$$ \\mathrm{generate}(\\mathrm{Presieve}.map F\\, s) = (\\mathrm{generate}\\, s).\\mathrm{functorPushforward}\\, F $$$

Lean4

theorem functorPullback_pullback {X Y : C} (f : X ⟶ Y) (S : Sieve (F.obj Y)) :
    functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S) :=
  by
  ext
  simp

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