image

Mathlib.CategoryTheory.Subpresheaf.Image

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.image

Lean4

/-- The image of a subpresheaf by a morphism of presheaves of types. -/
@[simps]
def image : Subpresheaf F' where
  obj i := (f.app i) '' (G.obj i)
  map := by
    rintro Δ Δ' φ _ ⟨x, hx, rfl⟩
    exact ⟨F.map φ x, G.map φ hx, by apply FunctorToTypes.naturality⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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