hom_inv_id_assoc

Mathlib.CategoryTheory.Iso

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

English

For any X → Y morphism f with IsIso, and any Z map g: X → Z, we have (f ≫ inv f) ≫ g = g.

Русский

Для любого морфизма f: X → Y с IsIso и любого g: X → Z имеем (f ≫ inv f) ≫ g = g.

LaTeX

$$$f \circ f^{-1} \circ g = g$$$

Lean4

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

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

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

Разделы

Аффилиация

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