inv_hom_id_left

Mathlib.CategoryTheory.Comma.Arrow

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.inv_hom_id_left

English

If sq : f ⟶ g is an isomorphism, IsIso f.hom ↔ IsIso g.hom.

Русский

Если sq : f ⟶ g является изоморфизмом, то IsIso f.hom ↔ IsIso g.hom.

LaTeX

$$$\text{IsIso}(f.hom) \iff \text{IsIso}(g.hom)$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_hom_id_left (e : f ≅ g) : e.inv.left ≫ e.hom.left = 𝟙 _ := by rw [← comp_left, e.inv_hom_id, id_left]

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

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

Разделы

Аффилиация

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