diagonal_isKernelPair

Mathlib.CategoryTheory.Limits.Shapes.Diagonal

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

← MathLib Explorer

English

The two projections form a kernel pair for f: X → Y.

Русский

Две проекции образуют пару ядра для отображения f: X → Y.

LaTeX

$$$ \\ IsKernelPair( f, \\text{pullback.fst}(f,f), \\text{pullback.snd}(f,f) ). $$$

Lean4

/-- The two projections `Δ_{X/Y} ⟶ X` form a kernel pair for `f : X ⟶ Y`. -/
theorem diagonal_isKernelPair : IsKernelPair f (pullback.fst f f) (pullback.snd f f) :=
  IsPullback.of_hasPullback f f

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

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

Разделы

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

Аффилиация

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