reflectsEpimorphisms_comp — Mathlib

English

Let F: C → D and G: D → E be functors that reflect epimorphisms. Then the composite F ∘ G reflects epimorphisms.

Русский

Пусть F: C → D и G: D → E — функторы, отражающие эпиморфизмы. Тогда композиция F ∘ G отражает эпиморфизмы.

LaTeX

$$$([ReflectsEpimorphisms F] \land [ReflectsEpimorphisms G]) \Rightarrow ReflectsEpimorphisms(F \circ G)$$$

Lean4

instance reflectsEpimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [ReflectsEpimorphisms F] [ReflectsEpimorphisms G] :
    ReflectsEpimorphisms (F ⋙ G) where reflects _ h := F.epi_of_epi_map (G.epi_of_epi_map h)

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