mapProjectivePresentation

Mathlib.CategoryTheory.Preadditive.Projective.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.mapProjectivePresentation

Lean4

/-- Given an adjunction `F ⊣ G` such that `G` preserves epis, `F` maps a projective presentation of
`X` to a projective presentation of `F(X)`. -/
def mapProjectivePresentation (adj : F ⊣ G) [G.PreservesEpimorphisms] (X : C) (Y : ProjectivePresentation X) :
    ProjectivePresentation (F.obj X) where
  p := F.obj Y.p
  projective := adj.map_projective _ Y.projective
  f := F.map Y.f
  epi :=
    have := Adjunction.leftAdjoint_preservesColimits.{0, 0} adj;
    inferInstance

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

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

Разделы

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

Аффилиация

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