English
A diagonal pullback identity expresses how the pullback along the diagonal interacts with the fst projection in a pullback square, giving a canonical isomorphism.
Русский
Идентичность диагонального предела выражает, как предельный по диагонали взаимодействует с проекцией fst в квадрате предела, задавая каноническую изоморфизм.
LaTeX
$$$$ diagonal_pullback_fst \;: \; diagonal (pullback.fst f g) = pullbackSymmetry (f,g).hom \circ (Over.pullback f).map (diagonal g) $$$$
Lean4
/-- The diagonal object of `X ×[Z] Y ⟶ X` is isomorphic to `Δ_{Y/Z} ×[Z] X`. -/
def diagonalObjPullbackFstIso {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
diagonalObj (pullback.fst f g) ≅ pullback (pullback.snd _ _ ≫ g : diagonalObj g ⟶ Z) f :=
pullbackRightPullbackFstIso _ _ _ ≪≫
pullback.congrHom pullback.condition rfl ≪≫
pullbackAssoc _ _ _ _ ≪≫ pullbackSymmetry _ _ ≪≫ pullback.congrHom pullback.condition rfl
