projectivePresentationOfMapProjectivePresentation

Mathlib.CategoryTheory.Preadditive.Projective.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation

Lean4

/-- Given an equivalence of categories `F`, a projective presentation of `F(X)` induces a
projective presentation of `X.` -/
def projectivePresentationOfMapProjectivePresentation (X : C) (Y : ProjectivePresentation (F.functor.obj X)) :
    ProjectivePresentation X where
  p := F.inverse.obj Y.p
  projective := Adjunction.map_projective F.symm.toAdjunction Y.p Y.projective
  f := F.inverse.map Y.f ≫ F.unitInv.app _
  epi := epi_comp _ _

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

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

Разделы

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

Аффилиация

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