map_projective — Mathlib

English

Let adj be an adjunction F ⊣ G with G preserving epimorphisms. If P is a projective object in C, then F.obj P is projective in D.

Русский

Пусть adj — тождество F ⊣ G с тем, что G сохраняет эпиморфизмы. Если P проективен в C, то F.obj P проективен в D.

LaTeX

$$$ (\\forall P)\\ (\\mathrm{Projective}(P) \\Rightarrow \\mathrm{Projective}(F\\!.(P))) \\quad \\text{under } F \\dashv G \\text{ and } G \\text{ preserves epimorphisms}. $$$

Lean4

theorem map_projective (adj : F ⊣ G) [G.PreservesEpimorphisms] (P : C) (hP : Projective P) : Projective (F.obj P) where
  factors f g
    _ := by
    rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩
    use F.map f' ≫ adj.counit.app _
    rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']
    simp

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