FirstObj

Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equalizer.FirstObj

Lean4

/-- The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram
of the Stacks entry.
-/
@[stacks 00VM "This is the middle object of the fork diagram there."]
def FirstObj : Type max v u :=
  ∏ᶜ fun f : Σ Y, { f : Y ⟶ X // R f } => P.obj (op f.1)

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

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

Разделы

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

Аффилиация

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