diagonal_snd

Mathlib.CategoryTheory.Limits.Shapes.Diagonal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.pullback.diagonal_snd

English

The composite diagonal f followed by pullback.snd is the identity on X.

Русский

Составная диагонали f с snd равна тождественному отображению на X.

LaTeX

$$$ \\text{diagonal}(f) \\; \\circ \\; \\text{pullback.snd}(f,f) = \\mathrm{id}_X. $$$

Lean4

@[reassoc (attr := simp)]
theorem diagonal_snd : diagonal f ≫ pullback.snd _ _ = 𝟙 _ :=
  pullback.lift_snd _ _ _

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

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

Разделы

Аффилиация

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