top_factors

Mathlib.CategoryTheory.Subobject.Lattice

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

English

Any morphism f factors through the top subobject of its codomain.

Русский

Любой морфизм f факторирует через верхний подпредмет своей кодоморфной области.

LaTeX

$$$\\text{top}.Factors\\, f$$$

Lean4

theorem top_factors {A B : C} (f : A ⟶ B) : (⊤ : Subobject B).Factors f :=
  ⟨f, comp_id _⟩

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

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

Разделы

Аффилиация

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