fromPreimage

Mathlib.CategoryTheory.Subpresheaf.Image

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

Lean4

/-- Given a morphism `p : F' ⟶ F` of presheaves of types and `G : Subpresheaf F`,
this is the morphism from the preimage of `G` by `p` to `G`. -/
def fromPreimage (G : Subpresheaf F) (p : F' ⟶ F) : (G.preimage p).toPresheaf ⟶ G.toPresheaf :=
  lift ((G.preimage p).ι ≫ p) (by rw [range_comp, range_ι, image_le_iff])

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

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

Разделы

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

Аффилиация

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