pullbackLeftPullbackSndIso_hom_fst

English

The hom component of the left inverse iso associated to pasting commutes with fst in a specified way, reflecting a universal property of the pullback-cone after pasting.

Русский

Головной компонент гомоморфизма левого изоморфизма, связанного с pasting, коммутирует с fst в определенном виде, отражая универсальность конуса пуллбек-склейки.

LaTeX

$$$(\\mathrm{pullbackLeftPullbackSndIso}(f,g,g')).\\mathrm{hom} \\;\\circ\\; \\mathrm{pullback.fst}(f,\\, \\mathrm{comp}(g',g)) \;=\; \\mathrm{pullback.fst}(\\mathrm{pullback\\,snd}(f,g),g') \\circ \\mathrm{pullback.fst}(f,g)$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackLeftPullbackSndIso_hom_fst :
    (pullbackLeftPullbackSndIso f g g').hom ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _ :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left

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