equalizerFork

Mathlib.Algebra.Category.Ring.Under.Limits

URI: https://scilib.ai/kg/mathlib#CommRingCat.Under.equalizerFork

Lean4

/-- The canonical fork on `f g : A ⟶ B` given by the equalizer. -/
def equalizerFork {A B : Under R} (f g : A ⟶ B) : Fork f g :=
  Fork.ofι ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder) (by rw [equalizer_comp])

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

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

Разделы

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

Аффилиация

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