ι_π

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Sigma.ι_π

← MathLib Explorer

English

For f: β → C and HasProduct f, the equality Pi.ι f b ≫ Pi.π f b = id_{f(b)} holds for all b.

Русский

Для любого b верна тождественность Pi.ι f b ≫ Pi.π f b = id_{f(b)}.

LaTeX

$$Pi.ι f b ≫ Pi.π f b = id_{f(b)}$$

Lean4

@[reassoc]
theorem ι_π (b c : β) : Sigma.ι f b ≫ Sigma.π f c = if h : b = c then eqToHom (congrArg f h) else 0 :=
  by
  split_ifs with h
  · subst h; simp
  · simp [Sigma.ι_π_of_ne f h]

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

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

Разделы

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

Аффилиация

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