instFaithfulSigmaIncl

Mathlib.CategoryTheory.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sigma.instFaithfulSigmaIncl

English

For each i ∈ I, incl_i: C_i ⥤ Σ i, C_i is a faithful functor.

Русский

Для каждого i ∈ I включение incl_i: C_i → Σ i, C_i является точной ( верной ) функторной связью.

LaTeX

$$$ \mathrm{incl}_i \text{ is faithful}. $$$

Lean4

instance (i : I) : Functor.Faithful (incl i : C i ⥤ Σ i, C i) where map_injective {_ _ _ _} h := by injection h

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

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

Разделы

Аффилиация

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