instFaithfulFibι

Mathlib.CategoryTheory.FiberedCategory.HasFibers

URI: https://scilib.ai/kg/mathlib#HasFibers.instFaithfulFibι

English

The induced functor on fibers is an equivalence.

Русский

Индуцированный функтор на фибрах является эквивалентностью.

LaTeX

$$$\\text{HasFibers.}\\text{inducedFunctor } p S \\text{ is an equivalence}$$$

Lean4

instance : Functor.Faithful (ι (p := p) S) :=
  Functor.Faithful.of_iso (inducedFunctor.natIso p S).symm

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

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

Разделы

Аффилиация

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