underlyingIso_inv_top_arrow

Mathlib.CategoryTheory.Subobject.Lattice

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.underlyingIso_inv_top_arrow

← MathLib Explorer

English

For any object A,B and morphism f: A → B, the top subobject of B factors f.

Русский

Для любогоA,B и морфизма f: A → B верхний подпредмет B факторизуется через f.

LaTeX

$$$(\top : \operatorname{Subobject} B).Factors f$$$

Lean4

@[reassoc (attr := simp)]
theorem underlyingIso_inv_top_arrow {B : C} : (underlyingIso _).inv ≫ (⊤ : Subobject B).arrow = 𝟙 B :=
  underlyingIso_arrow _

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

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

Разделы

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

Аффилиация

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