ofIso

Mathlib.CategoryTheory.Yoneda

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

Lean4

/-- If `F ≅ F'`, and `F` is corepresentable, then `F'` is corepresentable. -/
def ofIso {F F' : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) (e' : F ≅ F') : F'.CorepresentableBy X
    where
  homEquiv {X} := e.homEquiv.trans (e'.app _).toEquiv
  homEquiv_comp {Y Y'} g
    f := by
    dsimp
    rw [e.homEquiv_comp]
    apply congr_fun (e'.hom.naturality g)

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

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

Разделы

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

Аффилиация

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