instIsIsoHomHomCone

Mathlib.CategoryTheory.Limits.Cones

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.instIsIsoHomHomCone

English

If f is an isomorphism of cones, then its hom component f.hom is an isomorphism in the base category.

Русский

Если f — изоморфизм конуса, то компонента гомоморфизма f.hom является изоморфизмом в базовой категории.

LaTeX

$$IsIso(f.hom.hom)$$

Lean4

instance {c d : Cone F} (f : c ≅ d) : IsIso f.hom.hom :=
  ⟨f.inv.hom, by simp⟩

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

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

Разделы

Аффилиация

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