transportIso

Mathlib.CategoryTheory.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Grothendieck.transportIso

Lean4

/-- If `F : C ⥤ Cat` and `x : Grothendieck F`, then every `C`-isomorphism `α : x.base ≅ c` induces
an isomorphism between `x` and its transport along `α`
-/
@[simps!]
def transportIso (x : Grothendieck F) {c : C} (α : x.base ≅ c) : x.transport α.hom ≅ x :=
  (isoMk α (Iso.refl _)).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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