reflectsMonomorphisms_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance reflectsMonomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [ReflectsMonomorphisms F] [ReflectsMonomorphisms G] :
    ReflectsMonomorphisms (F ⋙ G) where reflects _ h := F.mono_of_mono_map (G.mono_of_mono_map h)

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