preservesEpimorphisms_of_preserves_of_reflects

English

If the composite F ∘ G preserves epimorphisms and G reflects epimorphisms, then F preserves epimorphisms.

Русский

Если композиция F ∘ G сохраняет эпиморфизмы и G отражает эпиморфизмы, то F сохраняет эпиморфизмы.

LaTeX

$$$(PreservesEpimorphisms(F \circ G)) \land (ReflectsEpimorphisms(G)) \Rightarrow PreservesEpimorphisms(F)$$$

Lean4

theorem preservesEpimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E) [PreservesEpimorphisms (F ⋙ G)]
    [ReflectsEpimorphisms G] : PreservesEpimorphisms F :=
  ⟨fun f _ => G.epi_of_epi_map <| show Epi ((F ⋙ G).map f) from inferInstance⟩

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