full_comp_preadditiveCoyonedaObj — Mathlib

English

If F is full, then the composite F ⋙ preadditiveCoyonedaObj G is full.

Русский

Если F полной, то композиция F ⋙ preadditiveCoyonedaObj G также полна.

LaTeX

$$$\text{Full}(F) \Rightarrow \text{Full}(F \circ \mathrm{preadditiveCoyonedaObj}\, G)$$$

Lean4

theorem full_comp_preadditiveCoyonedaObj [F.Full] {G : C} [Projective G] (hG : IsSeparator G)
    (hG₂ : ∀ X, ∃ (p : G ⟶ F.obj X), Epi p) : (F ⋙ preadditiveCoyonedaObj G).Full where
  map_surjective {X Y}
    f := by
    obtain ⟨p, _⟩ := hG₂ X
    obtain ⟨f, rfl⟩ := preadditiveCoyonedaObj_map_surjective hG p f
    obtain ⟨f, rfl⟩ := F.map_surjective f
    exact ⟨f, rfl⟩

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