pullbackRightPullbackFstIso_hom_snd

English

The isomorphism between the right-hand pullback cones commutes with the right leg, yielding a natural compatibility condition for the pasting of pullbacks.

Русский

Изоморфизм правого пулбэпа совместим с правой ножкой, обеспечивая естественную совместимость при склеивании пулбэпов.

LaTeX

$$$(\text{pullbackRightPullbackFstIso } f g f').hom \; ≫ \; \text{pullback.snd } _ _ = \text{pullback.snd } f' (\text{pullback.fst } f g) ≫ \text{pullback.snd } f g.$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackRightPullbackFstIso_hom_snd :
    (pullbackRightPullbackFstIso f g f').hom ≫ pullback.snd _ _ =
      pullback.snd f' (pullback.fst f g) ≫ pullback.snd f g :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right

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