reflectsMonomorphisms_of_preserves_of_reflects

English

If F preserves monomorphisms and F ∘ G reflects monomorphisms, then F reflects monomorphisms.

Русский

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

LaTeX

$$((PreservesMonomorphisms G) ∧ (ReflectsMonomorphisms (F \circ G))) ⇒ ReflectsMonomorphisms F$$

Lean4

theorem reflectsMonomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E) [PreservesMonomorphisms G]
    [ReflectsMonomorphisms (F ⋙ G)] : ReflectsMonomorphisms F :=
  ⟨fun f _ => (F ⋙ G).mono_of_mono_map <| show Mono (G.map (F.map f)) from inferInstance⟩

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