image_mem_functorPushforward

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.image_mem_functorPushforward

English

If f ∈ R, then the image under F of f belongs to the pushforward presieve R.functorPushforward F.

Русский

Если f ∈ R, то образ f через F принадлежит предсистеме pushforward R.functorPushforward F.

LaTeX

$$$F.map f \\in R.functorPushforward F$ whenever $f \\in R$$$

Lean4

theorem image_mem_functorPushforward (R : Presieve X) {f : Y ⟶ X} (h : R f) : R.functorPushforward F (F.map f) :=
  ⟨Y, f, 𝟙 _, h, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru