inducedFunctorOfEquiv

Mathlib.CategoryTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.inducedFunctorOfEquiv

English

If e: C' ≃ D is an equivalence, then the induced functor inducedFunctor e is an equivalence.

Русский

Если e: C' ≃ D — эквивалентность, то индуцированный функтор inducedFunctor e является эквивалентностью.

LaTeX

$$$(\mathrm{inducedFunctor}(e)).IsEquivalence$$$

Lean4

noncomputable instance inducedFunctorOfEquiv {C' : Type*} (e : C' ≃ D) : IsEquivalence (inducedFunctor e) where

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

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

Разделы

Аффилиация

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