isoToPlus_inv

Mathlib.CategoryTheory.Sites.Plus

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.isoToPlus_inv

Lean4

@[simp]
theorem isoToPlus_inv (hP : Presheaf.IsSheaf J P) : (J.isoToPlus P hP).inv = J.plusLift (𝟙 _) hP :=
  by
  apply J.plusLift_unique
  rw [Iso.comp_inv_eq, Category.id_comp]
  rfl

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

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

Разделы

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

Аффилиация

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