enoughProjectives_iff — Mathlib

English

For an equivalence F : C ≌ D, C has enough projectives iff D has enough projectives.

Русский

Для эквивалентности F : C ≌ D, C имеет достаточное количество проективных объектов тогда и только тогда, когда D имеет достаточное количество проективных объектов.

LaTeX

$$$ (\\mathrm{EnoughProjectives}(C)) \\iff (\\mathrm{EnoughProjectives}(D)) $ under F.$$

Lean4

theorem enoughProjectives_iff (F : C ≌ D) : EnoughProjectives C ↔ EnoughProjectives D :=
  by
  constructor
  all_goals intro H; constructor; intro X; constructor
  · exact F.symm.projectivePresentationOfMapProjectivePresentation _ (Nonempty.some (H.presentation (F.inverse.obj X)))
  · exact F.projectivePresentationOfMapProjectivePresentation X (Nonempty.some (H.presentation (F.functor.obj X)))

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