inl_inl_pushoutLeftPushoutInrIso_hom

English

The composed inl maps across successive pushouts are coherent with the left-left composition in the pasted diagram.

Русский

Склеенные слои inl в последовательных пушаут-структурах образуют когерентное отображение слева налево в диаграмме pasted.

LaTeX

$$$(\\mathrm{inl} f g) \\circ (\\mathrm{inl} (\\mathrm{pushout.inr} f g) g') \\circ (\\mathrm{pushoutLeftPushoutInrIso}(f,g,g')).hom = \\mathrm{inl} f (\\mathrm{comp}(g,g'))$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_inl_pushoutLeftPushoutInrIso_hom :
    (pushout.inl f g) ≫ (pushout.inl (pushout.inr f g) g') ≫ (pushoutLeftPushoutInrIso f g g').hom =
      (pushout.inl f (g ≫ g')) :=
  by
  rw [← Category.assoc]
  apply IsColimit.comp_coconePointUniqueUpToIso_hom (pasteHorizIsPushout _ _ _) _ WalkingSpan.left

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