instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf

English

Let F : A ⥤ B be a faithful functor. Then the composite functor (sheafCompose J F) followed by the forgetful functor to presheaves is faithful.

Русский

Пусть F : A ⥤ B — верный функтор. Тогда композиция (sheafCompose J F) с последующим забыванием к прешейфам верна (faithful).

LaTeX

$$$\mathrm{Faithful}\big( \mathrm{sheafToPresheaf} \circ \mathrm{sheafCompose}\, J\, F \big)$$$

Lean4

instance [F.Faithful] : (sheafCompose J F ⋙ sheafToPresheaf _ _).Faithful :=
  show (sheafToPresheaf _ _ ⋙ (whiskeringRight Cᵒᵖ A B).obj F).Faithful from inferInstance

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