map_projective_iff — Mathlib

English

For an equivalence F : C ≌ D, a object P in C is projective iff F.obj P is projective in D.

Русский

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

LaTeX

$$$ P \\in \\mathrm{Obj}(C):\\ \\mathrm{Projective}(F.\\mathrm{functor}.\\mathrm{obj}(P)) \\iff \\mathrm{Projective}(P). $$$

Lean4

theorem map_projective_iff (P : C) : Projective (F.functor.obj P) ↔ Projective P :=
  ⟨F.toAdjunction.projective_of_map_projective P, F.toAdjunction.map_projective P⟩

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