plusMap_id

Mathlib.CategoryTheory.Sites.Plus

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

← MathLib Explorer

English

The plus-map of the identity morphism is the identity on the plusObj.

Русский

Плюс-карта от тождества равна тождественному отображению на плюсObj.

LaTeX

$$$J.plusMap(\\mathrm{id}\\ P) = \\mathrm{id}_{J.plusObj P}$$$

Lean4

@[simp]
theorem plusMap_id (P : Cᵒᵖ ⥤ D) : J.plusMap (𝟙 P) = 𝟙 _ :=
  by
  ext : 2
  dsimp only [plusMap, plusObj]
  rw [J.diagramNatTrans_id, NatTrans.id_app]
  ext
  simp

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

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

Разделы

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

Аффилиация

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