coev_naturality

Mathlib.CategoryTheory.Closed.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ihom.coev_naturality

← MathLib Explorer

English

Another instance of naturality of ev in the setting of ihom, same content as above.

Русский

Ещё одна форма естественности_ev в рамках ihom.

LaTeX

$$$ f \\;\\mapsto\\; (ev A)^{-1} \\circ f $$$

Lean4

@[reassoc (attr := simp)]
theorem coev_naturality {X Y : C} (f : X ⟶ Y) : f ≫ (coev A).app Y = (coev A).app X ≫ (ihom A).map (A ◁ f) :=
  (coev A).naturality f

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

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

Разделы

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

Аффилиация

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