isoPullback_hom_snd — Mathlib

English

The canonical morphism from the pullback to Y via the pullback isos sends via snd to snd.

Русский

Канонический морфизм из предела к Y через пределы идёт к snd.

LaTeX

$$$ h.isoPullback.hom \circ pullback.snd f g = snd $$$

Lean4

@[reassoc (attr := simp)]
theorem isoPullback_hom_snd (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.hom ≫ pullback.snd _ _ = snd :=
  by
  dsimp [isoPullback, cone, CommSq.cone]
  simp

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