inv_hom_id_assoc

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.inv_hom_id_assoc

English

For an isomorphism e: X ≅ Y, the morphism e.hom is itself an isomorphism.

Русский

У изоморфизма e: X ≅ Y морфизм e.hom является изоморфизмом.

LaTeX

$$IsIso e.hom$$

Lean4

@[simp]
theorem inv_hom_id_assoc (f : X ⟶ Y) [I : IsIso f] {Z} (g : Y ⟶ Z) : inv f ≫ f ≫ g = g := by simp [← Category.assoc]

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

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

Разделы

Аффилиация

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