instFaithfulFiberInclusion

Mathlib.CategoryTheory.FiberedCategory.Fiber

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Fiber.instFaithfulFiberInclusion

English

If α is a morphism of BasedNatTrans and α.toNatTrans is an isomorphism, then α itself is an isomorphism.

Русский

Если тождество между BasedNatTrans имеет изоморфизм своей основы, то само преобразование является изоморфизмом.

LaTeX

$$$\\text{IsIso }\\alpha$$$

Lean4

instance : (fiberInclusion : Fiber p S ⥤ _).Faithful where

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

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

Разделы

Аффилиация

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