hom_snd — Mathlib

English

The inverse of the diagonal map iso satisfies dual identities with snd morphisms, expressing how the inverse interacts with snd and diags in the pullback diagram.

Русский

Обратное диагонального отображения удовлетворяет двойственным отношениям с snd-морфизмами, показывая, как обратное взаимодействует с snd и диагоналями в диаграмме предела.

LaTeX

$$$$ (pullbackDiagonalMapIso\ f\ i\ i_1\ i_2)^{−1} \;\circ\; snd\_{i_1,i_2} \;\circ\; snd = snd $$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_snd : (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.snd _ _ :=
  by
  delta pullbackDiagonalMapIso
  simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

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