equalizerCone

Mathlib.CategoryTheory.Limits.Constructions.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone

Lean4

/-- Define the equalizing cone -/
abbrev equalizerCone (F : WalkingParallelPair ⥤ C) : Cone F :=
  Cone.ofFork
    (Fork.ofι (pullbackFst F)
      (by
        conv_rhs => rw [pullbackFst_eq_pullback_snd]
        convert
            (eq_whisker pullback.condition Limits.prod.snd :
              (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
            1 <;>
          simp))

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

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

Разделы

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

Аффилиация

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