generate_map_eq_functorPushforward

English

For presheaves and maps, generate (Presieve.map F s) equals functorPushforward F (generate s).

Русский

Для отображения presieve через F порождение равно functorPushforward F (generate s).

LaTeX

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

Lean4

theorem generate_map_eq_functorPushforward {s : Presieve X} : generate (s.map F) = (generate s).functorPushforward F :=
  by
  ext
  rw [arrows_generate_map_eq_functorPushforward]
  simp [functorPushforward_extend_eq]

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