pullback_snd_iso_of_left_factors_mono

English

Let HasPullback f g and Mono g. Then HasPullback (f ≫ i) i.

Русский

Пусть существует pullback f g и моно g. Тогда HasPullback (f ≫ i) i.

LaTeX

$$$HasPullback\ (f \circ i) i.$$$

Lean4

instance pullback_snd_iso_of_left_factors_mono : IsIso (pullback.fst (f ≫ i) i) :=
  by
  have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono f (𝟙 _) i⟩ WalkingCospan.left
  convert (congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance
  · exact (Category.id_comp _).symm
  · exact (Category.id_comp _).symm

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