isSheaf_comp_uliftFunctor

Mathlib.CategoryTheory.Sites.SheafOfTypes

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

Lean4

/-- The composition of a sheaf with a ULift functor is still a sheaf. -/
theorem isSheaf_comp_uliftFunctor (h : IsSheaf J P) : IsSheaf J (P ⋙ uliftFunctor.{w'}) :=
  isSheaf_of_nat_equiv (fun _ => Equiv.ulift.symm) (fun _ _ _ _ => rfl) h

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

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

Разделы

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

Аффилиация

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