pullback_snd_iso_of_right_factors_mono

English

Let f: X → Z and i: Z → W with Mono i. Then IsIso(pullback.snd i (f ≫ i)).

Русский

Пусть f: X → Z и i: Z → W с моно. Тогда IsIso(pullback.snd i (f ≫ i)).

LaTeX

$$$IsIso\ (pullback.snd\ i\ (f \circ i)).$$$

Lean4

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

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