pullbackLeftPullbackSndIso_inv_snd_snd

English

The inverse of the left iso followed by snd equals the snd map in the doubly pasted configuration, expressing a factorization through the second paste.

Русский

Обратное к левому изоморфизму с последующим snd даёт отображение snd в дважды склеенной конфигурации, выражая факторизацию через вторую склейку.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem pullbackLeftPullbackSndIso_inv_snd_snd :
    (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.snd _ _ = pullback.snd _ _ :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.right

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