instWhiskerVerticalOfIsIsoFunctor

Mathlib.CategoryTheory.GuitartExact.VerticalComposition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.TwoSquare.GuitartExact.instWhiskerVerticalOfIsIsoFunctor

← MathLib Explorer

English

If α, β are isomorphisms, then (w.whiskerVertical α.hom β.inv) is GuitartExact.

Русский

Если α и β — изоморфизмы, то (w.whiskerVertical α.hom β.inv) точен по Гитхарту.

LaTeX

$$$\mathrm{GuitartExact}(w.whiskerVertical\, α.hom\, β.inv)$$$

Lean4

instance [w.GuitartExact] (α : L ⟶ L') (β : R' ⟶ R) [IsIso α] [IsIso β] : (w.whiskerVertical α β).GuitartExact :=
  whiskerVertical w (asIso α) (asIso β).symm

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

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

Разделы

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

Аффилиация

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