map₁_id

Mathlib.CategoryTheory.Comma.Presheaf.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.OverPresheafAux.YonedaCollection.map₁_id

English

Applying map₂ with identity yields the identity transformation on YonedaCollection.

Русский

Применение map₂ к идентичности даёт тождественный переход на YonedaCollection.

LaTeX

$$$\\forall X\\; {A : C^op \\to Type_v},\\; YonedaCollection.map₂ F (id X) = id$$$

Lean4

@[simp]
theorem map₁_id : YonedaCollection.map₁ (𝟙 F) (X := X) = id := by cat_disch

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

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

Разделы

Аффилиация

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