pushout_inr_iso_of_right_factors_epi

English

If h: W → X is epi and HasPushout f g then HasPushout (h ≫ f) (h ≫ g).

Русский

Если h: W → X эпиморфизм и существуют пушпоуты для f,g, тогда HasPushout (h ∘ f)(h ∘ g).

LaTeX

$$$\\text{HasPushout }(h\\circ f)(h\\circ g)$$$

Lean4

instance pushout_inr_iso_of_right_factors_epi : IsIso (pushout.inr _ _ : _ ⟶ pushout h (h ≫ f)) :=
  by
  convert
    (congrArg IsIso
          (show pushout.inr _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp (𝟙 _) f h⟩ WalkingSpan.right)).mp
      inferInstance
  · apply (Category.comp_id _).symm
  · apply (Category.comp_id _).symm

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