faithful_whiskeringLeft

Mathlib.CategoryTheory.Localization.Predicate

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.faithful_whiskeringLeft

← MathLib Explorer

English

The whiskeringLeft functor is faithful.

Русский

WhiskeringLeft обладает свойством Faithful.

LaTeX

$$$$\\text{Faithful}((\\text{Functor.whiskeringLeft})\\, L)$$$$

Lean4

theorem faithful_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*) [Category E] :
    ((whiskeringLeft C D E).obj L).Faithful :=
  inferInstanceAs (whiskeringLeftFunctor' L W E).Faithful

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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