inl_pushoutRightPushoutInlIso_hom

English

The inl map through the right pasting iso equals the direct inl map for the composed pushout, reflecting the horizontal pasting coherence.

Русский

Отображение inl через правый изоморфизм pasting эквивалентно прямому inl от композиции пушаутов, отражая горизонтальную когерентность.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem inl_pushoutRightPushoutInlIso_hom :
    pushout.inl _ _ ≫ (pushoutRightPushoutInlIso f g f').hom = pushout.inl _ _ :=
  IsColimit.comp_coconePointUniqueUpToIso_hom (pasteVertIsPushout rfl _ _) _ WalkingSpan.left

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