instIsEquivalenceFibFiberInducedFunctor

Mathlib.CategoryTheory.FiberedCategory.HasFibers

URI: https://scilib.ai/kg/mathlib#HasFibers.instIsEquivalenceFibFiberInducedFunctor

English

The induced functor is faithful; the forgetful inverse is faithful via an iso.

Русский

Индуцированный функтор является верным; обратный забывающий через изоморфизм верен.

LaTeX

$$$\\text{inducedFunctor}\\,p\\,S\\text{ is faithful}$$$

Lean4

instance : Functor.IsEquivalence (inducedFunctor p S) :=
  equiv S

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

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

Разделы

Аффилиация

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