preservesMonomorphisms_of_preserves_of_reflects

English

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

Русский

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

LaTeX

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

Lean4

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

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