inl_pushoutRightPushoutInlIso_inv

English

Inverse coherence for the right-hand projection in the pasted configuration, relating snd maps across pastings.

Русский

Обратная когерентность для правой проекции в склейке, связанная через карты snd.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem inl_pushoutRightPushoutInlIso_inv :
    pushout.inl _ _ ≫ (pushoutRightPushoutInlIso f g f').inv = pushout.inl _ _ :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ _ WalkingSpan.left

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