instFullSheafSheafComposeOfFaithful

English

If F is faithful and full, then the functor (sheafCompose J F) is full, and hence full when composed with the forgetful functor.

Русский

Если F верен и полно, то (sheafCompose J F) полно, и поэтому полно после забывания.

LaTeX

$$$\mathrm{Full}\big( \mathrm{sheafCompose}\, J\, F \big)$$$

Lean4

instance [F.Full] [F.Faithful] : (sheafCompose J F).Full :=
  Functor.Full.of_comp_faithful (sheafCompose J F) (sheafToPresheaf _ _)

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