diagram

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.SheafConditionEqualizerProducts.diagram

English

The apex of the fork is F.obj(op(iSup U)).

Русский

Апекс форка равен F(оп(объединение U)).

LaTeX

$$$\mathrm{fork}(F,U).\mathrm{pt} = F(\mathrm{op}(\bigvee U)).$$$

Lean4

/-- The equalizer diagram for the sheaf condition.
-/
abbrev diagram : WalkingParallelPair ⥤ C :=
  parallelPair (leftRes.{v'} F U) (rightRes F U)

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

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

Разделы

Аффилиация

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