reprW_hom_app

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.reprW_hom_app

← MathLib Explorer

English

coreprW provides an isomorphism between coyoneda.obj(op F.coreprX) and F.

Русский

coreprW задаёт изоморфизм между coyoneda.obj(op F.coreprX) и F.

LaTeX

$$$ coyoneda.obj(\\operatorname{op} F.coreprX) \\cong F $$$

Lean4

theorem reprW_hom_app (F : Cᵒᵖ ⥤ Type v₁) [F.IsRepresentable] (X : Cᵒᵖ) (f : unop X ⟶ F.reprX) :
    F.reprW.hom.app X f = F.map f.op F.reprx := by apply RepresentableBy.homEquiv_eq

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

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

Разделы

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

Аффилиация

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