sheafifyLift

Mathlib.CategoryTheory.Sites.Sheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.sheafifyLift

Lean4

/-- Given a sheaf `Q` and a morphism `P ⟶ Q`, construct a morphism from `sheafify J P` to `Q`. -/
noncomputable def sheafifyLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) : sheafify J P ⟶ Q :=
  (sheafificationAdjunction J D).homEquiv P ⟨Q, hQ⟩ |>.symm η |>.val

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

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

Разделы

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

Аффилиация

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