hom

Mathlib.CategoryTheory.Limits.Shapes.Diagonal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.pullbackDiagonalMapIso.hom

Lean4

/-- The underlying map of `pullbackDiagonalIso` -/
abbrev hom :
    pullback (diagonal f)
        (map (i₁ ≫ snd _ _) (i₂ ≫ snd _ _) f f (i₁ ≫ fst _ _) (i₂ ≫ fst _ _) i
          (by simp only [Category.assoc, condition]) (by simp only [Category.assoc, condition])) ⟶
      pullback i₁ i₂ :=
  pullback.lift (pullback.snd _ _ ≫ pullback.fst _ _) (pullback.snd _ _ ≫ pullback.snd _ _)
    (by
      ext
      · simp only [Category.assoc, pullback_diagonal_map_snd_fst_fst, pullback_diagonal_map_snd_snd_fst]
      · simp only [Category.assoc, condition])

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

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

Разделы

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

Аффилиация

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