instMonoFunctorWhiskerRightOfPreservesMonomorphisms

English

If f is mono and H preserves monomorphisms, then whiskerRight f H is mono.

Русский

Если f — моно, и H сохраняет мономорфизмы, тогда whiskerRight f H также моно.

LaTeX

$$$[\\text{Mono } f] \\Rightarrow \\operatorname{Mono}(\\mathrm{whiskerRight}\, f\, H).$$$

Lean4

instance [Mono f] (H : C ⥤ D) [H.PreservesMonomorphisms] : Mono (whiskerRight f H) :=
  by
  have : ∀ X, Mono ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
  apply NatTrans.mono_of_mono_app

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