preimage

Mathlib.CategoryTheory.Subpresheaf.Image

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

Lean4

/-- The preimage of a subpresheaf by a morphism of presheaves of types. -/
@[simps]
def preimage (G : Subpresheaf F) (p : F' ⟶ F) : Subpresheaf F'
    where
  obj n := p.app n ⁻¹' (G.obj n)
  map
    f :=
    (Set.preimage_mono (G.map f)).trans
      (by
        simp only [Set.preimage_preimage, FunctorToTypes.naturality _ _ p f]
        rfl)

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

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

Разделы

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

Аффилиация

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