pullbackFst_eq_pullback_snd — Mathlib

English

In a construction showing equalizers from pullbacks and binary products, pullback_fst coincides with pullback_snd.

Русский

В конструкциях, связывающих равносильности через pullback и бинарные произведения, проекция pullback_fst совпадает с pullback_snd.

LaTeX

$$$\\text{pullbackFst }F = \\text{pullbackSnd }F$$$

Lean4

theorem pullbackFst_eq_pullback_snd (F : WalkingParallelPair ⥤ C) : pullbackFst F = pullback.snd _ _ := by
  convert
      (eq_whisker pullback.condition Limits.prod.fst :
        (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _) <;>
    simp

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