instFaithfulSheafSheafCompose

Mathlib.CategoryTheory.Sites.Whiskering

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instFaithfulSheafSheafCompose

English

If F is faithful, then the functor (sheafCompose J F) is faithful.

Русский

Если F верен, то функтор (sheafCompose J F) верен.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru