instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms

English

If f is mono in the image of F and F reflects monos, then the adjunction-induced map adj.homEquiv X Y f is mono.

Русский

Если f моно в образе F и F отражает мономорфизмы, то отображение adj.homEquiv является моно.

LaTeX

$$$$ \\operatorname{Mono}(f) \\land \\mathrm{ReflectsMonomorphisms}(F) \\Rightarrow \\operatorname{Mono}(\\operatorname{adj.homEquiv}(X,Y,f)). $$$$

Lean4

instance (adj : F ⊣ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) [hf : Mono f] [F.ReflectsMonomorphisms] :
    Mono (adj.homEquiv _ _ f) :=
  F.mono_of_mono_map <| by
    rw [← (homEquiv adj X Y).symm_apply_apply f] at hf
    exact mono_of_mono_fac (adj.homEquiv_counit _ _ _).symm

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