pushout_inl_iso_of_left_factors_epi

English

Given the isColimitOfFactors construction, the isColimit is preserved when passing from (f,g) to (x,y) via epi h.

Русский

Доказательство isColimit сохраняется при переходе от (f,g) к (x,y) через эпиморфизм h.

LaTeX

$$$\\text{isColimitOfFactors}(f,g,h,x,y,hhx,hhy, s, hs)$$$

Lean4

instance pushout_inl_iso_of_left_factors_epi (f : X ⟶ Y) : IsIso (pushout.inl _ _ : _ ⟶ pushout (h ≫ f) h) :=
  by
  convert
    (congrArg IsIso
          (show pushout.inl _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp f (𝟙 _) h⟩ WalkingSpan.left)).mp
      inferInstance
  · exact (Category.comp_id _).symm
  · exact (Category.comp_id _).symm

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