factorThru_self

Mathlib.CategoryTheory.Subobject.FactorThru

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

English

For any P, P.Factors P.arrow holds, i.e., the identity factorization exists through its own arrow.

Русский

Для любого подобъекта P верно P.Factors P.arrow, существует факторизация через собственную стрелку.

LaTeX

$$P.Factors P.arrow$$

Lean4

@[simp]
theorem factorThru_self {X : C} (P : Subobject X) (h) : P.factorThru P.arrow h = 𝟙 (P : C) :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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