pushoutInl_eq_pushout_inr — Mathlib

English

Let F be any diagram of a parallel pair in a category C. Then the left pushout leg is equal to the right pushout leg, i.e. the two canonical arrows from the common source to the pushout coincide.

Русский

Пусть F — диаграмма параллельной пары в категории C. Тогда левая ножка пуш-аута равна правой, то есть две канонические стрелки из общей области в пуш-аут совпадают.

LaTeX

$$$\operatorname{pushoutInl}(F) = \operatorname{pushout.inr} \,\_\_\,$$$

Lean4

theorem pushoutInl_eq_pushout_inr (F : WalkingParallelPair ⥤ C) : pushoutInl F = pushout.inr _ _ := by
  convert (whisker_eq Limits.coprod.inl pushout.condition : (_ : F.obj _ ⟶ constructCoequalizer _) = _) <;> simp

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