fork_ι

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

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

English

The iso of diagrams is compatible with iso of presheaves via Pi.mapIso on each coordinate.

Русский

Изоморфизм диаграмм совместим с изоморфизмом преп presheaf по координатам через Pi.mapIso.

LaTeX

$$$\mathrm{diagram}.\mathrm{isoOfIso}(F,U) = \Pi\mathrm{mapIso}(\lambda i.\alpha_i)$$$

Lean4

@[simp]
theorem fork_ι : (fork F U).ι = res F U :=
  rfl

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

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

Разделы

Аффилиация

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