projective_iff_preservesEpimorphisms_coyoneda_obj

English

A object P is projective if and only if coyoneda.obj(op P) preserves epimorphisms.

Русский

Объект P проективен тогда и только тогда, когда coyoneda.obj(op P) сохраняет эпиморфизмы.

LaTeX

$$$ \\text{Projective}(P) \\;\\longleftrightarrow\\; (\\mathrm{coyoneda} \\cdot \\mathrm{obj}(\\mathrm{op}\\,P)).\\mathrm{PreservesEpimorphisms} $$$

Lean4

theorem projective_iff_preservesEpimorphisms_coyoneda_obj (P : C) :
    Projective P ↔ (coyoneda.obj (op P)).PreservesEpimorphisms :=
  ⟨fun hP =>
    ⟨fun f _ =>
      (epi_iff_surjective _).2 fun g =>
        have : Projective (unop (op P)) := hP
        ⟨factorThru g f, factorThru_comp _ _⟩⟩,
    fun _ => ⟨fun f e _ => (epi_iff_surjective _).1 (inferInstance : Epi ((coyoneda.obj (op P)).map e)) f⟩⟩

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